Limbaj de modelare Java

Limbajul de modelare Java ( JML ) este un limbaj de specificare care vă permite să definiți abstracții procedurale pe un model de programare contractuală , prin verificarea parametrilor de intrare ai unei metode și a valorii returnate a acesteia. Este disponibil numai pentru Java 1.4.2.

Specificațiile sunt adăugate în codul sursă Java , prin comentarii cu o sintaxă specială care precede metoda afectată. Aceasta înseamnă că codul JML nu este citit de compilatorul Java, ci doar de instrumentele JML.

Sintaxă

Specificațiile JML sunt exprimate în formular

 // @ <specificarea JML>

sau

 / * @ <Specificații JML> @ * /

Directivele

Principalele directive ale limbii sunt:

requires: definește o condiție prealabilă a metodei care urmează
ensures: definește o post-condiție a metodei care urmează
signals: definește o condiție în care ar trebui aruncată o excepție de la metoda care urmează
assignable: definește câmpurile care pot fi alocate prin următoarea metodă
pure: declară că următoarea metodă nu are efecte secundare (este o abreviere de la assignable \nothing )
invariant: definește o proprietate invariantă a clasei
also: declară că o metodă trebuie să moștenească condiții din superclasa sa.
assert: definește o afirmație JML.

Expresii

JML oferă, de asemenea, următoarele expresii:

\result: identificatorul valorii returnate a metodei care urmează
\old(<name>): modificator pentru a se referi la valoarea variabilei <name> la momentul lansării în metodă
(\forall <dominio>;<range_valori>;<condizione> ): cuantificatorul universal pe o gamă de valori într-un anumit domeniu care îndeplinesc o anumită condiție.
(\exists <dominio>;<range_valori>;<condizione> ): cuantificatorul existențial pe o gamă de valori într-un anumit domeniu care îndeplinesc o anumită condiție.
a ==> b: construcția logică a implică b
a <==> b: construcția logică a dacă și numai dacă b

Adnotările JML au, de asemenea, acces la obiecte Java, precum și la metode și operatori de obiecte . Acestea sunt combinate pentru a oferi specificații formale ale proprietăților claselor, câmpurilor și metodelor. Un exemplu de adnotare simplă a metodei ar putea fi următorul:

 public class BankingExample {
 
     public static final int MAX_BALANCE = 1000 ; 
     echilibru int privat ;
     private boolean isLocked = false ; 
 
     // @ sold invariant> = 0 && sold <= MAX_BALANCE;
 
     // @ sold alocabil;
     // @ asigură echilibru == 0;
     public BankingExample () { ... }
 
     // @ necesită suma> 0;
     // @ asigură sold = \ old (sold) + sumă;
     // @ sold alocabil;
     credit public nul ( suma int ) { ... }
 
     // @ necesită suma> 0;
     // @ asigură sold = \ old (sold) - sumă;
     // @ sold alocabil
     debit public nul ( suma int ) { ... }
 
     // @ asigură isLocked == adevărat;
     public void lockAccount () { ... }
 
     // @ signal (BankingException e) isLocked;
     public / * @ pur @ * / int getBalance () aruncă BankingException {...}
 }

Bibliografie

( RO ) Gary T. Leavens, Yoonsik Cheon. Proiectare prin contract cu JML. Proiect de tutorial.
( RO ) Gary T. Leavens, Albert L. Baker și Clyde Ruby. JML: o notație pentru proiectarea detaliată . În Haim Kilov, Bernhard Rumpe și Ian Simmonds, Specificații comportamentale ale afacerilor și sistemelor , capitolul 12, pp. 175-188. Kluwer, 1999.

linkuri externe

Site-ul oficial , la jmlspecs.org .

Portal IT : accesați intrările Wikipedia care se ocupă cu IT