20220826

Page 1

Ingegneria del Software — Soluzione del Tema 26/08/2022 Esercizio 1 Si consideri la seguente classe SeriesStore per memorizzare episodi di serie TV . Gli episodi sono rappresentati dalla classe immutabile Episode che espone tra gli altri un metodo per ottenere la serie di appartenenza di un episodio. public class SeriesStore { // Ritorna il primo episodio della serie passata per parametro. // Ritorna null se la serie non esiste. public /*@ pure @ */ Episode getFirstEpisode(String series); // Ritorna l’episodio successivo a quello passato per parametro. // Ritorna null se tale episodio non esiste, ovvero se quello passato per parametro // e’ l’ultimo della serie. public /*@ pure @ */ Episode getNextEpisode(Episode ep); // Ritorna il numero di episodi della serie successivi a quello passato per parametro. // Ritorna 0 se la serie non esiste. public /*@ pure @ */ int numNextEpisodes(Episode ep); // Aggiunge l’episodio in fondo alla sua serie di appartenenza. Se la serie ancora // non esiste, l’episodio viene aggiunto come il primo di quella serie. // Lancia una IllegalEpisodeException se l’episodio passato come parametro e’ null. public void addEpisode(Episode ep) throws IllegalEpisodeException; } public /*@ pure @ */ Episode { // Ritorna la seria di appartenenza dell’episodio. public /*@ pure @ */ String getSeries(); ... } Domanda a) Specificare in JML il metodo numNextEpisodes. Soluzione //@ requires ep != null //@ //@ ensures \result == (getNextEpisode(ep) == null) ? 0 : 1+numNextEpisodes(getNextEpisode(ep)) public /*@ pure @ */ int numNextEpisodes(Episode ep); Domanda b) Specificare in JML il metodo addEpisode. Soluzione Definiamo addEpisode solo a partire da getFirstEpisode e getNextEpisode in quanto numNextEpisodes deriva da questi. //@ ensures ep != null && //@ //@…