CSci532 Programming Languages and Paradigms: Homework 4 Solutions

Due date: Wednesday, November 19, 2008 in class
Each homework may have a different weight, which depends on its level of difficulty.
Absolutely no copying others' work

  1. Find wp( if x then x := x else x := 0 – x fi, x ≤ 0 ).     (25%)
    Ans> 
       wp( if  x  then  x := x  else  x := 0 – x  fi,  x ≤ 0 )
 = ( x > 0 → wp( x := x, x ≤ 0 ) and ( x ≤ 0 → wp( x := 0 – x, x ≤ 0 )
 = ( x > 0 → x ≤ 0 ) and ( x ≤ 0 → 0–x ≤ 0 )
 = ( ( x ≤ 0 ) or not ( x > 0 ) ) and ( ( 0–x ≤ 0 ) or not ( x ≤ 0 ) )
 = ( ( x ≤ 0 ) or ( x ≤ 0 ) ) and ( ( x ≥ 0 ) or ( x > 0 ) )
 = ( x ≤ 0 ) and ( x ≥ 0 )
 = ( x = 0 )
  2. Show using general properties of wp that wp(C, not Q) → not wp(C, Q) for any language construct C and any assertion Q.     (25%)
    Ans>
      Several ways can be used to prove this claim. Two of them are as follows.
    1. We know 
         wp( C, false ) = false
   wp( C, true  ) = true provided C terminates
      Implications can be proven to hold by constructing truth tables and showing that they are always true.

      Q wp( C, not Q ) not wp( C, Q ) wp(C, not Q) → not wp(C, Q)
      F T T T
      T F F T

      The rightmost column shows that wp(C, not Q) → not wp(C, Q) is always true. 
    2.    wp( C, not Q ) → not wp( C, Q )
 = ( not wp( C, Q ) ) or ( not wp( C, not Q ) )  // A → B = B or ( not A )
 = not ( wp( C, Q ) and wp( C, not Q ) )   // not (A and B) = (not A) or (not B)
 = not ( wp( C, Q and ( not Q ) ) )        // Distributivity of Conjunction
 = not ( wp( C, false ) )                  // Q and ( not Q ) = false
 = not ( false )                           // Law of the Excluded Miracle
 = true
  3. Show the correctness of the following program using axiomatic semantics:     (50%) 
         { n > 0 }
     i := n;
     fact := 1;
     while  i  do
       fact := fact * i;
       i := i – 1
     od
     { fact = 1 * 2 * … * n }
    Ans>
      A loop invariant W is 
       W = ( fact = (i+1) * … * n and i ≥ 0 )
    1. Proving the Condition (a): 
         W and i > 0 → wp( fact:=fact*i; i:=i–1, W )
         wp( fact:=fact*i; i:=i–1, W )
 = wp( fact:=fact*i; i:=i–1, fact=(i+1)*…*n and i≥0 )
 = wp( fact:=fact*i, wp( i:=i–1, fact=(i+1)*…*n and i≥0 ) )
 = wp( fact:=fact*i, fact=((i–1)+1)*…*n and i–1≥0 ) )
 = wp( fact:=fact*i, fact=i*…*n and i–1≥0 ) )
 = ( fact*i=i*…*n and i–1≥0 ) )
 = ( fact=(i+1)*…*n and i≥1 ) )
 = ( fact=(i+1)*…*n and i≥0 and i≥1 ) )
 = ( W and i≥1 )

   W and i > 0
 = ( fact=(i+1)*…*n and i≥0 and i>0 )
 = ( fact=(i+1)*…*n and i>0 )
 → ( fact=(i+1)*…*n and i≥0 and i≥1 )
 = ( W and i≥1 )
 = wp( fact:=fact*i; i:=i–1, W )
    2. Proving the Condition (b): 
         W and i ≤ 0 → { fact = 1 * 2 * … * n }
         W and i ≤ 0
 = ( fact = (i+1) * … * n and i ≥ 0 and i ≤ 0 )
 = ( fact = (i+1) * … * n and i = 0 )
 = ( fact = 1 * … * n and i = 0 )
 → ( fact = 1 * 2 * … * n )
    3. Proving the Condition (c):


        (Optional) We prove this part first: 
         { n > 0 }
   i := n;
   fact := 1
   { n > 0 and i = n and fact = 1 }
         wp( i:=n; fact:=1, n>0 and i=n and fact=1 )
 = wp( i:=n, wp( fact:=1, n>0 and i=n and fact=1 ) )
 = wp( i:=n, wp( fact:=1, n>0 ) and wp( fact:=1, i=n ) and
     wp( fact:=1, fact=1 ) )
 = wp( i:=n, wp( fact:=1, n>0 ) ) and wp( i:=n, wp( fact:=1, i=n ) ) and
     wp( i:=n, wp( fact:=1, fact=1 ) )
 = wp( i:=n, n > 0 ) and wp( i:=n, i=n ) and wp( i:=n, 1=1 )
 = ( n > 0 ) and ( n = n ) and ( 1 = 1 )
 = ( n > 0 ) and true and true
 = ( n > 0 )

      Prove the condition (c) 
         P → W
 = { n>0 and i=n and fact=1 } → { fact=(i+1)*…*n and i≥0 }
      by showing 
         { n>0 } → wp( i:=n; fact:=1, W )
         wp( i:=n; fact:=1, W )
 = wp( i:=n; fact:=1, fact=(i+1)*…*n and i≥0 )
 = wp( i:=n, wp( fact:=1, fact=(i+1)*…*n and i≥0 ) )
 = wp( i:=n, 1=(i+1)*…*n and i≥0 )
 = ( 1=(n+1)*…*n and n≥0 )
 = ( 1=1 and n≥0 )
 = ( n≥0 )
       n>0 → n≥0