Reading material

If you use the first edition of the textbook, follow the reading material in orange. If you use the second edition, follow the reading material in brown.

(1st) pages 32-35 (Section 2.2), pages 40-41 (Section 2.4.3), pages 134-136 (Section 4.4)

(2nd) pages 100-103 (Section 3.2), pages 108-109 (Section 3.4.3), pages 211-214 (Section 5.4)

Additional material

List

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 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 jth element of sequence > (j+1)th element of sequence then
             swap jth 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 jth element of sequence is greater than or equal to the first j elements of sequence.

Question

Consider

Algorithm Factorial(n):
   Precondition: n > 0
   Input: integer n
   Output: factorial of n
if n = 1 then
     return 1
else
     return n * Factorial(n - 1)

Why does Factorial(3) terminate? How is Factorial(3) computed?