11 02 11

Pagina 1

Dipartimento di Elettronica e Informazione Politecnico di Milano prof. Elisabetta Di Nitto e Raffaela Mirandola 20133 Milano (Italia) Piazza Leonardo da Vinci, 32 Tel. (39) 02-2399.3400 Fax (39) 02-2399.3411 Ingegneria del Software II 11 Febbraio 2011 Cognome Nome Matricola Note 1. La mancanza dei dati di cui sopra comporta l'annullamento dell’esame 2. Restituire solo queste pagine. Verranno ignorati fogli aggiuntivi. Si puo' scrivere con la matita. 3. È proibito l'uso di dispositivi elettronici (computers, calcolatrici, cellulari, macchine fotografiche). 4. Non si puo' tenere una copia del testo dell'esame quando si lascia l'aula. 2 Domanda 1 – Alloy (8 punti) A partire dalla signature sig Point {} di un punto geometrico, si definiscano le seguenti specifiche: 1) un Segmento; i.e., una coppia di punti 2) una Linea; i.e., una sequenza di segmenti connessi 3) un Poligono; i.e., una Linea chiusa 4) Assumendo che sia definito un predicato “intersect” per due segmenti, si definisca un predicato “linesIntersect” che controlli l’intersezione tra due linee. 5) Si definisca un’operazione “add” che a partire da una Linea e un Segmento produce una nuova Linea dove il Segmento viene aggiunto alla fine dell’ultimo segmento. L’ultimo punto dell’ultimo segmento della Linea deve coincidere con il primo punto del Segmento. Soluzione sig Point{} sig Segment { start: one Point, end: one Point }{start!=end} sig Line { startSeg: one Segment, endSeg: one Segment, intermediateSeg: set Segment } { no x: intermediateSeg | startSeg=x or endSeg=x one x: intermediateSeg | startSeg.end=x.start one x: intermediateSeg | endSeg.start=x.end no x: intermediateSeg | startSeg.start=x.end no x: intermediateSeg | endSeg.end=x.start all x: intermediateSeg | x.end = endSeg.start or one x1: intermediateSeg |…