CSSE 373 -- Formal Methods in Specification and Design

                                Quiz 8



Name:_________________________________________    Grade:______________


1. List your project teammates AND your team name (up to 3 person teams):








2. Mark up the following function and fact to use the OO-like notation:

		
		fun teaches[p: Prof]: set Course {
		
			p.~taughtBy
		
		}
		
		
		fact MaxPreps {
		
			all p: Prof | #teaches[p] <= 3
		
		}



3. In the traffic light example, what sort of assertion--mundane or
   essential--is Safe?





4. Which paragraph kind (fact, assertion, predicate, function) would be
   best for each of these scenarios?

   a. Specifying the number of floors that an elevator can visit
   
   
   
   b. Specifying that an elevator doesn't change direction until all
      requests in that direction are serviced
      
      
      
   c. Getting the set of requested floors for a particular elevator car
   
   
   
   d. Verifying that an elevator visits the floors in order
   
   
   

(continued on back)




5. In the command
		
		run show for exactly 3 Directory, exactly 3 Alias, 5 File
	
   how many total objects would be generated if we added "exactly"
   before "5 File"?  (Careful.  Alias and File are related.)