CSSE 373 Formal Methods in Specification and Design

HW8

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

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