Specification and Programming Notation

In the following, S and T are programs (or sub-programs), g, p, and q are boolean (or logical) expressions, E is a general expression, x is a program variable (or a list of program variables), and X is a type (or a list of types).

Sequential Composition: S ; T

Conditional: IF g THEN S ELSE T FI

Iteration: DO g -> S OD

Local Variable: VAR x:X . S

Local Constant: CON x:X . S

Assignment: x := E

Skip Statement: skip
We have that (skip;S) = S = (S;skip).

Assertion: { p }
Assume that condition p holds at this point in the program. We have that {true} = skip.

Generalised Assignment: x := x' | q
x is assigned a value x' satisfying the condition q. For example, x:=x' | x' > x increments x by some arbitrary amount.

Specification Statement: { p } x := x' | q
This is simply an assertion followed by a generalised assignment. In the refinement laws, we write a specification statement as

       { pre }  x := x'  |  rel

since pre represents a precondition, and rel represents a relation between the initial state, x, and the final state, x'. A special case is when rel is independent of the initial value of x and is thus simply a postcondition; we write this as:

       { pre }  x := x'  |  post


       { true }  x := x'  |  rel

is the same as

      x := x'  |  rel.