Capitolo sul JML

[m1gwings]

(WIP: ci sta già lavorando @m1gwings ) Paragrafi da scrivere:

• [ ] Sintassi (by @m1gwings )
  • [x] Condizioni
  • [x] Operatori booleani aggiuntivi
  • [x] Quantificatori
  • [x] Operatori di aggregazione
  • [x] \result
  • [x] assignable
  • [x] Commenti
  • [ ] ...
• [ ] Semantica
  • [ ] ...
  • [ ] Specifica ricorsiva
• [x] ADT
  • [x] Representation invariant
  • [x] Abstract function
  • [x] Metodi puri
• [ ] ...

[Furrrlo]

Li scrivo qui perché ho visto che li stai già scrivendo quindi magari ti servono:

• Inserire un elemento el di tipo T in un Set\:

  //@ ensures obsInd().contains(el) && 
  //@         (\forall T other; other != null && !other.equals(el); obsInd().contains(other) <==> \old(obsInd()).contains(other))

• Controllare che un Set\ non sia cambiato (serve nelle signals di metodi mutator):

  //@ ensures (\forall T el; el != null; obsInd().contains(el) <==> \old(obsInd().contains(el)))

• Inserire un elemento el di tipo T in una List\ (deve mantenere anche l'ordine):

  //@ ensures obsInd().size() == \old(size()) + 1 && 
  //@         obsInd().get(obsInd().size() - 1).equals(el) && 
  //@         (\forall int i; i >= 0 && i < \old(obsInd().size()); obsInd().get(i).equals(\old(obsInd().get(i)))

• Controllare che una List\ non sia cambiata:

  //@ ensures obsInd().size() == \old(size()) && 
  //@         (\forall int i; i >= 0 && i < obsInd().size(); obsInd().get(i).equals(\old(obsInd().get(i)))

[m1gwings]

Sì, grazie mille! Ci stavo lavorando proprio ora. Alcune "porzioni di specifica" ho cercato di scriverle per una Collection in generale in modo che siano riciclabili sia per i Set che per le List.

[Furrrlo]

Bisogna stare attenti che però le liste devono mantenere l'ordine, mentre i set no. Io non sono riuscito a farli generici 😭

[m1gwings]

Sí certamente. Infatti per alcune specifiche ho dovuto fare riferimento esplicitamente alle List o ai Set. Peró ad esempio quelle per l'inserimento o la rimozione di un elemento da una collezione le ho fatte anche generiche (perché a volte non è richiesto che la lista mantenga l'ordine).

[m1gwings]

Comunque effettivamente, adesso che mi ci fai pensare, dovrei specificare esplicitamente che quello non conserva l'ordine nel caso delle List. (L'ho messo tra i TODO)

[Furrrlo]

Eh sì perché tipo https://github.com/m1gwings/ing-sw-cheatsheet/blob/main/jml.md#L665-L670 non va bene per le liste, perché devi anche controllare che l'ordine della lista non venga modificato, quindi dovresti anche fare \forall int i; i >= 0 && i < j; list.get(i).equals(list.get(i)) e \forall int i; i > j && i < \old(list.size()); list.get(i - 1).equals(\old(list.get(i))) con j indice dell'elemento da rimuovere

[m1gwings]

Sì sì hai ragione. Quando l'ho scritto ricordavo che in più TdE ci fossero liste dove non c'è un ordine specificato, ed in quel caso mi risultava più comodo scrivere quello generico per la collezione in modo da risparmiare un po' di spazio. In realtà ho controllato al volo i TdE degli ultimi 2 anni e succede solo 1 volta nel TdE del 2021-07-13 dove getByArtist restituisce una lista senza un ordine particolare. Quindi in definitiva appena ci rimetto mano lo tolgo (anzi lo converto in quello per i Set) e metto quello per le List a parte come dicevi giustamente tu.