CSSE 373 -- Formal Methods in Specification and Design

                               Quiz 15


Name:_________________________________________    Grade:______________



1. 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:



























(continued on back)


2. 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(                                     );


3. Suppose that you are given the following specification for the
   procedure smaller:

		//@ requires a > 0;
		//@ assignable \nothing;
		//@ ensures \result < a;
		int smaller(int a);

   Prove that the implementation below agrees with its specification. 

		int smaller(int a) {
		
				//@ assert
		
			if (a == 1)  {
		
					//@ assert
		
					//@ assert
		
				r = 0;
		
					//@ assert
		
			} else {
		
					//@ assert
		
					//@ assert
		
					//@ assert
		
					//@ assert
		
				r = smaller(a - 1);
		
					//@ assert
		
					//@ assert
		
			}
		
				//@ assert
		
			return r;
		
		}