CSSE 373 -- Formal Methods in Specification and Design

                                Quiz 7



Name:_________________________________________    Grade:______________


1. What is the arity of the weather relation declared below: _________

		sig Forecast { weather: City -> one Weather }
		sig City, Weather {}
		one sig Rainy, Sunny, Cloudy extends Weather {}






2. In the model below, what is the greatest number of Colors that a single

   light may show at a given Time? _________
   
		sig TrafficLight { color: Color some -> Time }
		abstract sig Color {}
		one sig Red, Green, Yellow extends Color {}
		sig Time {}






3. Suppose we didn't have the "disj" keyword on the declarations of
   daily, peculiar, and ineffable below.

		sig Cat { disj daily, peculiar, ineffable: Name }
		sig Name {}

   Write a constraint that says, for any particular cat, the three names
   are mutually disjoint.





4. Describe, in English, what is meant by the field declarations of
   RadioStation:

		sig RadioStation { 
		  owns: set Freq, 
		  freq: Location -> one owns 
		}
		sig Freq, Location {}









(continued on back)




5. What are the two purposes of types in Alloy?

	*
	
	
	*
	
	

6. Given the declarations:

		sig Object {}
		sig File, Directory extends Object {}
		sig Temp in Object {}

   indicate if each pair of basic types below overlaps:
   
   a. Object and File     	yes / no
   
   b. Object and Directory	yes / no
   
   c. File and Directory    yes / no
   

----------------------------------------------------------------
The next three questions refer to the following model:

		sig Prof { dept: set Dept }
		sig Adjunct in Prof {}
		sig Dept { }
		sig Course {
			taughtBy: some Prof,
		}

7. What are the basic types defined by the declarations?





8. What are the types of the fields defined by the declarations?


	a. dept ________________________________
	

	b. taughtBy ____________________________


9. What is the type of the expression 'Dept.~dept'? ____________________


----------------------------------------------------------------
10. How does Alloy resolve overloaded field names?