Den Java Modeling Language ( JML ) er et sprog specifikation for Java , den er baseret på paradigmet om programmering af kontrakt . Det bruger Hoares logik , præ- og postbetingelser såvel som invarianter . Specifikationerne tilføjes i kommentarerne til koden i Java, de kompileres derefter af Java- kompilatoren .
Der er forskellige verifikationsværktøjer til JML, såsom en påstandskontrol, der kan køres, og den udvidede statiske kontrol (ESC / Java).
JML er et specifikationssprog til implementeringer i Java . Det giver semantik til formelt at beskrive adfærd af Java-programmer. Dets mål er at fjerne programmets tvetydigheder i forhold til designerens intentioner. JML kan sammenlignes med kontraktprogrammeringen af Eiffel og Larch-familien. Dets mål er at tilvejebringe streng formel verifikationssemantik, der forbliver tilgængelig for enhver Java-programmør. De specifikationer kan skrives direkte i kommentarfeltet Java-kode, eller opbevares i en separat fil specifikation. Forskellige værktøjer kan drage fordel af denne yderligere information leveret af JML-specifikationerne. Eftersom JML-annoteringer har form af kommentarer, kan programmer med sådanne specifikationer desuden kompileres direkte af enhver Java-kompilator.
JML-specifikationer føjes til Java-kode som kommentarer i kommentarer. Disse Java-kommentarer fortolkes som JML-kommentarer, når de starter med en @. Eksempel på JML-kommentarer:
//@ <Spécifications JML>eller
/*@ <Spécification JML> @*/Den basale syntaks for JML er baseret på følgende nøgleord:
requires Definerer en forudsætning for følgende metode . ensures Definerer en posttilstand for følgende metode . signals Definerer en betingelse, der bestemmer, hvornår en given undtagelse kan kastes ved hjælp af følgende metode. assignable Definerer, hvilke attributter der kan tildeles efter følgende metode. pure Erklær en ren metode uden bivirkninger, der ikke ændrer noget (som assignable \nothingmen kan kaste undtagelser). invariant Definerer en uforanderlig egenskab i klassen . also Tillader, at erklæringen om overspecifikationer føjes til de specifikationer, der er arvet fra superklassen. assert Definerer en JML- påstand .JML giver også følgende grundlæggende udtryk:
\result En identifikator for returværdien af følgende metode. \old(<name>) Et modifikator, der refererer til værdien af variablen, <name>når metoden kaldes. \forall Den universelle kvantificering til alt. \exists Den eksistentielle kvantificering er der. a ⇒ b Den logiske relation aindebærerb a ⇔ b Den logiske relation asvarer tilbsåvel som standardlogiske elementer og, eller, og ikke Java-syntaks. JML-annoteringer har også adgang til Java-objekter, metoder og operatører, der er tilgængelige via den kommenterede metode. Alle disse kombineres for at give en formel specifikation af egenskaberne for klasser, attributter og metoder. For eksempel svarer følgende kode til et simpelt eksempel på en JML-specifikation-kommenteret bankkontoklasse:
public class CompteBancaireExemple { public static final int MAX_SOLDE = 1000; private int solde; private boolean isLocked = false; //@ invariant solde >= 0 && solde ⇐ MAX_SOLDE; //@ assignable solde; //@ ensures solde == 0; public CompteBancaireExemple() { ... } //@ requires montant > 0; //@ ensures solde == \old(solde) + montant; //@ assignable solde; public void crediter(int montant) { ... } //@ requires montant > 0; //@ ensures solde == \old(solde) - montant; //@ assignable solde public void debiter(int montant) { ... } //@ ensures isLocked == true; public void lockCompte() { ... } //@ signals (CompteBancaireException e) isLocked; public /*@ pure @*/ int getSolde() throws CompteBancaireException { ... } }Der er forskellige værktøjer, der tilbyder funktionalitet baseret på JML-kommentarer. Iowa State JML-værktøjet kan konvertere JML-annoteringer til påstand, der kan eksekveres via en påstandsbekræftelsescompiler jmlc, generere en forbedret Javadoc inklusive information fra JML-specifikationer og generere enhedstest til JUnit via generatoren jmlunit.
Ud over dette værktøj arbejder uafhængige grupper på værktøjer, der bruger JML. Blandt disse: “ ESC / Java2 ” ( Arkiv • Wikiwix • Archive.is • Google • Hvad skal man gøre? ) , Udvidet statisk kontrol, der bruger JML-kommentarer til at udføre en strengere statisk kontrol end ellers muligt; Daikon , en dynamisk invariant generator; KeY , en sætningskontrol ; Krakatoa , en sætningskontrol baseret på Coq- bevis assistent ; og JMLeclipse , et plugin til det integrerede Eclipse- udviklingsmiljø.