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
Also,
{ true } x := x' | rel
is the same as
x := x' | rel.