Java-mallinnuskieli - Java Modeling Language

‹Alla olevaa mallia ( tarvitaan asiantuntijaa ) poistetaan. Katso keskustelupohjat yksimielisyyden saavuttamiseksi. ›

Java Modeling Language ( JML ) on erittely kieli ja Java -ohjelmia käyttäen Hoare tyyli esi- ja loppuehdot ja invariants , joka seuraa sopimuspohjainen ohjelmointi paradigma. Tekniset tiedot kirjoitetaan Java-huomautuskommentteina lähdetiedostoihin, jotka voidaan siten kääntää millä tahansa Java- kääntäjällä .

Erilaiset vahvistustyökalut, kuten ajonaikaisen vahvistuksen tarkistaja ja Extended Static Checker ( ESC / Java ), auttavat kehittämisessä.

Yleiskatsaus

JML on Java-moduulien käyttäytymisrajapinnan määrityskieli. JML tarjoaa semantiikkaa kuvaamaan virallisesti Java-moduulin käyttäytymistä estäen epäselvyyksiä moduulin suunnittelijoiden aikomuksista. JML perii ideoita Eiffel , lehtikuusi ja tarkentaminen Calculus , jonka tavoitteena on tarjota tiukan muodollinen semantiikka, kun vielä saatavilla mitään Java ohjelmoija. Saatavilla on erilaisia työkaluja, jotka hyödyntävät JML: n käyttäytymismäärityksiä. Koska tekniset tiedot voidaan kirjoittaa huomautuksina Java-ohjelmatiedostoihin tai tallentaa erillisiin määritystiedostoihin, JML-määrityksillä varustetut Java-moduulit voidaan koota muuttumattomina minkä tahansa Java-kääntäjän kanssa.

Syntaksi

JML-määritykset lisätään Java-koodiin kommenttien muodossa kommentteina. Java-kommentit tulkitaan JML-merkinnöiksi, kun ne alkavat @ -merkillä. Eli lomakkeen kommentit

//@ <JML specification>

tai

/*@ <JML specification> @*/

JML-perussyntaksi tarjoaa seuraavat avainsanat

requires: Määrittelee edellytys on menetelmä , joka seuraa.
ensures: Määrittää jälkiseoksen seuraavalle menetelmälle.
signals: Määrittää jälkisehdon sille, milloin tietty poikkeus heitetään seuraavalla menetelmällä.
signals_only: Määrittää, mitä poikkeuksia voidaan heittää, kun annettu edellytys täyttyy.
assignable: Määrittää, mitkä kentät voidaan määrittää seuraavalla menetelmällä.
pure: Julistaa menetelmän sivuvaikutuksettomaksi (kuten, assignable \nothing mutta voi myös heittää poikkeuksia). Lisäksi puhtaan menetelmän oletetaan aina joko päättyvän normaalisti tai aiheuttavan poikkeuksen.
invariant: Määrittää luokan invariantin ominaisuuden .
loop_invariant: Määrittää silmukan invariantin silmukalle.
also: Yhdistää spesifikaatiotapaukset ja voi myös ilmoittaa, että menetelmä perii spesifikaatiot sen supertyypeistä.
assert: Määrittää JML- väitteen .
spec_public: Ilmoittaa suojatun tai yksityisen muuttujan julkiseksi määrittelyä varten.

Basic JML tarjoaa myös seuraavat lausekkeet

\result: Tunniste seuraavan menetelmän palautusarvolle.
\old(<expression>): Muunnos, joka viittaa arvon arvoon <expression> menetelmän syöttöhetkellä.
(\forall <decl>; <range-exp>; <body-exp>): Universaali kvantisointi .
(\exists <decl>; <range-exp>; <body-exp>): Eksistentiaalinen kvantisointi .
a ==> b: a viittaa b
a <== b: a viittaa b
a <==> b: a jos ja vain jos b

sekä tavallinen Java-syntaksin looginen ja, tai, ja ei. JML-merkinnöillä on myös pääsy Java-objekteihin, objektimenetelmiin ja operaattoreihin, jotka ovat huomautettavan menetelmän piirissä ja joilla on asianmukainen näkyvyys. Nämä yhdistetään muodollisten eritelmien antamiseksi luokkien, kenttien ja menetelmien ominaisuuksille. Esimerkiksi kommentoitu esimerkki yksinkertaisesta pankkiluokasta voi näyttää

public class BankingExample
{
 
    public static final int MAX_BALANCE = 1000; 
    private /*@ spec_public @*/ int balance;
    private /*@ spec_public @*/ boolean isLocked = false; 
 
    //@ public invariant balance >= 0 && balance <= MAX_BALANCE;
 
    //@ assignable balance;
    //@ ensures balance == 0;
    public BankingExample()
    {
        this.balance = 0;
    }
 
    //@ requires 0 < amount && amount + balance < MAX_BALANCE;
    //@ assignable balance;
    //@ ensures balance == \old(balance) + amount;
    public void credit(final int amount)
    {
        this.balance += amount;
    }
 
    //@ requires 0 < amount && amount <= balance;
    //@ assignable balance;
    //@ ensures balance == \old(balance) - amount;
    public void debit(final int amount)
    {
        this.balance -= amount;
    }
 
    //@ ensures isLocked == true;
    public void lockAccount()
    {
        this.isLocked = true;
    }
 
    //@   requires !isLocked;
    //@   ensures \result == balance;
    //@ also
    //@   requires isLocked;
    //@   signals_only BankingException;
    public /*@ pure @*/ int getBalance() throws BankingException
    {
        if (!this.isLocked)
        {
                return this.balance;
        }
        else
        {
                throw new BankingException();
        }
    }
}

JML-syntaksin täydellinen dokumentaatio on saatavilla JML-käsikirjassa .

Työkalutuki

Erilaiset työkalut tarjoavat toimintoja, jotka perustuvat JML-merkintöihin. Iowan osavaltion JML-työkalut tarjoavat väitteiden tarkistamisen kääntäjän, jmlc joka muuntaa JML-merkinnät ajonaikaisiksi väitteiksi, dokumentointigeneraattorin, jmldoc joka tuottaa Javadoc- dokumentaatiota täydennettynä JML-merkinnöistä saatavilla lisätiedoilla, ja yksikön testigeneraattorilla, jmlunit joka tuottaa JUnit- testikoodin JML-merkinnöistä.

Riippumattomat ryhmät työskentelevät työkalujen parissa, jotka käyttävät JML-merkintöjä. Nämä sisältävät:

ESC / Java2 [1] , laajennettu staattinen tarkistaja, joka käyttää JML-merkintöjä suorittamaan tiukemman staattisen tarkistuksen kuin muuten on mahdollista.
OpenJML julistaa itsensä ESC / Java2: n seuraajaksi.
Daikon , dynaaminen invarianttigeneraattori.
KeY , joka tarjoaa avoimen lähdekoodin lauseen JML-käyttöliittymällä ja Eclipse- laajennuksella ( JML Editing ), joka tukee JML : n syntaksikorostusta .
Krakatoa , staattinen vahvistustyökalu, joka perustuu Why- tarkistusalustaan ja käyttää Coq proof -apuria.
JMLEclipse , integroidun Eclipse-kehitysympäristön laajennus, joka tukee JML-syntaksia ja rajapintoja erilaisiin työkaluihin, jotka käyttävät JML-merkintöjä.
Sireum / Kiasan , symbolinen suorituspohjainen staattinen analysaattori, joka tukee JML: ää sopimuskielenä.
JMLUnit , työkalu tiedostojen luomiseen JUnit-testien suorittamista varten JML-merkinnöillä varustetuilla Java-tiedostoilla.
TACO , avoimen lähdekoodin ohjelmaanalyysityökalu, joka tarkistaa staattisesti Java-ohjelman yhteensopivuuden Java Modeling Language -määrityksen kanssa.
VerCors-todentaja

Viitteet

Gary T.Levvens ja Yoonsik Cheon. Suunnittelu sopimuksen mukaan JML: n kanssa ; Luonnos opetusohjelma.
Gary T.Leavens , Albert L.Baker ja Clyde Ruby. JML: merkintä yksityiskohtaista suunnittelua varten ; julkaisussa Haim Kilov, Bernhard Rumpe ja Ian Simmonds (toimittajat), Yritysten ja järjestelmien käyttäytymismääritykset , Kluwer, 1999, luku 12, sivut 175--188.
Gary T.Leavens , Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin ja Daniel M.Zimmerman. JML Reference Manual (DRAFT), syyskuu 2009. HTML
Marieke Huisman , Wolfgang Ahrendt, Daniel Bruns ja Martin Hentschel. Muodollinen erittely JML: llä . 2014. lataa (CC-BY-NC-ND)

Ulkoiset linkit

JML-verkkosivusto

Languages

In other projects