CSSE 373 Formal Methods in Specification and Design

HW7

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

This is a team homework assignment. All work must be done by the team members together. All team members should understand all work submitted. If you have concerns about your own understanding or that of your teammates, please let me know. I want everyone to learn all they can in this course!

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 homework team subversion repository for this course.