CSSE 373 -- Formal Methods in Specification and Design

                                Quiz 10



Name:_________________________________________    Grade:______________


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








2. What three things could cause a theorem prover to fail to prove an
   assertion?
   
   
	*
	
	
	
	
	*
	
	
	
	
	*
	
	
	
	
3. Why does Alloy use instance finding instead of automatic theorem
   proving?	













(continued on back)















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










5. 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?