CSSE 373 -- Formal Methods in Specification and Design

                               Quiz 17



Name:_________________________________________    Grade:______________


1. 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;
		
		}







(continued on back)



The rest quiz is intentionally sparse so you have time to follow along in
Eclipse without being distracted.  Feel free to use the extra space for
notes if that's helpful.





2. When do class invariants have to first be true for a given object?





3. After a class invariant is established, how long must it remain true?





4. What are the three basic steps for specifying a class?

	a)
	
	
	
	
	
	b)
	
	
	
	
	
	c)
	
	
	
	
	d) Profit