Ciao gente, sto cercando di avventurarmi nella jml, allora, //@signal, quando si usa e come si usa, sopr come fare a decidere quando mettere una segnalazione di eccezione piuttosto che una requires in piu. Grazie.
Ciao gente, sto cercando di avventurarmi nella jml, allora, //@signal, quando si usa e come si usa, sopr come fare a decidere quando mettere una segnalazione di eccezione piuttosto che una requires in piu. Grazie.
La sintassi usata:
//@ensures CondizioneA
//@signals (Exception e) CondizioneB
Se la condizioneB viene verificata indipendentemente dalla verità di CondizioneA viene lanciata l'eccezione e.
Converrebbe quasi sempre togliere requires e segnalare eccezione: in fondo con il secondo metodo vieniamo sempre avvisati che qualcosa non va.
Secondo me, conviene mettere eccezioni e non precondizioni soprrattuto quando riusciamo a dimostrare (siamo sicuri...) che la CondizioneA e CondizioneB si autoesclodono: stando in questa situazione è inutile controllare una condizione (in questo caso la B) che potrebbe non verificarsi mai...
...c'è chi come te attende l'alba...
puoi farmi un esempio concreto?
Vedila semplicemente in questo modo (come in java):
Usa le eccezioni e non le requires quando l' "errore" è abbastanza grave.
In fondo l'uso delle eccezioni al posto di qualunque requires non è mai tecnicamente sbagliato: ovvero...la specifica funziona lo stesso.
Ancora conviene usare eccezioni quando il verificarsi della condizione della ensures esclude il verificarsi della condizione della exception (in my opinion)
...c'è chi come te attende l'alba...
Permessi di invio
Rispondi quotando