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 should have at least one assert clause between every line of code. That level or 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. Turn in your work by committing a pdf file to the appropriate HW folder in your individual subversion repository for this course.
4. Please complete the short, anonymous survey on ANGEL regarding this assignment. (I will study these surveys in detail after the conclusion of this offering of the course. If you have suggestions that you would like me to consider during this offering of the course, please tell me in person or use the separate Anonymous Suggestion Box on ANGEL.)