20220207

Page 1

Ingegneria del Software — Soluzione del Tema 07/02/2022 Esercizio 1 Si consideri la classe JavaJobsDB per la gestione di domande e offerte di lavoro (classiJobRequest e JobOffer). public class JobsDB { // Ritorna l’elenco delle richieste salvate. public /*@ pure @ */ Set<JobRequest> getRequests(); // Ritorna l’elenco delle offerte salvate // in ordine cronologico dalla meno alla piu’ recente. public /*@ pure @ */ List<JobOffer> getOffers(); // Aggiunge una richiesta di lavoro. // Lancia una DuplicateException se la richiesta e’ gia’ presente. public void addRequest(JobRequest req) throws DuplicateException; // Aggiunge un’offerta di lavoro e ritorna l’insieme di tutte le richieste // di lavoro compatibili con l’offerta (senza rimuoverle) public Set<JobRequest> addOffer(JobOffer offer); // Ricerca un’offerta di lavoro compatibile con la richiesta req. // Se esiste almeno un’offerta di lavoro compatibile con la richiesta, // ritorna la prima offerta compatibile (meno recente) e la rimuove. // Altrimenti, ritorna null. public JobOffer getOffer(JobRequest req); } public /*@ pure @ */ class JobRequest { // Ritorna true se e solo se l’offerta e’ compatibile con la richiesta. public boolean matches(JobOffer offer); ... } Domanda a) Si specifichi in JML il metodo addOffer. Soluzione Definiamo unchangedRequests, unchangedOffers come segue. //@ unchangedRequests <==> (getRequests().size() == \old(getRequests()).size() && //@ getRequests().containsAll(\old(getRequests()) //@ //@ unchangedOffers <==> (getOffers().size() == \old(getOffers()).size() && //@ (\forall int i; i>=0 && i<getOffers().size(); //@ \old(getOffers()).get(i).equals(getOffers().get(i)) ) Possiamo ora definire addOffer come segue. //@requires offer != null //@ //@ensures unchangedRequests && //@…