CSSE 373 Formal Methods in Specification and Design

HW8

Purpose: practice using invariant-assertion style to prove programs correct

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. Prove that each of the following program fragments satisfy their pre- and post-conditions.

   Please note: You must have at least one assert clause between every line of code.

   1.   //@ assert true;
      i = b.length - 1;
      s = 0;
        //@ maintaining -1 <= i && i < b.length;
        //@ maintaining s == (\sum int k; i+1 <= k && k < b.length; b[k]);
        //@ decreasing i;
      while (i != -1) {
        s = s + b[i];
        i = i - 1;
      }
        //@ assert s == (\sum int k; 0 <= k && k < b.length; b[k]);
      
      
      
      

   2.   //@ assert true;
      i = 0;
        //@ maintaining 0 <= i && i <= b.length;
        //@ maintaining !(\exists int k; 0 <= k && k < i; x == b[k]);
        //@ decreasing -i;
      while ((i < b.length) && (x != b[i])) {
        i = i + 1;
      }
        /*@ assert (0 <= i && i < b.length && x == b[i]) ||
          @        (i == b.length && !(\exists int k; 0 <= k && k < b.length; x == b[k]));
          @*/
      
      
      

   3.   //@ assert 0 < b.length;
      i = 1;
      k = 0;
        //@ maintaining 0 < i && i <= b.length;
        //@ maintaining (\forall int j; 0 <= j && j < i; b[k] >= b[j]);
        //@ decreasing -i;
      while (i < b.length) {
        if (b[i] >= b[k]) {
          k = i;
        }
        i = i + 1;
      }
        //@ assert (\forall int j; 0 <= j && j < b.length; b[k] >= b[j]);
      
      
      

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.