We use an algorithmic notation that, compared to common programming languages
Programs consist of
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
.
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:
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:
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}
P ⇒ Q[x, y := E, F]
{P} S {Q}
and {Q} T {R}
{P ∧ B} S {Q}
and {P ∧ ¬B} T {Q}
{P ∧ B} S {Q}
and P ∧ ¬B ⇒ Q
{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
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>
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
E'
, a mathematical expression to what it evaluates, and its∆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}
P ⇒ ∆E ∧ ∆F ∧ Q[x, y := E', F']
{P} S {Q}
and {Q} T {R}
P ⇒ ∆B
and {P ∧ B'} S {Q}
and {P ∧ ¬B'} T {Q}
P ⇒ ∆B
and {P ∧ B'} S {Q}
and P ∧ ¬B' ⇒ Q
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
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)
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 N³
. 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 N³
, 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?
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])
#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
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])
#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
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 positionadvance
: move the print head one position to the rightprint
: print a dot and move one position to the rightThe 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}
S
do not occur in P
{P0} S {Q0}
and {P1} S {Q1}
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:
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:
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
.
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.
Carry out the proof of the program for swapping two variables! The three conditions are:
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]