Sequential Programming

Emil Sekerinski, McMaster University, January 2022


Licensed under Creative Commons CC BY-NC-ND

Fundamental 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 evaluated, have a result,
  • statements that, when executed, have an effect on variables.

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

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

algorithm
x := E

</div>

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:

algorithm
x, y := E, F

</div>

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

algorithm
S ; T

</div>

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

</div>

algorithm
if B then S

</div>

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:

algorithm
while B do S

</div>

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:

algorithm
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

</div>

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}

</div>

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

</div>

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

</div>

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

</div>

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}

</div>

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 arbitrary variable x and expression E:

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

</div>

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}

</div>

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 ghost (or logical 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}

</div>

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]

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)}

</div>

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 reasoning about correctness, in particular of concurrent programs.

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}

</div>

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).

For integers x, y, the greatest common divisor 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)}

</div>

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:

  1. algorithm
    {x ≥ 0 ∧ y > 0}
    q, r := 0, x
    {x = q × y + r ∧ r ≥ 0 ∧ y > 0}
  2. 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}
  3. algorithm
    r < y ∧ x = q × y + r ∧ r ≥ 0 ∧ y > 0   ⇒   q = x div y ∧ r = x mod y

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 is a function D → T where the domain D is a "small" range of integers and T is the type of he array elements. An array x: l .. u → T has elements x(l), x(l + 1), ..., x(u). 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: 0 .. N – 1 → integer be an array whose sum is to be computed and N ≥ 0 a constant. The invariant of the loop states that s is the partial sum of the first k elements of a:

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))}

</div>

Let a, b, c : 0 .. N – 1 → integer represent three vectors of length N ≥ 0; following program sets c to the sum of a and b. The invariant states that the first k elements of c are the sum of the corresponding elements 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
{∀ i ∈ 0 .. N – 1 • c(i) = a(i) + b(i)}

</div>

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: 0 .. N – 1 → 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: 0 .. L – 1 → 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.

In other word, we hava E' = E under the definedess ∆E. 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 where x, y are unsigned integer variables

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 where x, y are unsigned integer variables

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 where x, y are unsigned integer variables

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 : D → T and E is an expression

The corresponding values are not changed.

Assuming that signed integers are bounded between minint and maxint and have for value and definedness 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 := 0
while k < N and a(k) ≠ key do
    k := k + 1
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:

  1. algorithm
    {P}
    k := 0
    {Q}
  2. algorithm
    Q ⇒ ∆(k < N and a(k) ≠ key)
  3. algorithm
    {Q ∧ (k < N and a(k) ≠ key)'}
    k := k + 1
    {Q}
  4. algorithm
    Q ∧ ¬(k < N and a(k) ≠ key)' ⇒ R

Question: Above postcondition specifies that k is the index of the first occurrence of key. How can you weaken the postcondition to allow k to be the index of any occurrence?

Answer: 0 ≤ k ≤ N ∧ (k < N ⇒ a(k) = key)

Program Development: Minimal Segment Sum

For an array f: 0 .. N – 1 → integer, the segment sum ss(i, j) for 0 ≤ i ≤ j ≤ N is defined as:

algorithm
ss(i, j) = (∑ h ∈ i .. j – 1 • f(h))

The minimal segment sum is the smallest segment sum in an array:

algorithm
(MIN i ∈ 0 .. N, j ∈ i .. N • ss(i, j))

For example, if f = [1, 2, –3, 0, 2, –9, 7], the minimal segment sum is –10. Since the empty segment is allowed and has a sum of 0, the minimal segment sum can be at most 0. The number of combinations of i and j are N + 1 (for i = 0) plus N (for i = 1) plus N – 1 (for i = 2) etc., so in total (N + 1) × (N + 2) / 2. For each combination of i and j, in the order of N additions have to carried out. A naive program therefore requires time proportional to . How can a more efficient program be obtained?

Obviously all values of f need to be consulted, so the approach is to iterate over all elements, from n = 0 to N – 1. Let P0(n) be the invariant of the loop and let the final value of x be the minimal segment sum,

algorithm
"establish n = 0 and P0(0)"
{P0(n)}
while n < N do
    "modify x"
    {n < N ∧ P0(n + 1)}
    n := n + 1
    {P0(n)}

where:

P0(n) ≡ 0 ≤ n ≤ N ∧ x = (MIN i ∈ 0 .. n, j ∈ i .. n • ss(i, j))

For "establish n = 0 and P0(0)" we immediately get

algorithm
n, x := 0, 0

from the definiton of P0(n). For "modify x", the precondition is n < N ∧ P0(n); for its postcondition, we have:

algorithm
    P0(n + 1)
=       {by definition of P0}
    x = (MIN i ∈ 0 .. n + 1, j ∈ i .. n + 1 • ss(i, j))
=       {by case analysis j = n + 1 and j ≠ n + 1}
    x = min((MIN i ∈ 0 .. n, j ∈ i .. n • ss(i, j)),
            (MIN i ∈ 0 .. n + 1 • ss(i, n + 1)))

The first argument of min appears in the precondition, P0(n), suggesting for "modify x":

algorithm
x := min(x, (MIN i ∈ 0 .. n + 1 • ss(i, n + 1)))

A direct implementation of MIN would make the overall runtime still proportional to , but we can improve further. The shape of the expression suggests to intoduce a new variable, say y, with the invariant

P1(n) ≡ y = (MIN i ∈ 0 .. n • ss(i, n))

and update y in the loop. Thus the program becomes

algorithm
"establish n = 0 and P0(0) and P1(0)"
{P0(n) ∧ P1(n)}
while n < N do
    "modify y"
    {n < N ∧ P0(n) ∧ P1(n + 1)}
    x := min(x, y)
    {n < N ∧ P0(n + 1) ∧ P1(n + 1)}
    n := n + 1
    {P0(n)}

For "establish n = 0 and P0(0) and P1(0)" we now get:

algorithm
n, x, y := 0, 0, 0

The precondition of "modify y" is n < N ∧ P0(n) ∧ P1(n). For the postcondition we have:

algorithm
    P1(n + 1)
=       {by definition of P1}
    y = (MIN i ∈ 0 .. n + 1 • ss(i, n + 1))
=       {by case analysis y = n + 1 and y ≠ n + 1}
    y = min((MIN i ∈ 0 .. n • ss(i, n + 1)), ss(n + 1, n + 1))
=       {by definition of ss, empty summation}
    y = min((MIN i ∈ 0 .. n • ss(i, n) + f(n)), 0)
=       {i does not appear in f(n)}
    y = min((MIN i ∈ 0 .. n • ss(i, n)) + f(n), 0)

The first argument of min appears in the precondition P1(n), suggesting for "modify y":

algorithm
y := min(y + f(n), 0)

The resulting program, without annotations, becomes

algorithm
n, x, y := 0, 0, 0
while n < N do
    y := min(y + f(n), 0)
    x := min(x, y)
    n := n + 1

or, when replacing min with conditional statements and exploiting the additional invariant x ≤ 0:

algorithm
n, x, y := 0, 0, 0
while n < N do
    y := y + f(n)
    if y ≥ 0 then y := 0
    else if x > y then x := y
    n := n + 1

This program has a running time proportional to N.

Question: How would you implement the cubic and the linear version in your favourite programming language and time them with a "large" array?

In [ ]:
def minSegSumCubic(f):
    return min(sum(f[i:j]) for i in range(0, len(f) + 1) for j in range(i, len(f) + 1))

minSegSumCubic([1, 2, -3, 0, 2, -9, 7])
In [ ]:
#input is: 0, -2, 4, -6, 8, -10, 12, -14, ..., - 2 * 999
%time assert minSegSumCubic([2 * (-1) ** n * n for n in range(1000)]) == - 999 * 2
In [ ]:
def minSegSumLinear(f):
    n, x, y = 0, 0, 0
    for n in range(len(f)):
        y += f[n]
        if y >= 0: y = 0
        else:
            if x > y: x = y
    return x

minSegSumLinear([1, 2, -3, 0, 2, -9, 7])
In [ ]:
#input is: 0, -2, 4, -6, 8, -10, 12, -14, ..., - 2 * 999
%time assert minSegSumLinear([2 * (-1) ** n * n for n in range(1000)]) == - 999 * 2

Program Development: Printing Images

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 example also illustrates how to reason about program output.

The task is to print a picture given by the arrays fx, fy, where

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

That means with each input of i from 0 to N – 1, two functions fx(i) and fy(i) indicate each printed point.

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: 0 .. X – 1 × 0 .. Y – 1 → bool     // paper is a 2D array
var hx, hy: integer                                       // the position of the printer.
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:

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))}

where

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

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: 0 .. X – 1 × 0 .. Y – 1 → 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}

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: hy = y ∧ ∀ 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 < Y 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  ∧  hx = x ∧ (∀ 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: 0 .. X – 1 × 0 .. Y – 1 → bool      // image is a 2D array
    var x, y, n : integer

    y := 0
    while y < Y do        // clear the image
        x := 0
        while x < X do    // clear the image for each line
            image(x, y) := false ; x := x + 1
        y := y + 1

    n := 0
    while n < N do        // markdot to the image 
        image(fx(n), fy(n)) := true ; n := n + 1

    y := 0
    while y < N do        // print to the paper
        x := 0
        while x < X do    // print to the paper for each line
            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:

algorithm
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

</div>

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

</div>

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:

```algorithm a, b := x, y do a ≠ b → if a > b → a := a – b ⫿ a < b → b := b – a ```
```algorithm 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:

algorithm
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:

algorithm
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}

</div>

if P ⇒ Q

</div>

{P} if B → S ⫿ C → T {Q} </div>

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

</div>

{P} do B → S ⫿ C → T {Q} </div>

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

</div>

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} </div>

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

</div>

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.

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

Historic Notes and Further Reading

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.

Check Your Understanding

Exercise 1: Swapping Two Variables

Carry out the proof of the program for swapping two variables! The three conditions are:

  1. x = A ∧ y = B ⇒ (x - y = A ∧ y = B)[x := x + y]
  2. x - y = A ∧ y = B ⇒ (y = A ∧ x - y = B)[y := x - y]
  3. y = A ∧ x - y = B ⇒ (y = A ∧ x = B)[x := x - y]

References