CSSE 373 Formal Methods in Specification and Design

HW9

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. Please note: You should have at least one assert clause between every line of code.

   Assume the following methods with specifications as given:

   //@ requires l <= r && r < a.length;
   //@ assignable a[l..r];
   //@ ensures a[r] == (\max int k; l <= k && k <= r; a[k]);
   public void bubble(int[] a, int l, int r);
   
   
   //@ requires i <= j && j < a.length;
   //@ assignable a[i], a[j];
   //@ ensures a[i] == \old(a[j]) && a[j] == \old(a[i]);
   public void exchange(int[] a, int i, int j);
   
   
   //@ requires n >= 0;
   //@ assignable \nothing;
   //@ ensures (n == 0 ==> \result == 1) 
   //@         && (n > 0 ==> \result == (\product int k; 1 <= k && k <= n; k)); 
   public int fact(n);
   
   
   

   1. Show the result of applying the substitution rule to the specification of fact for the following call:

        //@ assert ____________________________
      x = fact(y);
        //@ assert ____________________________
        
        
        
      

   2. Show the result of applying the substitution rule to the specification of fact for the call below. Simplify the post-condition of the call. (For this problem, you do not need to simplify completely. That is, you can leave a “call” to fact in your post-condition. Just eliminate the parts of the original post-condition that are vacuously true.) Show your work.

        //@ assert ____________________________
      x = fact(5);
        //@ assert ____________________________
      
      
      
      

   3. Prove that the bubble method meets its specification. You may assume that the exchange method meets its specification.

      //@ requires l <= r && r < a.length;
      //@ assignable a[l..r];
      //@ ensures a[r] == (\max int k; l <= k && k <= r; a[k]);
      public void bubble(int[] a, int l, int r) {
        int i = l;
          /*@ 
            @ maintaining a[i] == (\max int k; l <= k && k <= i; a[k]);
            @ maintaining i <= r;
            @ decreasing -i;
            @*/
        while (i < r) {
          if(a[i] > a[i+1]) {
            exchange(a, i, i+1);
          }
          i = i + 1;
        }
      }
      
      
      
      

   4. Prove that the following program meets its specification:

        //@ assert 1 <= a.length;
      i = a.length - 1;
        /*@
          @ maintaining i >= 0;
          @ maintaining (\forall int k; i < k && k < a.length; a[k-1] <= a[k]);
          @ maintaining (\forall int j; 0 <= j && j <= i; 
          @                      a[j] <= (\min int k; i < k && k < a.length; a[k]));
          @ decreasing i;
          @*/
      while (i > 0) {
        bubble(a, 0, i);
        i = i - 1;
      }
        //@ assert (\forall int k; 0 < k && k < a.length; a[k-1] <= a[k]);
        
        
        
        
      

   5. Prove that the fact method meets its specification:

      //@ requires n >= 0;
      //@ assignable \nothing;
      //@ ensures (n == 0 ==> \result == 1) 
      //@         && (n > 0 ==> \result == (\product int k; 1 <= k && k <= n; k)); 
      public int fact(n) {
        int r = 0;
        if (n == 0) {
          r = 1;
        } else {
          r = fact(n - 1);
          r = r * n;
        }
        return r;
      }
        
        
        
        
      

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