CSSE 373 -- Formal Methods in Specification and Design

                               Quiz 14


Name:_________________________________________    Grade:______________


1. What is the JML expression to refer to the return value of a
   method?



2. Why do JML expression keywords begin with backslashes?





3. In JML, what's the opposite of /*@ pure @*/?




4. What are the basic steps in the basic pattern for reasoning about method 
   calls?
   
   *
   
   
   *
   
   
   *
   
   
   
5. Suppose Q is `x > y && y >= 0'.  What is Q[a/x, b/y]?





6. Suppose we have the following method specification:

		//@ requires true;
		//@ assignable \nothing;
		//@ ensures \result == x + y;
		int sum(int x, int y) {...}
   
   Fill in the pre- and post-conditions for the following call to sum:
   

   			//@ assert ___________________

   		r = sum(n, n);

   			//@ assert ___________________
   


(continued on back)







7. Find the weakest pre-condition for the following program fragment:

			//@ assert 
		
		
			//@ assert 
		
		
		c = sum(a, b);
		
		
			//@ assert 
			
			//@ assert c >= 10 && a <= 2;
		
		

8. Given the following method specification:

		//@ requires d > 0;
		//@ assignable a, b;
		//@ ensures \result >= a && \result >= b && a + b == \old(a) + \old(b);
		int shift(int d) {
			a = a + d;
			b = b - d;
			r = max(a, b);
			return r;
		}

   Give the first and last assertions needed to prove the method correct.
   (You do not need to complete the proof.)   
   
		
		
			//@ assert _____________________________________________________
		
		a = a + d;
		b = b - d;
		r = max(a, b);
		
		
			//@ assert _____________________________________________________
		
		return r;