← Back to System Internals

Basic Commands & the Assignment Axiom

The primitive statements of Gries’ tiny language and the semantics that make each one provable — skip, abort, assignment, and sequential composition — with the assignment axiom, the rule everyone gets backward the first time, at the centre.

The weakest-precondition calculus is only as trustworthy as the language it describes. Gries deliberately keeps that language tiny: a handful of primitive commands, each with a single, precisely stated wp rule. This page covers the straight-line core — skip, abort, assignment (single, multiple, and to array elements), and sequential composition — and derives the semantics you will use in every proof. The star of the show is the assignment axiom, whose backward substitution is both the most surprising and the most useful rule in the book.

A deliberately tiny language

Gries’ programming notation is small on purpose. Every construct you add to a language is a construct whose semantics you must define, whose wp rule you must trust, and whose proof obligations you must discharge. A small language means few axioms to trust — and few is exactly what you want when correctness is the goal. The entire language reduces to these constructs:

This page covers the straight-line subset — everything except selection and iteration. Those two branching constructs get their own treatment; the alternative command (if…fi) is at sop-05-alternative.html. For the general laws that every command’s wp obeys — excluded miracle, distributivity, monotonicity — see sop-03-wp.html.

skip and abort

The two simplest commands sit at opposite extremes: one does nothing, the other does nothing useful ever.

skip — the do-nothing command

skip changes no variable. Whatever was true before is still true after, so its weakest precondition is the postcondition unchanged. It is the identity of sequential composition: skip ; S and S ; skip both equal S.

abort — the never-succeeds command

abort models a fault — a program that fails, or that never terminates. It is guaranteed to establish nothing, not even the trivially-true postcondition T. So its weakest precondition is F: there is no starting state from which abort is guaranteed to reach any given R.

Two facts make abort worth keeping in the language even though you would never write it deliberately. First, it is the identity of nondeterministic choice: in a set of guarded alternatives, an arm that can never be selected behaves like abort, and the calculus treats a command with no true guard as aborting. Second, it is a precise reasoning tool — when a derivation forces wp = F, that is the calculus telling you the specification is unsatisfiable from that state. abort is how “this can go wrong” is expressed formally rather than hand-waved.

Sequential composition

To run S1 ; S2 is to run S1, then run S2 on the resulting state. To make R hold at the end, S1 must land in a state from which S2 can still establish R — that intermediate condition is exactly wp(S2, R). So the rule composes the two transformers:

The crucial habit this rule teaches: reason right-to-left. Take the final postcondition, push it back through S2 to get an intermediate condition, then push that back through S1. You work from the goal toward the start — the opposite of the order the machine executes, and exactly the order in which you should design. For a longer chain S1 ; S2 ; S3 you peel from the right:

# wp("S1 ; S2 ; S3", R)
#   = wp(S1, wp(S2, wp(S3, R)))
# compute the innermost first, then move left
step3 = wp("S3", R)          # condition needed before S3
step2 = wp("S2", step3)      # condition needed before S2
step1 = wp("S1", step2)      # condition needed before S1  = the precondition

The assignment axiom

This is the centrepiece — the single rule that makes program proving mechanical. The weakest precondition of an assignment is the postcondition with the target variable textually replaced by the assigned expression, and the substitution runs backward, into the postcondition, which trips up everyone the first time.

Gries is careful about one more thing: the expression e must be defined in the starting state — no division by zero, no array index out of bounds, no undefined function application. The full form carries a domain condition:

Why backward, not forward

The natural but wrong instinct is to reason forward: “x := 5, so afterward x = 5” — and then to substitute into the precondition. The axiom does the opposite: it substitutes into the postcondition. Think of it as asking “what must be true of e now, so that after copying e into x, the claim R about x holds?” The answer is R with x’s slot filled by e.

# "x := x + 1 makes x bigger,
#  so the precondition must be x > 10"
# Wrong: this pushes forward and
# substitutes into the PREcondition.

# Want post:  x > 10   after   x := x + 1
# Wrong guess: pre is x > 10
# (that would give x > 11 afterward)

# wp("x := x + 1", x > 10)
#   = (x > 10)[x := x + 1]
#   = (x + 1 > 10)
#   = x > 9

# So:  {x > 9}  x := x + 1  {x > 10}   ✓
# Replace x by e in R, then simplify.

More examples

The mechanics are always the same: copy the postcondition, replace every free x with e, simplify, and attach a domain condition if e can be undefined.

# (1) A plain arithmetic postcondition
wp("x := x * 2", x < 100)   =  (x*2 < 100)   =  x < 50

# (2) Establishing an exact value
wp("x := y + 1", x = 7)      =  (y + 1 = 7)   =  y = 6

# (3) An array read on the right-hand side
#     e = b[i] is defined only when i is a legal index
wp("x := b[i]", x > 0)
    =  domain(b[i]) ∧ (b[i] > 0)
    =  (0 ≤ i < n) ∧ (b[i] > 0)

# (4) Division — the domain condition earns its keep
#     e = a / b is defined only when b ≠ 0
wp("x := a / b", x = q)
    =  domain(a/b) ∧ (a/b = q)
    =  (b ≠ 0) ∧ (a = q*b)     # without b≠0 the wp is meaningless

Example (4) is the reason the domain condition is not pedantry: drop b ≠ 0 and the precondition would falsely claim the assignment is safe from a state where it faults. The calculus refuses to lie about that.

Multiple (simultaneous) assignment

The multiple assignment x, y := e, f evaluates both right-hand sides in the starting state and then assigns them simultaneously. Its wp is a simultaneous substitution — every free x becomes e and every free y becomes f, all at once, with no interference between them:

The payoff is the classic swap, provable in a single step. Let X and Y be the initial values, and take postcondition x = X ∧ y = Y:

# {?}  x, y := y, x  {x = X and y = Y}
wp("x, y := y, x", x = X ∧ y = Y)
    =  (x = X ∧ y = Y)[x, y := y, x]
    =  (y = X ∧ x = Y)            # both substituted at once
# precondition:  y = X and x = Y   →  the swap is proven

Contrast this with the three-statement sequential version using a temporary. It needs composition (right-to-left) and an extra variable, and each intermediate state must be tracked:

x, y := y, x
# wp = (y = X and x = Y)
# no temporary, no ordering to reason about

t := x ;  x := y ;  y := t
# wp("y:=t", x=X ∧ y=Y)  = (x=X ∧ t=Y)
# wp("x:=y", x=X ∧ t=Y)  = (y=X ∧ t=Y)
# wp("t:=x", y=X ∧ t=Y)  = (y=X ∧ x=Y)
# same precondition — more machinery

The simultaneity matters: x, y := y, x is not the same as x := y ; y := x, which would clobber x before y could read its old value. Reading both right-hand sides in the original state is precisely what makes the one-step swap correct.

Array element assignment

Assigning to a single array element, b[i] := e, looks like it changes only one slot — but formally it changes the whole array. Gries models an array as a function from indices to values, and b[i] := e replaces b with an altered function, written (b; i:e), that agrees with b everywhere except at index i, where it returns e:

Treating the assignment as replacing the entire array b (not just editing a cell) is what keeps the substitution rule sound — the ordinary assignment axiom applies verbatim, with the altered function as the “expression.” An example:

# wp("b[i] := 5", b[i] = 5)
#   = (b[i] = 5)[b := (b; i:5)]
#   = (b; i:5)[i] = 5
#   = 5 = 5
#   = T          (with domain: 0 ≤ i < n)

wp("b[i] := e", b[j] = c)
    =  (b[j] = c)[b := (b; i:e)]
    =  (b; i:e)[j] = c
    =  (i = j ∧ e = c)  ∨  (i ≠ j ∧ b[j] = c)
# the i = j alias is easy to forget — and a classic source of bugs

Worked: proving a straight-line program correct

Put the rules together on a small assignment sequence. The task: given the precondition, prove the program establishes y = a*a + 1. We push the postcondition back through each statement, right-to-left, using the assignment axiom at every step.

# Program (straight-line, no branches):
#   {a ≥ 0}
#   x := a ;
#   x := x * x ;
#   y := x + 1
#   {y = a*a + 1}

# Derive the wp from the bottom up (right-to-left).

# Step 1 — push through  y := x + 1
wp("y := x + 1", y = a*a + 1)
    =  (y = a*a + 1)[y := x + 1]
    =  (x + 1 = a*a + 1)
    =  x = a*a                              # call this R2

# Step 2 — push R2 through  x := x * x
wp("x := x * x", x = a*a)
    =  (x = a*a)[x := x*x]
    =  (x*x = a*a)                          # call this R1

# Step 3 — push R1 through  x := a
wp("x := a", x*x = a*a)
    =  (x*x = a*a)[x := a]
    =  (a*a = a*a)
    =  T                                    # the derived precondition

# Result:  wp(whole program, y = a*a + 1) = T
# The precondition simplifies to T, and a ≥ 0 ⇒ T trivially,
# so  {a ≥ 0} x:=a; x:=x*x; y:=x+1 {y = a*a + 1}  holds.  ✓

Because the derived precondition is T, the program is correct from any starting state — the stated precondition a ≥ 0 is stronger than required and trivially implies it. Every line was verified purely by textual substitution; no execution, no test cases, no guessing.

Summary