CSSE 373 Formal Methods in Specification and Design

HW7

Purpose: practice using invariant-assertion style to reason about program fragments

1. Keep track of how much time you spend on this assignment. You will submit your answers as a pdf file at the end of the homework.

2. For each of the following program fragments, calculate the weakest pre-condition of the statement, given the post-condition.

   Please note: You must have at least one assert clause between every line of code. That level of rigor will be necessary for the more complicated problems to come.

   1.   //@ assert ____________________________;
      x = 2*y + 3;
        //@ assert x == 13;
      
      
      

   2.   //@ assert ____________________________;
      x = x + y;
        //@ assert x < 2*y;
      
      
      

   3.   //@ assert ____________________________;
      j = j + 1;
        //@ assert j > 0;
      
      
      

   4.   //@ assert ____________________________;
      i = i + 1;
        //@ assert i <= n;
      
      
      

   5.   //@ assert ____________________________;
      a = a - b;
        //@ assert a > b;
      
      
      

   6.   //@ assert ____________________________;
      x = z - 3;
      y = x * z;
        //@ assert y > 0;
      
      
      

   7.   //@ assert ____________________________;
      if (a > b) {
        a = a - b;
      } else {
        b = b - a;
      }
        //@ assert a > 0 && b > 0;
      
      
      

   8.   //@ assert ____________________________;
      if (i > 0) {
        a = i;
      }
        //@ assert a == Math.abs(i);
          
      
      

3. Record how much time you spent on this assignment.
4. Turn in your work by committing a pdf file to the appropriate HW folder in your individual subversion repository for this course.