CSSE 373 -- Formal Methods in Specification and Design

                                Quiz 9



Name:_________________________________________    Grade:______________


1. Why does Alloy's int[] operator (for converting from Int atoms to
   integer values) return a sum?






2. Rewrite the Alloy model below to not use a Boolean type.

	sig Lift {
		goingUp: Time -> Boolean,
		goingDown: Time -> Boolean
	} 











3. What's the difference between the "solution" that Alloy looks for
   when running a predicate vs. checking an assertion.








4. What three things could cause a theorem prover to fail to prove an
   assertion?
   
   
	*
	
	
	
	
	*
	
	
	
	
	*
	
	
	
	
(continued on back)





5. Why does Alloy use instance finding instead of automatic theorem
   proving?	













6. What is the conclusion we can draw from the Small Scope Hypothesis?










7. Jackson writes, "Software, unlike hardware, rarely fails because of a
   single tiny but debilitating flaw.  In almost all cases, software
   fails because of poor abstractions that lead to a proliferation of
   bugs, one of which happens to cause the failure."

   Do you tend to agree with this claim?  Why or why not?