---

Sequential Programming

Emil Sekerinski, McMaster University, Fall 2019

---

Basic Statements

We use an algorithmic notation that, compared to common programming languages

• is simpler: it abstract from the specifics of particular programming languages,
• is more "expressive": features will be introduced that are not commonly available in programming languages.

Programs consist of

• variables that hold values,
• expressions that, when evaluted, have a result,
• statements that, when executed, have an effect on variables.

The basic statements are assignment, sequential composition, conditional, and repetition. We introduce them in textual form and visualize them by state diagrams.

The assignment evaluates expression and assigns the result to a variable. Suppose x is a variable and E an expressions:

x := E

Simple assignments can be generalized to multiple assignments in which two or more variables are modified. Suppose y is a variable distinct from x and E, F are expressions:

x, y := E, F

Suppose S, T are statements. Their sequential composition first executes S and then T:

algorithm
S ; T

The conditional statement evaluates a Boolean expression and executes a statement or does nothing, depending on the result. Suppose S, T are statements and B is a Boolean expression:

algorithm
if B then S else T

algorithm
if B then S

The repetitive statement executes the body, a statement, as long as the condition, a Boolean expression, is true. Suppose S is a statement and B is a Boolean expression:

while B do S

Statements can be composed to form more complex statements. For multi-line statements, indentation is used to avoid explicit parenthesis and the ; operator is left out at the end of lines. The following statements are the same:

if B then                   if B then (S ; T)
    S
    T

if B then                   if B then (if C then S else T)
    if C then
        S
    else
        T

Simple and composed statements always have a single entry and single exit. The shades below illustrate the hierarchical composition of statements. The example also illustrates that in composed statement, all transitions between states are labelled with a guard, an assignment, or a guard with an assignment:

algorithm
a, b := x, y
while a ≠ b do
    if a > b then
        a := a - b
    else
        b := b - a

Question: What does this program do?

Answer: It sets both a and b to the greatest common divisor of x and y.

Annotations and Correctness

Statements have a number of properties, like the length in lines, the size of the executable code, the running time, and the memory used. The property we consider here is which final state is produced for which initial state. For example:

if initially
then after
finally

x = 3
x := x + 1
x = 4

More generally, we consider the final states for a set of possible initial states. The initial and final states are characterized by predicates (Boolean expressions). For example:

if initially
then after
finally

x ≥ y
x := x + 1
x ≥ y + 1`

In general, for predicates P, Q, we express that under precondition P statement S establishes postcondition Q by the correctness assertion (color distinguishes programs from properties):

algorithm
  {P}  S  {Q}

A composed statement can be annotated with intermediate conditions, which are the pre- and postconditions of consitutent statements. The correctness of a statement with respect to its precondition, postcondition, and intermediate annotations is checked in state diagrams by following rule:

Rules for correctness of transitions:

if     P ∧ B ⇒ Q     then

if     P ⇒ Q[x, y := E, F]     then

if     P ∧ B ⇒ Q[x, y := E, F]     then

Here, P[x, y := E, F] stands for the simultaneous substitution of x with E and y with F. A statement is correct if all its transitions are correct.

The last rules is the most general one: by specializing the multiple assignment to "assign to no variables", the first rules emerges as a special case. By specializing B to be true, the second rules emerges.

Assuming x, y, z are integer variables, consider:

algorithm
    {x + y = 10}  z := x + y  {z = 10}

The assignment is correct with respect to the annotation provided if:

algorithm
    x + y = 10 ⇒ (z = 10)[z := x + y]

Here is the proof using equational logic, with justifications between the steps:

algorithm
    x + y = 10 ⇒ (z = 10)[z := x + y]
≡        {by substitution}
    x + y = 10 ⇒ x + y = 10
≡        {reflexivity of ⇒}
    true

Question: If the precondition and statement are fixed, what else are possible postconditions?

Answer:

• true (which does not say anything about the state)
• z = 10 ∧ x + y = 10 (as x, y do not change)

In general, if P is a Boolean-valued function, following holds for arbirary variable x and expression E:

algorithm
{P(E)}  x := E  {P(x)}

The correctness follows immediately from the rule for assignments.

Assuming a, u, y, z are integer variables, following annotated statement is correct:

algorithm
{z + u × y = a ∧ u > 0}
z, u := z + y, u - 1
{z + u × y = a ∧ u ≥ 0}

Here is the proof; simple steps are justified by "arithmetic" and "logic":

algorithm
    z + u × y = a ∧ u > 0 ⇒
          (z + u × y = a ∧ u ≥ 0)[z, u := z + y, u - 1]
≡        {by substitution, leaving out parenthesis}
    z + u × y = a ∧ u > 0 ⇒  z + y + (u - 1) × y = a ∧ u - 1 ≥ 0
≡        {distrbutivity of × over -; E - 1 ≥ F ≡ E > F for any E, F}
    z + u × y = a ∧ u > 0 ⇒  z + y + u × y - y = a ∧ u > 0
≡        {arithmetic}
    z + u × y = a ∧ u > 0 ⇒  z + u × y = a ∧ u > 0
≡        {logic}
    true

The next example involves sequential composition of statements. Suppose that x, y are program variables an A, B logical (or "ghost" variables)–variables that appear in annotations but not in statements. Following program exchanges the values of x and y without using an auxiliary variable:

algorithm
{x = A ∧ y = B}
x := x + y
{x - y = A ∧ y = B}
y := x - y
{y = A ∧ x - y = B}
x := x - y
{y = A ∧ x = B}

The correctness of the three assignments follows the corresponding conditions:

• x = A ∧ y = B ⇒ (x - y = A ∧ y = B)[x := x + y]
• x - y = A ∧ y = B ⇒ (y = A ∧ x - y = B)[y := x - y]
• y = A ∧ x - y = B ⇒ (y = A ∧ x = B)[x := x - y]

Exercise: Carry out the proofs!

The maximum of two numbers is defined as:

algorithm
m = max(x, y)   ≡   x ≤ m ∧ y ≤ m ∧ (m = x ∨ m = y)

Determining the maximum of two numbers involves a conditional statement:

algorithm
{true}
if x < y then
    m := y
else
    m := x
{m = max(x, y)}

The correctness follows from following conditions:

• x < y ⇒ (m = max(x, y))[m := y]
• x ≥ y ⇒ (m = max(x, y))[m := x]

To prove the first implication, rather than reducing it to true, we show that the left-hand side is a consequence of the right-hand side:

algorithm
    (m = max(x, y))[m := y]
≡        {by substitution, leaving out parenthesis}
    y = max(x, y)
≡        {definition of max}
    x ≤ y ∧ y ≤ y ∧ (y = x ∨ y = y)
≡        {reflexivity of ≤, =}
    x ≤ y ∧ true
≡        {simplification}
    x ≤ y
⇐        {E < F ⇒ E ≤ F for any E, F}
    x < y

Further on, annotations of true in programs and in state diagrams will be left out.

Aside: Flowcharts are different from state diagrams; in flowcharts, statements are attached to nodes rather than to vertices:

We continue with state diagrams as they are more suitable for visualizing concurrency.

Exercise: Generalize max to three arguments and develop the corresponding program!

The next program computes the product of integer variables x and y by successive additions:

algorithm
{x ≥ 0}
z, u := 0, x
{z + u × y = x × y ∧ u ≥ 0}
while u > 0 do
    z, u := z + y, u - 1
{z = x × y}

The correctness follows from these conditions:

• x ≥ 0 ⇒ (z + u × y = x × y ∧ u ≥ 0)[z, u := 0, x]
• u > 0 ∧ z + u × y = x × y ∧ u ≥ 0 ⇒
     (z + u × y = x × y ∧ u ≥ 0)[z, u := z + y, u - 1]
• u ≤ 0 ∧ z + u × y = x × y ∧ u ≥ 0 ⇒
     z = x × y

The intermediate annotation above is a loop invariant: it captures the design decision behind the loop, namely how z approximates the product.

Loop invariants are analogous to induction hypothesis: a loop invariant has to hold at entry of the loop (induction base) and assuming that the loop invariant holds at the beginning of the body, it has to hold at the end (induction step).

Exercise: Complete the three proofs!

For integers x, y, the greatest common divisior gcd(x, y) is integer d such that d divides x and y and any other divisor of x and y divides d. Following properties hold:

algorithm
	gcd(x, x) = x
	gcd(x, y) = gcd(y, x)
	gcd(x, y) = gcd(x - y, y)    if    x > y

The annotated algorithm using Euclid's method for the greatest common divisor is:

algorithm
{x > 0 ∧ y > 0}
a, b := x, y
{gcd(a, b) = gcd(x, y) ∧
 a > 0 ∧ b > 0}
while a ≠ b do
    if a > b then
        a := a - b
    else
        b := b - a
{a = gcd(x, y)}

Exercise: State the conditions for correctness and complete the proofs!

The correctness rules can be equivalently expressed in textual form, which is more suitable for larger programs. There is one rule for each kind of statements:

Rules for correctness of statements:

{P} x, y := E, F {Q}

{P} S ; T {R}

{P} if B then S else T {Q}

{P} if B then S {Q}

{P} while B do S {Q}

if   P ⇒ Q[x, y := E, F]

if   {P} S {Q}   and  {Q} T {R}

if   {P ∧ B} S {Q}   and  {P ∧ ¬B} T {Q}

if   {P ∧ B} S {Q}   and  P ∧ ¬B ⇒ Q

if   {P ∧ B} S {P}   and  P ∧ ¬B ⇒ Q

Let's apply the rules for correctness assertions to programs with loops. For integers x, y, the quotient x div y (also written x ÷ y) and the remainder x mod y are defined for all y > 0 by:

algorithm
x div y = q        ≡        x = q × y + r  
x mod y = r                 0 ≤ r < y

The following program determines x div y and x mod y by addition and subtraction:

algorithm
{x ≥ 0 ∧ y > 0}
q, r := 0, x
{x = q × y + r ∧ r ≥ 0 ∧ y > 0}
while r ≥ y do
    q, r := q + 1, r - y
{q = x div y ∧ r = x mod y}

Applying the rules, the correctness follows from:

algorithm
{x ≥ 0 ∧ y > 0}
q, r := 0, x
{x = q × y + r ∧ r ≥ 0 ∧ y > 0}

algorithm
{r ≥ y ∧ x = q × y + r ∧ r ≥ 0 ∧ y > 0}
q, r := q + 1, r - y
{x = q × y + r ∧ r ≥ 0 ∧ y > 0}

algorithm
r < y ∧ x = q × y + r ∧ r ≥ 0 ∧ y > 0   ⇒   q = x div y ∧ r = x mod y

Exercise: Complete the three proofs!

Aside: For negative divisors, we have for example -5 div 2 = -3 and -5 mod 2 = 1. This is the most natural definition. Python follows it, but not all programming languages do.

An array of type array D of T is a function D → T where the domain D is a "small" range of integers. Updating an array element is formally defined as assigning a new, altered array:

x(E) := F    =    x := (x; E: F)

The alter function (x; E: F) is defined by:

(x; E: F)(G)  =  F        if   E = G
(x; E: F)(G)  =  x(G)   if   E ≠ G 

For example, given array x of suitable type, in

algorithm
{x(0) = a ∧ x(1) = b}
x(1) := c
{x(0) = a ∧ x(1) = c}

the assignment is first replaced with:

algorithm
x := (x; 1: c)

The proof is then:

algorithm
    x(0) = a ∧ x(1) = b ⇒ (x(0) = a ∧ x(1) = c)[x := (x; 1: c)]
≡        {by substitution, leaving out parenthesis}
    x(0) = a ∧ x(1) = b ⇒ (x; 1: c)(0) = a ∧ (x; 1: c)(1) = c
≡        {definition of alter, twice}
    x(0) = a ∧ x(1) = b ⇒ x(0) = a ∧ c = c
≡        {simplification}
    true

Let a: array 0 .. N - 1 of integer be an array whose sum is to be computed and N ≥ 0 a constant:

algorithm
{true}
s, k := 0, 0
{s = (∑ i ∈ 0 .. k - 1 • a(i)) ∧ 0 ≤ k ≤ N}
while k < N do
    s, k := s + a(k), k + 1
{s = (∑ i ∈ 0 .. N - 1 • a(i))}

Exercise: Prove the program correct with respect to the annotation!

Let a, b, c : array 0 .. N - 1 of integer represent three vectors of length N ≥ 0; following program sets c to the sum of a and b:

algorithm
{true}
k := 0
{(∀ i ∈ 0 .. k - 1 • c(i) = a(i) + b(i)) ∧ 0 ≤ k ≤ N}
while k < N do
    c(k), k := a(k) + b(k), k + 1 end
{∀ i ∈ 0 .. N - 1 • c(i) = a(i) + b(i)}

Exercise: Prove the program correct with respect to the annotation!

Undefinedness and Conditional Evaluation

In mathematics, E = E is universally true: it holds even if E is 1/0! In programs, evaluating E = E may result in an error.

• Programming languages detect programming errors, for example when a division by zero or an array access out of its domain is attempted and no reasonable course of action is possible.

• Errors also arise due to machine limitations, like the finiteness of integers and the approximation of real numbers by floating point numbers.

The correctness rules so far were idealized: they ignored potential undefinedness of expressions. The rules are now extended to guarantee the absence of such errors arising from undefinedness.

So far, the same expression appeared in programs and in annotations. Now we distinguish between expressions in annotations and program expressions.

The same operator, like +, can appear in annotations and in programs, but with a different meaning: in annotations + is mathematical addition, in programs + can overflow.

We write and, or for conditional conjunction and disjunction in program expressions. Consider following program, a linear search of key: T in array a: array 0 .. N - 1 of T:

algorithm
k := 0
while k < N and a(k) ≠ key do
    k := k + 1

The evaluation of E and F is conditional: if E is false, the result is false and F is not evaluated at all.

This is essential in above linear search, as when the search reaches k = N (in case key is not in a), k < N is false and a(k) ≠ key is not evaluated: if it were, it would lead to an error as a would be indexed outside its domain! Therefore, taking a(k) ≠ key and k < N as the guard would be incorrect.

Similarly, E or F is evaluated conditionally: if E is true, the result is true and F is not evaluated at all. Suppose text: array 0 .. L - 1 of char and EOL is a constant of type char. Suppose that end-of-line is reached either at the end of text or at an EOL character:

algorithm
eol := pos = L or text[pos] = EOL

Here, text[pos] is not evaluated if pos = L.

In general, if E and F, E or F evaluate successfully, the value is that of E ∧ F, E ∨ F.

Notation: Different notations are common for conditional conjunction and disjunction: cand, cor (Dijkstra); and then, or else (Eiffel); &&, || (C, Java, C#, Swift); and, or (Pascal, Python, here).

For program expression E, we consider its

• value E', a mathematical expression to what it evaluates, and its
• definedness ∆E, a mathematical expression telling when the evaluation succeeds.

For example, if machine arithmetic is bounded, the result of an arithmetic operation has to be between the minimal and maximal representable integer. If the word size is 32 bits, unsigned integers can only be less than 2³²:

value	definedness
(x + y)' = x + y	∆(x + y) ≡ x + y ≤ 2³²	where x, y are unsigned integer variables
(x div y)' = x div y	∆(x div y) ≡ y ≠ 0

Some programming languages use arithmetic modulo the word size:

value	definedness
(x + y)' = (x + y) mod 2³²	∆(x + y) ≡ true	where x, y are unsigned integer variables
(x div y)' = x div y	∆(x div y) ≡ y ≠ 0

In saturating arithmetic, the result is capped at the maximal representable value (this is used in signal processing):

| value | definedness | | |:--------------------|:-------------------------------------|:-----------------------------| | (x + y)' = min(x + y, 2³² - 1) | ∆(x + y) ≡ true | where x, y are unsigned integer variables | | (x div y)' = x div y | ∆(x div y) ≡ y ≠ 0 |

Value and definedness are defined over the structure of program expressions:

value	definedness
c' = c	∆c ≡ true	where c is constant true, false, 0, 1, ...
x' = x	∆x ≡ true	where x is a variable
x(E)' = x(E')	∆x(E) ≡ ∆E ∧ E' ∈ D	where x : array D of T and E is an expression

Assuming that signed integers are bounded between minint and maxint and have for value and defineness in bounded arithmetic, assuming E, F are integer expressions:

value	definedness
(-E)' = -E'	∆(-E) = ∆E ∧ minint ≤ -E' ≤ maxint
(E + F)' = E' + F'	∆(E + F) = ∆E ∧ ∆F ∧ minint ≤ E' + F' ≤ maxint
(E - F)' = E' - F'	∆(E - F) = ∆E ∧ ∆F ∧ minint ≤ E' - F' ≤ maxint
(E × F)' = E' × F'	∆(E × F) = ∆E ∧ ∆F ∧ minint ≤ E' × F' ≤ maxint
(E div F)' = E' div F'	∆(E div F) = ∆E ∧ ∆F ∧ F' ≠ 0
(E mod F)' = E' mod F'	∆(E mod F) = ∆E ∧ ∆F ∧ F' ≠ 0

Boolean operators are strict in the sense that all operands have to be defined, like arithmetic operators, except for and, or, which are conditional. Assuming B, C are Boolean expressions and E, F expression of the same type, we have:

| value | definedness
|:-----------------------|:-------------------------------| | (¬B)' = ¬B' | ∆(¬B) = ∆B |
| (B and C)' = B' ∧ C' | ∆(B and C) = ∆B ∧ (B' ⇒ ∆C) | | (B or C)' = B' ∨ C' | ∆(B or C) = ∆B ∧ (B' ∨ ∆C) | | (E = F)' = (E' = F') | ∆(E = F) = ∆E ∧ ∆F | | (E < F)' = (E' < F') | ∆(E < F) = ∆E ∧ ∆F | | (E ≤ F)' = (E' ≤ F') | ∆(E ≤ F) = ∆E ∧ ∆F | | ... | ... |

Conditional and, or appear only in programs, mathematical ∧, ∨ appear only in annotations.

As an example, we determine the definedness of k < N and a(k) ≠ key in above linear search:

algorithm
    ∆(k < N and a(k) ≠ key)
≡        {by ∆ of and}
    ∆(k < N) ∧ ((k < N)' ⇒ ∆(a(k) ≠ key))
≡        {by ∆ of <, ≠ and ' of <}
    ∆k ∧ ∆N ∧ (k < N ⇒ ∆a(k) ∧ ∆key))
≡        {by ∆ of variable, constant; simplification}
    k < N ⇒ ∆a(k)
≡        {by ∆ of indexing}
    k < N ⇒ k ∈ 0 .. N - 1
≡        {as k ∈ 0 .. N - 1 ≡ 0 ≤ k < N; logic}
    k < N ⇒ 0 ≤ k

The correctness rules are revised to take undefinedness of expressions into account:

Extended rules for correctness of statements:

{P} x, y := E, F {Q}

{P} S ; T {R}

{P} if B then S else T {Q}

{P} if B then S {Q}

{P} while B do S {Q}

if P ⇒ ∆E ∧ ∆F ∧ Q[x, y := E', F']

if {P} S {Q} and {Q} T {R}

if P ⇒ ∆B and {P∧B'} S {Q} and {P∧¬B'} T {Q}

if P ⇒ ∆B and {P ∧ B'} S {Q} and P ∧ ¬B' ⇒ Q

if P ⇒ ∆B and {P ∧ B'} S {P} and P ∧ ¬B' ⇒ Q

A possible annotation for the linear search is:

algorithm
{P: true}
k := 0
{Q: (∀ i ∈ 0 .. k - 1 • a(i) ≠ key) ∧ 0 ≤ k ≤ N}
while k < N and a(k) ≠ key do
    k := k + 1
{R: (∀ i ∈ 0 .. k - 1 • a(i) ≠ key) ∧ 0 ≤ k ≤ N ∧ (k < N ⇒ a(k) = key)}

The correctness follows from applying the extended rules for sequential composition and repetition:

algorithm
{P}
k := 0
{Q}

algorithm
Q ⇒ ∆(k < N and a(k) ≠ key)

algorithm
{Q ∧ (k < N and a(k) ≠ key)'}
k := k + 1
{Q}

algorithm
Q ∧ ¬(k < N and a(k) ≠ key)' ⇒ R

Exercise: Above postcondition specifies that k is the index of the first occurrence of key. Weaken the postcondition to allow k to be the index of any occurrence.

Program Development

Larger programs are decomposed into modules that may have private variables which can only be accessed through public procedures, a principle known as encapsulation. While the inner working of a module may be intricate, the specification of the module should remain simple.

The following development illustrates how a module is specified with abstract variables and these are used in annotations.

The task is to print a picture given by the functions (or array) fx, fy, where

algorithm
∀ i ∈ 0 .. N - 1 • 0 ≤ fx(i) < X ∧ 0 ≤ fy(i) < Y

We assume that the printer can print only one black dot at a time and starts at the upper left corner. The printer is controlled by following commands:

• newLine: start a new line at the leftmost position
• advance: move the print head one position to the right
• print: print a dot and move one position to the right

The state of the printer is represented by the state of the paper and the coordinates of the print head. Each dot on the paper is represented by a boolean value, true for black and false for white.

algorithm
var paper: array 0 .. X - 1, 0 .. Y - 1 of bool
var hx, hy: integer

algorithm
newLine:
    hx, hy := 0, hy + 1
advance:
    hx := hx + 1
print:
    paper(hx, hy) := true ; hx := hx + 1

Initially the paper is blank and the print head is at the origin:

P0:
    (∀ i ∈ 0 .. X - 1, j ∈ 0 .. Y - 1 • ¬paper(i, j)) ∧
    hx = 0 ∧ hy = 0

The printing task is then specified by:

algorithm
{P1: P0 ∧ (∀ i ∈ 0 .. N - 1 • 0 ≤ fx(i) < X ∧ 0 ≤ fy(i) < Y)}
printPicture
{∀ i ∈ 0 .. X - 1, j ∈ 0 .. Y - 1 •
    paper(i, j) = (∃ k ∈ 0 .. N - 1 • i = fx(k) ∧ j = fy(k))}

Our approach is first to build the whole image in memory and then to print it. To this end, we declare a variable of the size of the paper:

algorithm
printPicture:
    var image: array 0 .. X - 1, 0 .. Y - 1 of bool
        buildImage
        {P0 ∧ ∀ i ∈ 0 .. X - 1, j ∈ 0 .. Y - 1 •
            image(i, j) = (∃ k ∈ 0 .. N - 1 • i = fx(k) ∧ j = fy(k))}
        printImage
        {paper = image}

It is easy to see that the paper will satisfy the desired postcondition of printImage.

We refine buildImage: we first have to clear image and then can set the dots:

algorithm
buildImage:
    clearImage
    {P1 ∧ (∀ i ∈ 0 .. X - 1, j ∈ 0 .. Y - 1 • ¬image(i, j))}
    markDots

We refine clearImage by clearing all lines:

algorithm
clearImage:
    var y : integer
        y := 0
        {P2: P1 ∧ (∀ i ∈ 0 .. X - 1, j ∈ 0 .. y - 1 • ¬image(i, j))}
        while y < Y do
            clearLine(y) ; y := y + 1

We refine clearLine(y) by clearing all dots of line y:

algorithm
clearLine(y):
    var x : integer
        x := 0
        {P2 ∧ (∀ i ∈ 0 .. x - 1 • ¬image(i, y))}
        while x < X do
            image(x, y) := false ; x := x + 1

We refine markDots by iterating over all N dots to be drawn:

algorithm
markDots:
    var n : integer
        n := 0
        {∀ x ∈ 0 .. X - 1, y ∈ 0 .. Y - 1 •
            image(x, y) = (∃ i ∈ 0 .. n - 1 • x = fx(i) ∧ y = fy(i))}
        while n < N do
            image(fx(n), fy(n)) := true ; n := n + 1

We refine printImage by printing all lines from top to bottom:

algorithm
printImage:
    var y : integer
        y := 0
        {P3: ∀ i ∈ 0 .. X - 1, j ∈ 0 .. y - 1 •
            paper(i, j) = image(i, j)
            paper(i, j) = (∃ k ∈ 0 .. N - 1 • i = fx(k) ∧ j = fy(k))}
        while y < N do
            printLine(y) ; newLine ; y := y + 1

Finally we refine printLine(y) by printing all dots of a line:

algorithm
printLine(y):
    var x : integer
        x := 0
        {P3 ∧ (∀ i ∈ 0 .. x - 1 •
            paper(i, y) = (∃ k ∈ 0 .. N - 1 • i = fx(k) ∧ y = fy(k)))}
        while x < X do
            if image(x, y) then print else advance
            x := x + 1

By putting all parts together we arrive at the complete program:

algorithm
printPicture:
    var image: array 0 .. X - 1, 0 .. Y - 1 of bool
    var x, y, n : integer
        y := 0
        while y < Y do
            x := 0
            while x < X do
                image(x, y) := false ; x := x + 1
            y := y + 1
        n := 0
        while n < N do
            image(fx(n), fy(n)) := true ; n := n + 1
        y := 0
        while y < N do
            x := 0
            while x < X do
                if image(x, y) then print else advance
                x := x + 1
            newLine ; y := y + 1

A formal proof is laborious as intermediate annotations get long: for example, P0 has to be "carried along" in all intermediate annotations of buildImage to be available as a precondition of printImage. Following two rules help to reason about smaller annotations:

Rules for simplification of correctness reasoning:

{P} S {P}

{P0 ∧ P1} S {Q0 ∧ Q1}

if variables assigned in S do not occur in P

if   {P0} S {Q0}   and   {P1} S {Q1}

Hierarchical Diagrams

Nesting allows an annotation that is repeated in several states to be factored out into a superstate. Following are equivalent diagrams:

As long as the computation resides within the superstate, R is an invariant. For example, the algorithm for multiplication by shifting is:

algorithm
{x ≥ 0}
z, u, v := 0, x, y
{z + u × v = x × y ∧ u ≥ 0}
while u ≠ 0 do
    if odd(u) then
        z := z + v
    u, v := u div 2, 2 × v
{z = x × y}

Following are two equivalent diagrams; the one to the right factors out u > 0 to a superstate:

Nondeterminism and Blocking

The skip statement does nothing (noop in assembly, pass in Python). For example:

if B then S   =   if B then S else skip

Guarded commands, introduced by Dijkstra, generalize the conditional and repetitive statements to multiple alternatives:

algorithm
if B → S ⫿ C → T

If B holds, executes S; if C holds, executes T; if both hold, selects one nondeterministically; if none holds, stops execution ("gets stuck").

algorithm
do B → S ⫿ C → T

If B holds, executes S and starts over again; if C holds, executes T and starts over again; if both hold selects one nondeterministically; if none holds, finishes.

Here is Euclid's algorithm for the gcd with guarded commands next to the earlier formulation:

a, b := x, y
do a ≠ b →
    if a > b → a := a - b
     ⫿ a < b → b := b - a

a, b := x, y
while a ≠ b do
    if a > b then a := a - b
    else b := b - a

Question: Is the guarded if well-defined? In what way is it more abstract than the corresponding if-then-else?

Answer: The guards x < y and x > y are only evaluated if x ≠ y, hence the if never stops. It is more abstract as it does not contain an arbitrary choice what to do if x = y, as the if-then-else does, a situation that cannot occur.

Argue that the following formulation is equivalent:

a, b := x, y
do a > b → a := a - b
 ⫿  a < b → b := b - a

Next is a program for sorting integers x, y, z into ascending order by swapping two "adjacent" elements:

do x > y → x, y := y, x
 ⫿  y > z → y, z := z, y

Question: In which ways is this more abstract than a deterministic program doing the same? Is the outcome always the same as with a deterministic program? Think of the situation when x, y, z are 5, 4, 3!

Answer: A deterministic program would give preference to either swapping x, y first or y, z first, even if it does not matter. The outcome is here always the same as that of a deterministic program.

Rules for correctness of guarded commands:

{P} skip {Q}

if P ⇒ Q

{P} if B → S ⫿ C → T {Q}

if P ⇒ ∆B
and P ⇒ ∆C
and {P ∧ B'} S {Q}
and {P ∧ C'} T {Q}

{P} do B → S ⫿ C → T {Q}

if P ⇒ ∆B
and P ⇒ ∆C
and {P ∧ B'} S {P}
and {P ∧ C'} T {P}
and P ∧ ¬B' ∧ ¬C' ⇒ Q

Question: Guarded commands can have an arbitrary number of alternatives. What is the meaning of if with a single alternative?

{P} if B → S {Q}

if P ⇒ ∆B
and {P ∧ B'} S {Q}

Answer: If B holds initially, executes S, otherwise stops (stays in initial state).

Question: If additionally B is false, what is the meaning then?

Answer: if false → S always stops.

We can formally define a stop statement by:

    stop = if false → skip

It has the "miraculous" property of establishing any postcondition, by not reaching the final state.

Aside: If an if without alternatives were allowed as a statement, it would also be stop.

Historically, nondeterminism was first connected to concurrent programs. However, nondeterminism allows describing any kind of programs more abstractly. Nondeterminism commonly arises in the specification of programs, to allow the implementation more freedom.

Here is an example from the Python documentation of built-in sets:

pop() Remove and return an arbitrary element from the set. Raises KeyError if the set is empty.