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.