15 01 15

Pagina 1

Dipartimento di Elettronica, Informazione e Bioingegneria Politecnico di Milano Prof. Elisabetta Di Nitto, Raffaela Mirandola 20133 Milano (Italia) Piazza Leonardo da Vinci, 32 Tel. (39) 02-2399.3400 Fax (39) 02-2399.3411 Software Engineering II January 15th 2015 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. You can use textbooks, slides and your notes 4. The use of any electronic apparatus (computer, cell phone, camera, etc.) is strictly forbidden. 5. You cannot keep a copy of the exam when you leave the room. 6. The exam should finish at 10.05 2 General note about the solutions The solutions given here are not the only ones possible. You can think of many others that fulfill the request of the exercises. In the case of the function points calculation we have been considering the minimum set of functions/data structures based on the given text. Question 1 Alloy (6 points) Consider the following fragment of an Alloy specification: sig Address {} sig Value {} sig Computer { memory: Address -> Value } 1. Formalize in Alloy the following invariant: in each computer, exactly one value is associated to each memory cell. 2. Modify the above invariant to represent also computers in which memory cells can be uninitialized. 3. Define in Alloy the writeMemory operation that, given a computer cell address, associates to it a new value, replacing the pre-existing one (if any). Solution 1. It is enough to change the Computer signature as follows: sig Computer { memory: Address -> one Value } 2. It is enough to change the Computer signature as follows: sig Computer { memory: Address -> lone Value } 3. pred writeMemory[c:…