#### Reading material

Pages 100-103 (Section 3.2),
pages 108-109 (Section 3.4.3),
pages 211-214 (Section 5.4)
#### Additional material

**Loop invariants**
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*.

#### Question

Complete the following *recursive* algorithm.

**Algorithm** fibonacci(*n*):

*Input:* integer

*Output:* *n*th Fibonacci number

*Precondition:* *n* >= 1