(1st) pages 40-41 (Section 2.4.3), pages 134-136 (Section 4.4), pages 162-163 (Section 5.3.1)

(2nd) pages 108-109 (Section 3.4.3), pages 211-214 (Section 5.4), pages 249-250 (Section 6.3.3)

Pre- and postconditions are predicates. Both tell us something about the
values of the variables of our programs. For example, `n = 1' and
`list is nonempty' are such predicates. We use

{ P } S { Q }

to specify that

if the variables have values such that the predicate
P is satisfied at the start of the execution of
statement S

and the execution of the statement S terminates

then at termination the variables have values such that the predicate
Q is satisfied.

For example,

{ n = 0 } n = n + 1; { n = 1 }

and

{ true } list.insertLast("x");
{ list is nonempty }

A loop invariant is also a predicate. It tells us something about the
values of the variables while executing a loop. This predicate should be
satisfied at the beginning of every iteration of the loop. Consider the
loop

**while** B **do** S

with loop invariant LI. If

{ LI B }
S { LI },

that is, statement S preserves the loop invariant LI
within the loop, then we can conclude that

{ LI } **while** B **do** S
{ LI
B },

that is, if the loop invariant LI is satisfied at
the start of the execution of the loop and the loop terminates then the
loop invariant LI (and of course also
B) is satisfied at termination.

**Bubble-sort**

**Algorithm** bubbleSort(*sequence*):

*Input:* sequence of integers *sequence*

*Postcondition:* *sequence* is sorted and
contains the same integers as the original sequence

*length* length of *sequence*

**for** *i* 0 **to** *length* - 1
**do**

**for** *j* 0 **to** *length* -
*i* - 2 **do**

**if** *j*th element of *sequence* > (*j*+1)th element of
*sequence* **then**

swap *j*th and (*j*+1)th element of *sequence*

A loop invariant for the outer loop is:
the last *i* elements of *sequence* are sorted and are all greater
than or equal to the other elements of *sequence*.
A loop invariant for the inner loop is:
the last *i* elements of *sequence* are sorted and are all greater
than or equal to the other elements of *sequence* and the *j*th
element of *sequence* is greater than or equal to the first *j*
elements of *sequence*.

Proof of Proposition 5.9 and 5.10/ Proposition 6.10 and 6.11 in PostScript and PDF.

**Variant function**

Before we can reason inductively about recursive algorithms, we need to
prove that the algorithm terminates. To show that there is no infinite
recursion without tracing through the actual computation, we
introduce a *variant function*. This function maps each instance of the
parameters satisfying the precondition to a natural number. That is, it
is a function from instances to natural numbers. Consider for example

**Algorithm** factorial(*n*):

*Input:* integer

*Output:* *n*!

*Precondition:* *n* > 0

**if** *n* = 1 **then**

**return** 1

**else**

**return** *n* * factorial(*n* - 1)

The variant function *variant* has to map each instance of the
parameters satisfying the precondition, in this example a positive integer,
to a natural number. This natural number can be thought of as an upperbound of
the number of recursive calls this instance gives rise to. For example,
factorial(*n*) gives rise to *n* - 1 recursive calls.

To prove that a recursive algorithm does not lead to infinite recursion, it is
enough to find a variant function *variant* with the following two
properties:

*variant*maps instances of the base case(s) to 0.*variant*maps (the instances of) recursive calls to a smaller number than (the instance of) original call.

*variant*(1) = 0.*variant*(*n*- 1) <*variant*(*n*).

Let us have a look at another example. Consider the following algorithm.

**Algorithm** numberOfNodes(*node*):

*Input:* node of a binary tree

*Output:* number of nodes of the subtree
rooted at *node*

**if** *node* is a leaf **then**

**return** 1

**else**

**return** numberOfNodes(left child of *node*) +
numberOfNodes(right child of *node*) + 1

In this example, the instances of the parameters are nodes of a binary tree.
The variant function *variant* has to satisfy

*variant*(*node*) = 0 if*node*is a leaf and*variant*(left child of*node*) <*variant*(*node*) and*variant*(right child of*node*) <*variant*(*node*) if*node*is not a leaf.

Now consider the following algorithm.

**Algorithm** f(*n*):

*Input:* integer

*Output:* 1

*Precondition:* *n* > 0

**if** *n* = 1 **then**

**return** 1

**else**

**return** f(*n* + 1)

Again the instances are positive integers. In this case, the variant function
*variant* should satisfy

*variant*(1) = 0.*variant*(*n*+ 1) <*variant*(*n*).