Lecture Notes for Algorithm Design

Statements, 30 November 1999

1. overview - state transformers

   1. going from the initial state to the final state

   2. statements as state transformers

   3. each statement is a small program with initial and final states

2. assignment statements

   1. working forward - establish a truth in the initial state and use the assignment to establish it

      1. {a[0..i + 1] <= n} i <- i + 1 {a[0..i] <= n}

   2. work backward from the final to initial state

      1. {P[x <- E]} x <- E {P}

3. choice statements

   1. Find S to establish

      {x = X and y = Y}
      S
      {x = X and y = Y and (z = X or Z = Y) and z >= X and z >= Y}

   2. there are two cases to consider:

      1. X >= Y, in which case

         {x = X and y = Y and X >= Y}
         z <- x
         {x = X and y = Y and (z = X or z = Y) and z >= X and z >= Y}

         does the trick

      2. X <= Y, in which case

         {x = X and y = Y and X < Y}
         z <- y
         {x = X and y = Y and (z = X or z = Y) and z >= X and z >= Y}

         does the trick

   3. but which case holds on any particular execution?

      1. The alternative (or choice or if) statement:

         {x = X and y = Y}
         if x >= y
           {x = X and y = Y and X >= Y}
           z <- x
           {x = X and y = Y and (z = X or z = Y) and z >= X and z >= Y}
         else
           {x = X and y = Y and X < Y}
           z <- y
           {x = X and y = Y and (z = X or z = Y) and z >= X and z >= Y}
         fi
         

      2. In general

         { I }
         if B
           { I and B}
           S1
           { F }
         else
           { I and not B}
           S2
           { F }
         fi
         { F }
         

      3. eliminate the else if P and not B can establish Q

4. repetitive statements

   1. In general

      { I }
      do B
        { I and B}
        S
        { I }
      od
      { I and not B }
      { F }
      

   2. partial correctness - no termination

   3. termination function - a function decreasing on every iteration

   4. creating the invariant

      1. the tip-off is a for-all statement in the final state

      2. create the invariant by weakening the final state

      3. the do guard becomes the part removed from the final state to get the invariant

      4. example

         1. given predicate B(), find the smallest natural number x such that B(x) is true.

         2. the initial state is true

         3. the final state is for all i such that 0 <= i < x : not B(i) and B(x)

         4. one way to weaken the final state is to drop part of it; the dropped part becomes the guard to the do.

5. sequencing statements

   1. { I1 } S1 { F1 } ; { I2 } S2 { F2 }

   2. the relation between F1 and I2

      1. simple - F1 = I2

      2. more complicated - manipulate F1 to I2; stronger and weaker states

   3. working backward, working forward, inside out, from both ends in

   4. for example, swap

      { x = X and y = Y } S { x = Y and y = X }

This page last modified on 14 December 1999.