20220618

Page 1

Ingegneria del Software — Soluzione del Tema 18/06/2022 Esercizio 1 Si consideri la classe Java HotelDB per gestire la prenotazione di stanze di hotel. public class HotelDB { // Ritorna l’elenco di tutti gli hotel contenuti. public /*@ pure @ */ Set<Hotel> getHotels(); // Ritorna la lista di tutte le stanze che (i) possono ospitare almeno people persone, // (ii) si trovano vicino a location, (iii) sono libere il giorno day. // La lista e’ in ordine crescente di prezzo (dalla stanza meno costosa alla piu’ costosa). public /*@ pure @ */ List<Room> findRooms( int people, Location location, Day day); // Prenota la stanza room per il giorno day. // Solleva una AlreadyBookedException se la stanza non e’ disponibile il giorno specificato. public void book(Room room, Day day) throws AlreadyBookedException; } public class Hotel { // Ritorna tutte le stanze presenti nell’hotel. public /*@ pure @ */ Set<Room> getRooms(); // Ritorna true sse l’hotel e’ vicino a location. public /*@ pure @ */ boolean isCloseTo(Location location); } public class Room { // Ritorna true sse la stanza e’ disponibile il giorno day. public /*@ pure @ */ boolean isAvailable(Day day); // Ritorna il numero massimo di persone che la stanza puo’ ospitare. public /*@ pure @ */ int getMaxPeople(); // Ritorna il prezzo della stanza. public /*@ pure @ */ float getPrice(); // Permette di prenotare la stanza nel giorno precisato. // Richiede che la stanza non sia gia’ prenotata per lo stesso giorno. public void book(Day day); } Domanda a) Si specifichi in JML il metodo findRooms(). Soluzione //@ requires people > 0 && location != null && day != null //@ //@ ensures \result != null && //@ (\forall Room r; r != null; \result.contains(r) <==> ( //@ (\exists Hotel h; getHotels().contains(h) && h.isCloseTo(location);…