CSSE 373 -- Formal Methods in Specification and Design

                               Quiz 13


Name:_________________________________________    Grade:______________


1. Below is a partially complete proof of partial correctness for a program
   fragment.  Fill in the blanks according to the rule for while loops.
   (You do not have to complete the rest of the proof.)

		//@ assert lo == 0;
		//@ assert lo == 0 && 0 <= a.length && 0 == a.length - a.length;
		//@ assert lo - 1 <= a.length && 0 == a.length - (a.length - lo);
	hi = a.length;
		//@ assert lo - 1 <= hi && 0 == a.length - (hi - lo);
	c = 0;
		/*@ maintaining lo - 1 <= hi;
		  @ maintaining c == a.length - (hi - lo);
		  @ decreasing hi - lo;
		  @*/



		//@ assert ___________________________________________________________

	while (lo < hi) {



			//@ assert ________________________________________________________


			//@ assert (omitted for quiz)
		lo = lo + 1;
			//@ assert (omitted for quiz)
		hi = hi - 1;
			//@ assert (omitted for quiz)
		c = c + 2;


			//@ assert ________________________________________________________

	}



		//@ assert ___________________________________________________________

		//@ assert (omitted for quiz)
		//@ assert c >= a.length;

2. Argue why the program in question 1 terminates (i.e., is totally correct).









(continued on back)




3. WhatÕs _the value_ of the following JML expression and _why_:

	(\forall int i; 0 < i && i < 1; false)




4. In English, what does the following mean:

	(\forall int j; 0 <= j && j <= i; 
             a[j] <= (\min int k; i < k && k < a.length; a[k]))
                          
             
             
             

5. Find the weakest precondition for the following program. Be sure to
   show all intermediate steps. That is, fill in the blanks with correct
   assertions.  To save some writing, the loop invariant has been copied to 
   the appropriate places already.


		//@ assert 


		//@ assert 


		//@ assert 
	x = 0;


		//@ assert 
	a = 0;
		/*@ maintaining x == (\sum int i; 0 <= i && i <= a; i);
		  @ maintaining a <= n;
		  @ decreasing -a;
		  @*/
		//@ assert x == (\sum int i; 0 <= i && i <= a; i) && a <= n;
	while (a < n) {
			//@ assert x == (\sum int i; 0 <= i && i <= a; i) && a <= n && a < n;


			//@ assert 


			//@ assert 
		a = a + 1;


			//@ assert 
		x = x + a;
			//@ assert x == (\sum int i; 0 <= i && i <= a; i) && a <= n;
	}

		//@ assert x == (\sum int i; 0 <= i && i <= a; i) && a <= n && a >= n;
		//@ assert x == (\sum int i; 0 <= i && i <= a; i) && a == n;
		//@ assert x == (\sum int i; 0 <= i && i <= n; i);