CSci532 Programming Languages and Paradigms: Homework 4

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%)





  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%)








  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 }