CSSE 373 -- Formal Methods in Specification and Design

                                Quiz 4



Name:_______________________________________ Grade:______________


"Prof" Alloy model referred to in some questions:

	sig Prof { inDept: set Dept }
	sig Dept {}
	sig Course { taughtBy: some Prof }
	
	fact {
		all p: Prof | some p.inDept
	}
	
	pred show[] {
		#Prof = 3
		#Dept = 2
		#Course = 0
	}
	
	run show for 4 but 2 Dept
	
	
	
	

1. Complete the value for univ based on the Prof model above.  (Note
   that the show predicate gives precise bounds on the number of Profs, Depts, and Courses.)

	univ = {-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7, 
	
			_________, _________, _________, _________, ________ }






2. Complete the value for iden based on the Prof model above.  (Note
   that the show predicate gives precise bounds on the number of Profs
   and Depts.)

	iden = {-8 -> -8, -7 -> -7, -6 -> -6, -5 -> -5, -4 -> -4, -3 -> -3, 
			-2 -> -2, -1 -> -1, 0 -> 0, 1 -> 1, 2 -> 2, 3 -> 3, 4 -> 4, 
			5 -> 5, 6 -> 6, 7 -> 7, 
	
			__________________, __________________, __________________,
			
			
			__________________, _________________ }





(continued on back)










3. Give the values of the following Alloy expressions, assuming:

	inDept = {Prof$0->Dept$0, Prof$0->Dept$1, Prof$1->Dept$1, Prof$2->Dept$0}
	
	r1 = {Prof$0->Dept$0, Prof$0->Dept$1}
	
	r2 = {Prof$0->Dept$1, Prof$1->Dept$1}

		a. r1 + r2 = ____________________________________________
		
		b. r1 & r2 = ____________________________________________
		
		c. r1 in inDept = _________
		
		d. Prof$0 -> Dept$1 in inDept = __________
	


4. Based on the constraints given in the Prof model, what is the size of
   the relation Prof -> Dept ?
   
   									_______
   									
   									
5.	a. {(C0,P0)} . {(P0,D0)} = ______________

	b. {(C0,P0)} . {(P1,D0)} = ______________
	

6. Suppose you wanted to form a relation consisting of courses and the
   departments of the professors that taught them.  How would you write
   that in Alloy?
	
	


7. Assuming inDept = {P0->D0, P0->D1, P1->D1, P2->D0}
	
	
   what is ~inDept? ______________________________________________________
	

8. Describe (in English) an operation on the Prof model that might be
   defined using the override (++) operator.  (Hint: taughtBy is a
   binary relation.)