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 should 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. 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.)