[JML]: Significato di /*@Pure@*/

[wave00]

In JML a cosa serve e come funziona /*@PURE@*/
Non capisco come mai vengano definiti dei metodi in questo modo e qual'è la sua funzione

[np2k]

I metodi definiti come "pure" sono (QUASI) uguali a quelli in cui definisci
//@assignable nothing
ovvero sono dei metodi che non hanno effetti collaterali, ovvero non modificano lo stato di un oggetto.

Si deve sapere (per spiegare quel "QUASI") che:
nella specifica di un metodo pubblico (non statico) possono essere utilizzati:
1. metodi pubblici puri
2. attributi pubblici
3. possono essere utilizzati solo gli elementi pubblici del metodo (parametri formali e la clausola \result) e della classe

----> ma non possono essere utilizzati metodi pubblici NON PURI.

Quindi se ci interessa che un certo metodo M1 (pubblico e non statico) venga utilizzato nella specifica di un'altro metodo M2 (puro) bisogna che questo sia dichiarato come "pure": se avessimo che l'M1 fosse solo un //@assignable nothing allora non potremmo chiamarlo dalla specifica JML di M2.

Inoltre anche i costruttori possono essere puri, ovvero possono inizializzare gli attributi dichiarati nella classe e non possono fare altro.

Spero di essere stato chiaro.
Ciao.

[np2k]

Non so se leggerai ancora la risposta comunque in quella precedente c'erano delle inessattezze.
Riscrivo:

I metodi definiti come "pure" sono (QUASI) uguali a quelli in cui definisci
//@assignable nothing
ovvero sono dei metodi che non hanno effetti collaterali, ovvero non modificano lo stato di un oggetto.

Si deve sapere (per spiegare quel "QUASI") che:
nella specifica di un metodo pubblico (non statico) possono essere utilizzati:
1. metodi pubblici puri
2. attributi pubblici
3. possono essere utilizzati solo gli elementi pubblici del metodo (parametri formali e la clausola \result) e della classe

----> ma non possono essere utilizzati metodi pubblici NON PURI.

Quindi se ci interessa che un certo metodo M1 (pubblico e non statico) venga utilizzato nella specifica di un'altro metodo M2 (pubblico non statico) bisogna che M1 sia dichiarato come "pure": se avessimo che l'M1 fosse solo un //@assignable nothing allora non potremmo chiamarlo dalla specifica JML di M2.

Inoltre anche i costruttori possono essere puri, ovvero possono inizializzare gli attributi dichiarati nella classe e non possono fare altro.

Spero di essere stato chiaro.
Ciao.