20210902

Page 1

Ingegneria del Software — Soluzione del Tema 2/09/2021 Esercizio 1 Si consideri la seguente classe Java PhotoLibrary per la gestione di una collezione di foto. Ogni foto `e rappresentata dalla classe immutabile Photo che contiene alcune informazioni tra cui l’insieme delle persone (classe immutabile Person) che appaiono nella foto. public class PhotoLibrary { // Ritorna il numero di foto contenute nella collezione. public /*@ pure @ */ int size(); // Ritorna l’i-esima foto contenuta nella collezione (in ordine di inserimento). public /*@ pure @ */ Photo get( int i); // Aggiunge una foto alla collezione. // Lancia una DuplicateException se la foto e’ gia’ presente nella collezione. public void add(Photo photo) throws DuplicateException; // Ritorna le foto che contengono tutte le persone in s. // s deve contenere almeno una persona. public /*@ pure @ */ Set<Photo> getPhotosWith(Set<Person> s); // Ritorna la lista di tutte le persone contenute in foto della collezione. La lista e’ // ordinata dalla persona che appare in piu’ foto alla persona che appare in meno foto // (in caso di uguale numero di apparizioni, l’ordine non e’ specificato). public /*@ pure @ */ List<Person> getAllPeople(); } public /*@ pure @ */ class Photo { // Ritorna l’insieme di persone contenute nella foto (puo’ essere vuoto). public Set<Person> getPeople(); ... } Domanda a) Si specifichino in JML i metodi add, getPhotosWith, getAllPeople. Soluzione //@requires photo != null //@ //@ensures (\forall int i; i>=0 && i<\old(size()); !\old(get(i)).equals(photo)) && //@ size() == \old(size())+1 && get(size()-1).equals(photo) && //@ (\forall int i; i>=0 && i<\old(size()); \old(get(i)).equals(get(i))) //@ //@signals (DuplicateException e) //@ (\exists int i; i>=0 && i<\old(size()); \old(get(i)).equals(photo))…