17 01 14

Page 1

Dipartimento di Elettronica e Informazione Politecnico di Milano prof. Elisabetta Di Nitto, Raffaela Mirandola, Luca Mottola 20133 Milano (Italia) Piazza Leonardo da Vinci, 32 Tel. (39) 02-2399.3400 Fax (39) 02-2399.3411 Software Engineering II 17 January 2014 Last Name First Name Id number (Matricola) Note 1. The exam is not valid if you don’t fill in the above data. 2. Write your answers on these pages. Extra sheets will be ignored. You may use a pencil. 3. The use of any electronic apparatus (computer, cell phone, camera, etc.) is strictly forbidden. 4. You cannot keep a copy of the exam when you leave the room. 2 Question 1 Alloy (7 points) Specify in Alloy the following informal statements: 1. A person can have several friends (who are also persons). The friendship relationship is symmetric (that is, if A is a friend of B then B is a friend of A). 2. A function "linked to" can be defined from the friendship relation. The function yields the set of direct or indirect friends of a given person P. That is, it contains all the persons Q such that either Q is a friend of P or Q is a friend of a friend of P or Q is a friend of a friend of ... a friend of P. 3. The predicate unrelated (X, Y), where X and Y are persons, is true when the set of persons linked to X and the set of persons linked to Y are disjoint. 4. The predicate linkedButNotFriend (X, Y), where X and Y are persons, is true if X and Y are not direct friends but they are linked. 5. A couple is composed of exactly two distinct persons. 6. No bigamy is allowed (each person should belong to at most one couple). 7. The predicate coupleButUnrelated(X, Y), where X and Y are persons, is true if X and Y are a couple but they are unrelated. Solution sig Person { friends: set Person } sig Couple { partner1: one…