20230213

Page 1

Ingegneria del Software — Soluzione del Tema 13/02/2023 Esercizio 1 Si consideri la seguente classe Championship che memorizza i risultati di un campionato tra diversi Team. Si noti che il campionato distingue tra andata e ritorno di ogni partita. public class Championship { // Ritorna l’insieme dei team che fanno parte del campionato. public /*@ pure @ */ Set<Team> getTeams() {...} // Cancella tutti i risultati delle partite fin qui giocate. public void clear() {...} // Ritorna il team vincente nella partita giocata tra t1 (in casa) e t2 (fuori casa), oppure null // se non si e’ giocata nessuna partita tra t1 e t2 (t1 e t2 devono essere squadre del campionato). // Si noti che il valore restituito potrebbe non coincidere esattamente con t1 o t2, ma deve essere // uguale ("equals") a uno dei due. public /*@ pure @ */ Team winner(Team t1, Team t2) {...} // Inserisce il risultato della partita tra t1 (in casa) e t2 (fuori casa) con vincitore winner // (riguardo t1, t2 e winner valgono le stesse note indicate per il precedente metodo). // Solleva l’eccezione MatchAlreadyPlayedException se la partita e’ gia’ stata giocata. public void addMatch(Team t1, Team t2, Team winner) throws MatchAlreadyPlayedException {...} // Ritorna l’elenco dele squadre con cui la squadra t ha vinto giocando in casa. public /*@ pure @ */ List<Team> defeatedAtHome(Team t) {...} // Ritorna il punteggio accumulato dalla squadra t (la squadra vincente, in casa o fuori casa, // prende un punto). public /*@ pure @ */ int numPoints(Team t) {...} Domanda a) Specificare in JML il metodo addMatch. Soluzione //@requires t1!=null && t2!=null && getTeams().contains(t1) && //@ getTeams().contains(t2) && !t1.equals(t2) && (winner.equals(t1) || winner.equals(t2)) //@ensures \old(winner(t1,t2)==null) &&…