Język modelowania Java - Java Modeling Language

‹Poniższy szablon ( wymagany ekspert ) jest rozważany do usunięcia. Zobacz szablony do dyskusji, które pomogą osiągnąć konsensus. ›

Java Modeling Language ( JML ) to język specyfikacja dla Javy programów wykorzystujących Hoare stylu pre- i postconditions i niezmienników , że podąża za programowanie kontraktowe paradygmatu. Specyfikacje są zapisywane jako komentarze adnotacji Java do plików źródłowych, które w związku z tym mogą być kompilowane za pomocą dowolnego kompilatora Java .

Różne narzędzia weryfikacyjne, takie jak narzędzie do sprawdzania asercji w czasie wykonywania i rozszerzony kontroler statyczny ( ESC / Java ), ułatwiają tworzenie oprogramowania.

Przegląd

JML to język specyfikacji interfejsu behawioralnego dla modułów Java. JML zapewnia semantykę do formalnego opisu zachowania modułu Java, zapobiegając niejednoznaczności w odniesieniu do intencji projektantów modułu. JML dziedziczy idee z Eiffla , Larcha i Refinement Calculus , mając na celu zapewnienie rygorystycznej formalnej semantyki, będąc nadal dostępnym dla każdego programisty Java. Dostępne są różne narzędzia, które wykorzystują specyfikacje behawioralne JML. Ponieważ specyfikacje mogą być zapisywane jako adnotacje w plikach programu Java lub przechowywane w oddzielnych plikach specyfikacji, moduły Java ze specyfikacjami JML mogą być kompilowane bez zmian za pomocą dowolnego kompilatora Java.

Składnia

Specyfikacje JML są dodawane do kodu Java w postaci adnotacji w komentarzach. Komentarze Java są interpretowane jako adnotacje JML, gdy zaczynają się od znaku @. To znaczy komentarze do formularza

//@ <JML specification>

lub

/*@ <JML specification> @*/

Podstawowa składnia JML zawiera następujące słowa kluczowe

requires: Definiuje warunek wstępny dla metody, która następuje.
ensures: Definiuje warunek końcowy w metodzie, która następuje.
signals: Definiuje warunek końcowy, w którym dany wyjątek jest zgłaszany przez poniższą metodę.
signals_only: Definiuje, jakie wyjątki mogą być generowane, gdy spełniony jest dany warunek wstępny.
assignable: Określa, które pola mogą być przypisywane za pomocą poniższej metody.
pure: Deklaruje metodę jako wolną od skutków ubocznych (na przykład, assignable \nothing ale może również zgłaszać wyjątki). Co więcej, czysta metoda powinna zawsze kończyć się normalnie lub zgłosić wyjątek.
invariant: Definiuje niezmienną właściwość klasy .
loop_invariant: Definiuje niezmienną pętlę dla pętli.
also: Łączy przypadki specyfikacji i może również deklarować, że metoda dziedziczy specyfikacje ze swoich nadtypów.
assert: Definiuje JML twierdzenie .
spec_public: Deklaruje zmienną chronioną lub prywatną jako publiczną do celów specyfikacji.

Podstawowy JML udostępnia również następujące wyrażenia

\result: Identyfikator wartości zwracanej metody, która następuje.
\old(<expression>): Modyfikator odnoszący się do wartości <expression> w momencie wejścia do metody.
(\forall <decl>; <range-exp>; <body-exp>): Kwantyfikator .
(\exists <decl>; <range-exp>; <body-exp>): Kwantyfikator egzystencjalny .
a ==> b: a sugeruje b
a <== b: a jest implikowane przez b
a <==> b: a wtedy i tylko wtedy gdy b

a także standardową składnię Java dla logicznych i, lub, i nie. Adnotacje JML mają również dostęp do obiektów Java, metod obiektowych i operatorów, które znajdują się w zakresie adnotacji metody i które mają odpowiednią widoczność. Są one łączone, aby zapewnić formalne specyfikacje właściwości klas, pól i metod. Na przykład może wyglądać opisany przykład prostej klasy bankowej

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();
        }
    }
}

Pełna dokumentacja składni JML jest dostępna w podręczniku JML Reference Manual .

Wsparcie narzędziowe

Różnorodne narzędzia zapewniają funkcjonalność opartą na adnotacjach JML. Narzędzia JML stanu Iowa zapewniają kompilator sprawdzania asercji, jmlc który konwertuje adnotacje JML na asercje środowiska uruchomieniowego, generator dokumentacji, jmldoc który tworzy dokumentację Javadoc wzbogaconą o dodatkowe informacje z adnotacji JML, oraz generator testów jednostkowych, jmlunit który generuje kod testowy JUnit z adnotacji JML.

Niezależne grupy pracują nad narzędziami wykorzystującymi adnotacje JML. Obejmują one:

ESC / Java2 [1] , rozszerzone narzędzie do sprawdzania statycznego, które wykorzystuje adnotacje JML do wykonywania bardziej rygorystycznych kontroli statycznych niż jest to możliwe w innym przypadku.
OpenJML deklaruje się następcą ESC / Java2.
Daikon , dynamiczny niezmienny generator.
KeY , który udostępnia narzędzie do sprawdzania twierdzeń typu open source z interfejsem JML i wtyczką Eclipse ( edycja JML ) z obsługą podświetlania składni JML.
Krakatoa , narzędzie do weryfikacji statycznej oparte na platformie weryfikacji Why i przy użyciu asystenta Coq proof.
JMLEclipse , wtyczka do zintegrowanego środowiska programistycznego Eclipse z obsługą składni JML i interfejsami do różnych narzędzi wykorzystujących adnotacje JML.
Sireum / Kiasan , analizator statyczny oparty na symbolicznym wykonaniu, który obsługuje JML jako język kontraktowy.
JMLUnit , narzędzie do generowania plików do uruchamiania testów JUnit na plikach Java z adnotacjami JML.
TACO , narzędzie do analizy programów typu open source, które statycznie sprawdza zgodność programu Java ze specyfikacją Java Modeling Language.
Weryfikator VerCors

Bibliografia

Gary T. Leavens i Yoonsik Cheon. Zaprojektuj na podstawie umowy z JML ; Szkic samouczka.
Gary T. Leavens , Albert L. Baker i Clyde Ruby. JML: notacja do projektowania szczegółowego ; w Haim Kilov, Bernhard Rumpe i Ian Simmonds (redaktorzy), Behavioral Specifications of Businesses and Systems , Kluwer, 1999, rozdział 12, strony 175-188.
Gary T. Leavens , Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin i Daniel M. Zimmerman. JML Reference Manual (DRAFT), wrzesień 2009. HTML
Marieke Huisman , Wolfgang Ahrendt, Daniel Bruns i Martin Hentschel. Formalna specyfikacja z JML . 2014. pobierz (CC-BY-NC-ND)

Zewnętrzne linki

Witryna JML

Languages

In other projects