CSSE 373 -- Formal Methods in Specification and Design

                               Quiz 16


Name:_________________________________________    Grade:______________



1. Assume the following method satisfies its specification:

		//@ requires n >= 0;
		//@ assignable \nothing;
		//@ ensures \result == (\product int k; 1 <= k && k <= n; k); 
		public int fact(n);

	Find weakest pre-condition:

		//@ assert __________________________________;








	g = g * 2;




	r = fact(g);




		//@ assert r >= 120;


























(continued on back)



2. Assume the following method satisfies its specification:

		//@ requires (\forall int k; 0 <= k && k < a.length; a[k] >= 0);
		//@ assignable \nothing;
		//@ ensures \result = (\sum int k; 0 <= k && k < a.length; a[k]);
		double sumAll(double[] a) { ... }

   Work in pairs to find the specification for the following method and prove it
   correct:

		//@ requires 
		
		
		
		//@ assignable
		
		//@ ensures
		
		
		
   
		void setAverageScore() {
			double s = sumAll(scores);
			avg = s / scores.length;
		}

   Proof of correctness:




















3. Suppose the specification for setRange allows it to assign to lo and
   hi.  Re-write the following statement to avoid the aliasing pitfall
   so that we can use our proof rules for reasoning about.  (You don't
   have to give any assertions.)
   
		setRange(lo + 100 - hi, 100);
		
   Re-write:
   
   
   
   
   		
   
   		setRange(                                     );