Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    A Refinement Calculus for Communicating Processes with State

    1st Irish Workshop on Formal Methods

    Dublin, Ireland. 3rd - 4th July 1997


    L. Lai & J.W. Sanders


    A uniform treatment is presented of specifications, programs, and programming for communicating processes with machine state.

    The treatment is based on addition of a specification statement to a CSP-like language. The extended language is viewed as a specification language in which programs are identified with a subclass of specifications.

    A semantics is provided and here a selection of sound refinement laws is given to support the development of programs from specifications.

    The result is a homogeneous framework for the specification and development of parallel programs which, as usual, guarantees functional correctness of an implementation as a consequence of development using its laws. An example is given to demonstrate use of the method.


    PDF filePDF Version of this Paper (172kb)