CSSE 373 -- Formal Methods in Specification and Design

                                Quiz 5



Name:_________________________________________    Grade:______________


1. Is the relation {a->b, c->d, b->c} transitive? ______ Why or why not? 









2. Is the relation {a->b, c->d, c->b} transitive? ______ Why or why not? 










3. Give the transitive closure of r={a->c, c->b, b->d}


	^r = ___________________________________________________________
	
	
	
	
	
	

Consider the following Alloy model:

sig Prof { dept: set Dept }
sig Dept { }
sig Course {
	taughtBy: some Prof,
	ownedBy: lone Dept
}

4. What constraint would we write to say that if the course is taught by
   a single prof, then the course is owned by that prof's department,
   otherwise the course doesn't have an owner

	all c: Course | 
		#c.taughtBy = 1 => ___________________________________________________





(continued on back)








5. Given address = {N0->A0, N1->N0, N1->N2, N2->A1, N2->A2}, say whether
   or not each of the following (separate) constraints hold:

   (a) some n: Name, a: Address | a in n.address
   
   
   
   
   (b) no n: Name | n in n.^address
   
   
   
   
   (c) all n: Name | lone d: Address | d in n.address
   
   
   
   
   (d) all n: Name | no disj d, d': Address | d + d' in n.address
   
   
   
   
   
   

6. What's a more concise way to say that a name maps to at most one
   address?







7. Give a declaration for a formal parameter, faculty, mapping
   departments to professors.

	faculty: ________________________________________
	
	
	
	
8. Rewrite (below) your declaration from the previous question to say that every
   department has at least one professor.

	faculty: ________________________________________