20230828

Page 1

Ingegneria del Software — Soluzione del Tema 28/08/2023 Esercizio 1 Si consideri la seguente classeCityMap che memorizza i punti di interesse di una citt`a (Site), organizzati per tipo (ristoranti, hotel, musei, etc.). public class CityMap { // Ritorna l’insieme di tutti i punti di interesse memorizzati public /*@ pure @ */ Set<Site> getSites() { ... } // Aggiunge il punto di interesse passato per parametro public void addSite(Site site) { ... } // Ritorna tutti i punti di interesse del tipo passato per parametro, // ordinati per distanza crescente rispetto alla location loc indicata. // Lancia una NotFoundException se non esiste alcun punto di interesse del tipo indicato. public /*@ pure @ */ List<Site> getSitesByType(Type type, Location loc) throws NotFoundException { ... } // Ritorna i k punti di interesse piu’ vicini alla location loc indicata // (per semplicita’, si assuma che non possano esistere due punti equidistanti da loc). // Se i punti di interesse sono meno di k, vengono ritornati tutti. // La mappa ritornata contiene i punti di interesse come chiave e la loro distanza da loc come valore. public /*@ pure @ */ Map<Site, Double> getNearestSites( int k, Location loc) { ... } } public /*@ pure @ */ class Site { // Ritorna la posizione geografica del punto di interesse public Location getLocation() { ... } // Ritorna il tipo del punto di interesse (ristorante, hotel, museo, ...) public Type getType() { ...} ... } public /*@ pure @ */ class Location { // Calcola la distanza rispetto alla Location passata per parametro public double getDistance(Location other) { ... } ... } Domanda a) Si specifichi in JML il metodo getSitesByType. Soluzione //@ requires type!=null && loc!=null //@ //@ ensures (\exists Site s; getSites().contains(s); s.getType().equals(type)) &&…