Java Modelling Language: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
m Orfanizzo Java (linguaggio) |
m tag source deprecati, replaced: <source lang= → <syntaxhighlight lang= (3), </source> → </syntaxhighlight> (3) |
||
Riga 5:
==Sintassi==
Le specifiche JML sono espresse nella forma
<
//@ <Specifica JML>
</syntaxhighlight>
oppure
<
/*@ <Specifica JML> @*/
</syntaxhighlight>
===Direttive===
Riga 48:
Le annotazioni JML hanno inoltre accesso agli [[oggetto (informatica)|oggetti]] Java, oltre che ai metodi ed agli [[Operatore (informatica)|operatori]] degli oggetti. Questi sono combinati per fornire specifiche formali delle proprietà delle classi, dei campi e dei metodi. Un esempio di semplice annotazione di un metodo potrebbe essere il seguente:
<
public class BankingExample {
Riga 77:
public /*@ pure @*/ int getBalance() throws BankingException { ... }
}
</syntaxhighlight>
==Bibliografia==
| |||