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