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.