Java Modelleme Dili - Java Modeling Language

‹Aşağıdaki şablon ( Uzman gereklidir ) silinmek üzere değerlendiriliyor. Bir fikir birliğine varmaya yardımcı olması için tartışma şablonlarına bakın . ›

Java Modelleme Dili ( JML ) bir olduğunu belirtim dili için Java kullanarak programları Hoare tarzı onceden ve Hedefşartlar ve değişmezleri izler, sözleşme ile tasarım paradigması. Spesifikasyonlar , kaynak dosyalara Java açıklama yorumları olarak yazılır ve bu nedenle herhangi bir Java derleyicisiyle derlenebilir .

Çalışma zamanı onaylama denetleyicisi ve Genişletilmiş Statik Denetleyici ( ESC / Java ) gibi çeşitli doğrulama araçları, geliştirmeye yardımcı olur.

Genel Bakış

JML, Java modülleri için davranışsal bir arayüz belirtim dilidir. JML, bir Java modülünün davranışını resmi olarak tanımlamak için anlambilim sağlar ve modül tasarımcılarının niyetleriyle ilgili belirsizliği önler. JML, Eiffel , Larch ve Refinement Calculus'tan alınan fikirleri devralır ve herhangi bir Java programcısı tarafından erişilebilir olmaya devam ederken titiz biçimsel anlamlar sağlama amacı taşır . JML'nin davranışsal özelliklerini kullanan çeşitli araçlar mevcuttur. Spesifikasyonlar Java program dosyalarında açıklama olarak yazılabildiğinden veya ayrı spesifikasyon dosyalarında saklanabildiğinden, JML spesifikasyonlarına sahip Java modülleri herhangi bir Java derleyicisiyle değiştirilmeden derlenebilir.

Sözdizimi

JML spesifikasyonları, yorumlarda ek açıklamalar şeklinde Java koduna eklenir. Java yorumları, @ işaretiyle başladıklarında JML ek açıklamaları olarak yorumlanır. Yani, formun yorumları

//@ <JML specification>

veya

/*@ <JML specification> @*/

Temel JML sözdizimi aşağıdaki anahtar kelimeleri sağlar

requires: Bir tanımlar ön şartı üzerinde yöntemle izler.
ensures: Aşağıdaki yöntemde bir son koşul tanımlar .
signals: Aşağıdaki yöntem tarafından belirli bir İstisna oluşturulduğunda bir son koşul tanımlar .
signals_only: Verilen ön koşul gerçekleştiğinde hangi istisnaların atılabileceğini tanımlar.
assignable: Aşağıdaki yöntem tarafından hangi alanlara atanmasına izin verildiğini tanımlar.
pure: Bir yöntemin yan etkisiz olduğunu bildirir (gibi assignable \nothing ancak istisnalar da atabilir). Dahası, saf bir yöntemin her zaman ya normal şekilde sonlandırması ya da bir istisna oluşturması beklenir.
invariant: Sınıfın değişmez bir özelliğini tanımlar .
loop_invariant: Bir döngü için döngüsel değişmez tanımlar .
also: Spesifikasyon durumlarını birleştirir ve ayrıca bir yöntemin spesifikasyonları süper tiplerinden miras aldığını bildirebilir.
assert: Bir JML iddiasını tanımlar .
spec_public: Spesifikasyon amaçları için korumalı veya özel bir değişkeni genel olarak bildirir.

Temel JML ayrıca aşağıdaki ifadeleri sağlar

\result: Aşağıdaki yöntemin dönüş değeri için bir tanımlayıcı.
\old(<expression>): Bir <expression> yönteme giriş anındaki değerine atıfta bulunan bir değiştirici .
(\forall <decl>; <range-exp>; <body-exp>): Evrensel miktar belirleyici .
(\exists <decl>; <range-exp>; <body-exp>): Varoluşsal miktar belirleyici .
a ==> b: a ima eder b
a <== b: a ima ediliyor b
a <==> b: a ancak ve ancak b

mantıksal ve veya, ve değil için standart Java sözdizimi . JML açıklamalarının ayrıca, açıklama eklenen yöntemin kapsamına giren ve uygun görünürlüğe sahip olan Java nesnelerine, nesne yöntemlerine ve işleçlerine erişimi vardır. Bunlar, sınıfların, alanların ve yöntemlerin özelliklerinin biçimsel özelliklerini sağlamak için birleştirilir. Örneğin, basit bir bankacılık sınıfının açıklamalı bir örneği şöyle görünebilir:

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 sözdiziminin tam dokümantasyonu JML Referans Kılavuzunda mevcuttur .

Araç desteği

Çeşitli araçlar, JML açıklamalarına dayalı işlevsellik sağlar. Iowa State JML araçları , JML açıklamalarını çalışma zamanı iddialarına dönüştüren bir onaylama denetimi derleyicisi jmlc , JML açıklamalarından gelen ek bilgilerle artırılmış Javadoc belgeleri jmldoc üreten bir belge üreteci ve JML açıklamalarından JUnit test kodu üreten bir birim test üreteci sağlar . jmlunit

Bağımsız gruplar, JML notlarından yararlanan araçlar üzerinde çalışıyor. Bunlar şunları içerir:

ESC / Java2 [1] , aksi takdirde mümkün olandan daha sıkı statik kontrol gerçekleştirmek için JML açıklamalarını kullanan genişletilmiş bir statik denetleyici.
OpenJML kendisini ESC / Java2'nin halefi olarak ilan eder.
Daikon , dinamik değişmez bir jeneratör.
ÖNEMLİ bir JML ön uç ve bir birlikte bir açık kaynak teoremi prover sağlar, Eclipse plug-in ( JML düzenleme desteği ile) dizim JML arasında.
Neden doğrulama platformuna dayanan ve Coq prova yardımcısını kullanan statik bir doğrulama aracı olan Krakatoa .
JML sözdizimini destekleyen ve JML açıklamalarını kullanan çeşitli araçlara arabirimlere sahip Eclipse entegre geliştirme ortamı için bir eklenti olan JMLEclipse .
Sireum / Kiasan , sözleşme dili olarak JML'yi destekleyen sembolik yürütme tabanlı statik analizci.
JMLUnit , JML açıklamalı Java dosyalarında JUnit testleri çalıştırmak için dosyalar oluşturmak için bir araçtır.
TACO , bir Java programının Java Modelleme Dili spesifikasyonuna uygunluğunu statik olarak kontrol eden açık kaynaklı bir program analiz aracıdır.
VerCors doğrulayıcı

Referanslar

Gary T. Leavens ve Yoonsik Cheon. JML ile Sözleşmeli Tasarım ; Taslak öğretici.
Gary T. Leavens , Albert L. Baker ve Clyde Ruby. JML: Ayrıntılı Tasarım İçin Bir Gösterim ; Haim Kilov, Bernhard Rumpe ve Ian Simmonds (editörler), İşlerin ve Sistemlerin Davranış Özellikleri , Kluwer, 1999, bölüm 12, sayfalar 175-188.
Gary T. Leavens , Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin ve Daniel M. Zimmerman. JML Referans Kılavuzu (TASLAK), Eylül 2009. HTML
Marieke Huisman , Wolfgang Ahrendt, Daniel Bruns ve Martin Hentschel. JML ile resmi şartname . 2014. indirme (CC-BY-NC-ND)

Dış bağlantılar

JML web sitesi

Languages

In other projects