20210713

Page 1

Ingegneria del Software — Soluzione del Tema 13/07/2021 Esercizio 1 Si consideri la seguente classe Java MusicLibrary per la gestione di una collezione di brani musicali. Ogni brano `e rap- presentato dalla classe immutabile Song che contiene alcune informazioni tra cui l’artista o gruppo musicale ( Artist) che esegue il brano e la data (Date) in cui il brano `e stato registrato, come riportato di seguito. public class MusicLibrary { // Ritorna l’insieme di artisti che eseguono almeno un brano nella collezione. public /*@ pure @ */ Set<Artist> getArtists(); // Ritorna la lista di brani eseguiti dall’artista artist. // Lancia una UnknownArtistException se la collezione non contiene brani di artist. public /*@ pure @ */ List<Song> getByArtist(Artist artist) throws UnknownArtistException; // Ritorna l’insieme dei brani eseguiti in data date. // Lancia una UnknownDateException se nessun brano della collezione e’ // stato composto in data date. public /*@ pure @ */ Set<Song> getByDate(Date date) throws UnknownDateException; // Aggiunge il brano alla collezione. public void addSong(Song s); } public /*@ pure @ */ class Song { // Ritorna l’artista o gruppo che esegue il brano public Artist getArtist(); // Ritorna la data di registrazione del brano public Date getDate(); } Domanda a) Si specifichi in JML il metodo getByDate(). Soluzione Definiamo getByDate() in funzione di getByArtist() e getArtists(). //@requires date != null //@ //@ensures \result != null && ! \result.isEmpty() && //@ (\forall Artist a; getArtists().contains(a); //@ (\forall Song s; getByArtist(a).contains(s); //@ \result.contains(s) <==> date.equals(s.getDate()))) && //@ (\forall Song s; \result.contains(s); //@ s.getDate().equals(date) && getArtists().contains(s.getArtist()) && //@…