CSSE 373 Formal Methods in Specification and Design

HW9

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. 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 \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. 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 lt <= rt && rt < a.length;
      //@ assignable a[lt..rt];
      //@ ensures a[rt] == (\max int k; lt <= k && k <= rt; a[k]);
      public void bubble(int[] a, int lt, int rt) {
        int i = lt;
          /*@ 
            @ maintaining a[i] == (\max int k; lt <= k && k <= i; a[k]);
            @ maintaining i <= rt;
            @ decreasing -i;
            @*/
        while (i < rt) {
          if(a[i] > a[i+1]) {
            exchange(a, i, i+1);
          }
          i = i + 1;
        }
      }
      
      
      
      

   4. Argue why the bubble method is totally correct. That is, explain how we know that the bubble method terminates. (You may assume that the exchange method is totally correct.)

   5. 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]);
        
        
        
        
      

   6. Prove that the fact method meets its specification. (Note that, by definition, in JML a \product expression with an empty range has the value 1.)

      //@ requires n >= 0;
      //@ assignable \nothing;
      //@ ensures \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;
      }
        
        
        
        
      

   7. Argue why the fact method is totally correct. That is, explain how we know that the fact method terminates when called with an argument that satisfies its precondition.
3. Record the amount of time you spent on this assignment in your answers file.
4. Turn in your work by committing a pdf file to the appropriate HW folder in your homework team subversion repository for this course.