Question

Problem 6 (20% total).  Show your work step by step to receive full credit.

Q1) (5%) Suppose {Z > Y} is the post-condition of the assignment statement

        shown below.   Compute the weakest precondition for this statement:   

                       Z = X - 2*Y -10;

Q2) (7%) Compute the weakest precondition for the following sequence

        of assignment statements and its post-condition:

p = q - 3;           
k = p * 3 + 6;  
{Q: k <= 12}

Q3) (8%) Compute the weakest precondition for the following selection

       construct and its post-condition

        if  (x < y)  y = 2 *  x - 4;        
        else  y = 2 * x + 4;                  
        {Q: y <  10} 

Answer 1