Linguaggio di modellazione Java - Java Modeling Language

‹Il modello seguente ( necessario un esperto ) viene preso in considerazione per l'eliminazione. Consulta i modelli di discussione per raggiungere un consenso. ›

Il Java Modeling Language ( JML ) è un linguaggio di specifica per programmi Java , che utilizza pre e postcondizioni e invarianti in stile Hoare , che segue il paradigma del design by contract . Le specifiche vengono scritte come commenti di annotazione Java nei file di origine, che quindi possono essere compilati con qualsiasi compilatore Java .

Vari strumenti di verifica, come un runtime assertion checker e l'Extended Static Checker ( ESC / Java ) aiutano lo sviluppo.

Panoramica

JML è un linguaggio di specifica dell'interfaccia comportamentale per i moduli Java. JML fornisce la semantica per descrivere formalmente il comportamento di un modulo Java, prevenendo ambiguità riguardo alle intenzioni dei progettisti del modulo. JML eredita idee da Eiffel , Larch e Refinement Calculus , con l'obiettivo di fornire una semantica formale rigorosa pur essendo accessibile a qualsiasi programmatore Java. Sono disponibili vari strumenti che fanno uso delle specifiche comportamentali di JML. Poiché le specifiche possono essere scritte come annotazioni nei file di programma Java o memorizzate in file di specifiche separati, i moduli Java con specifiche JML possono essere compilati senza modifiche con qualsiasi compilatore Java.

Sintassi

Le specifiche JML vengono aggiunte al codice Java sotto forma di annotazioni nei commenti. I commenti Java vengono interpretati come annotazioni JML quando iniziano con un segno @. Cioè, commenti del modulo

//@ <JML specification>

o

/*@ <JML specification> @*/

La sintassi JML di base fornisce le seguenti parole chiave

requires: Definisce una precondizione sul metodo che segue.
ensures: Definisce una postcondizione sul metodo che segue.
signals: Definisce una postcondizione per quando una determinata eccezione viene lanciata dal metodo che segue.
signals_only: Definisce quali eccezioni possono essere generate quando vale la precondizione data.
assignable: Definisce quali campi possono essere assegnati tramite il metodo che segue.
pure: Dichiara che un metodo è privo di effetti collaterali (come assignable \nothing ma può anche generare eccezioni). Inoltre, un metodo puro dovrebbe sempre terminare normalmente o generare un'eccezione.
invariant: Definisce una proprietà invariante della classe .
loop_invariant: Definisce un ciclo invariante per un ciclo.
also: Combina casi di specifica e può anche dichiarare che un metodo eredita le specifiche dai suoi supertipi.
assert: Definisce un'asserzione JML .
spec_public: Dichiara una variabile pubblica protetta o privata per scopi di specifica.

Il JML di base fornisce anche le seguenti espressioni

\result: Un identificatore per il valore restituito del metodo che segue.
\old(<expression>): Un modificatore per fare riferimento al valore di <expression> al momento dell'ingresso in un metodo.
(\forall <decl>; <range-exp>; <body-exp>): Il quantificatore universale .
(\exists <decl>; <range-exp>; <body-exp>): Il quantificatore esistenziale .
a ==> b: a implica b
a <== b: a è implicito da b
a <==> b: a se e solo se b

così come la sintassi Java standard per logico and, or e not. Le annotazioni JML hanno anche accesso agli oggetti Java, ai metodi degli oggetti e agli operatori che rientrano nell'ambito del metodo annotato e che hanno visibilità appropriata. Questi vengono combinati per fornire specifiche formali delle proprietà di classi, campi e metodi. Ad esempio, potrebbe assomigliare un esempio annotato di una semplice classe bancaria

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

La documentazione completa della sintassi JML è disponibile nel Manuale di riferimento JML .

Supporto dello strumento

Una varietà di strumenti fornisce funzionalità basate su annotazioni JML. Gli strumenti JML dell'Iowa State forniscono un compilatore per il controllo delle asserzioni jmlc che converte le annotazioni JML in asserzioni di runtime, un generatore di documentazione jmldoc che produce documentazione Javadoc arricchita con informazioni aggiuntive dalle annotazioni JML e un generatore di unit test jmlunit che genera il codice di test JUnit dalle annotazioni JML.

Gruppi indipendenti stanno lavorando su strumenti che fanno uso di annotazioni JML. Questi includono:

ESC / Java2 [1] , un controllo statico esteso che utilizza le annotazioni JML per eseguire un controllo statico più rigoroso di quanto sarebbe altrimenti possibile.
OpenJML si dichiara il successore di ESC / Java2.
Daikon , un generatore invariante dinamico.
KeY , che fornisce un prover di teoremi open source con un front-end JML e un plug-in Eclipse ( JML Editing ) con supporto per l' evidenziazione della sintassi di JML.
Krakatoa , uno strumento di verifica statica basato sulla piattaforma di verifica Why e utilizzando l' assistente di prova Coq .
JMLEclipse , un plugin per l'ambiente di sviluppo integrato Eclipse con supporto per la sintassi JML e interfacce per vari strumenti che fanno uso di annotazioni JML.
Sireum / Kiasan , un analizzatore statico basato su esecuzione simbolica che supporta JML come linguaggio contrattuale.
JMLUnit , uno strumento per generare file per l'esecuzione di test JUnit su file Java annotati JML.
TACO , uno strumento di analisi del programma open source che verifica staticamente la conformità di un programma Java rispetto alla specifica del linguaggio di modellazione Java.
VerCors verificatore

Riferimenti

Gary T. Leavens e Yoonsik Cheon. Design by Contract con JML ; Bozza tutorial.
Gary T. Leavens , Albert L. Baker e Clyde Ruby. JML: una notazione per la progettazione dettagliata ; in Haim Kilov, Bernhard Rumpe e Ian Simmonds (editori), Behavioral Specifications of Businesses and Systems , Kluwer, 1999, capitolo 12, pagine 175-188.
Gary T. Leavens , Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin e Daniel M. Zimmerman. JML Reference Manual (DRAFT), settembre 2009. HTML
Marieke Huisman , Wolfgang Ahrendt, Daniel Bruns e Martin Hentschel. Specifica formale con JML . 2014. download (CC-BY-NC-ND)

link esterno

Sito Web JML

Languages

In other projects