जावा मॉडलिंग भाषा

जावा मॉडलिंग लैंग्वेज (जेएमएल) जावा (प्रोग्रामिंग लैंग्वेज) प्रोग्रामों के लिए एक विनिर्देश लैंग्वेज है, जो होरे स्टाइल प्री- और पोस्टकंडिशन और इनवेरिएंट का उपयोग करती है, जो अनुबंध प्रतिमान द्वारा डिजाइन का पालन करती है। विशिष्टताओं को सोर्स फ़ाइलों पर जावा एनोटेशन टिप्पणियों के रूप में लिखा जाता है, जिसे किसी भी जावा कंपाइलर के साथ संकलित किया जा सकता है।

विभिन्न सत्यापन उपकरण (वेलिडेशन टूल्स), जैसे रनटाइम अस्सेरशन चेकर और  एक्सटेंडेड स्टेटिक  चेकर (ईएससी/जावा) विकास में सहायता करते हैं।

अवलोकन

जेएमएल जावा मॉड्यूल के लिए एक व्यवहारिक इंटरफ़ेस विनिर्देश लैंग्वेज है। जेएमएल जावा मॉड्यूल के व्यवहार का औपचारिक रूप से वर्णन करने के लिए शब्दार्थ प्रदान करता है, जो मॉड्यूल डिजाइनरों के इरादों के संबंध में अस्पष्टता को रोकता है। जेएमएल को एफिल, लार्च और रिफाइनमेंट कैलकुलस से विचार विरासत में मिले हैं, जिसका लक्ष्य किसी भी जावा प्रोग्रामर के लिए सुलभ रहते हुए कठिन औपचारिक शब्दार्थ प्रदान करना है। विभिन्न उपकरण उपलब्ध हैं जो जेएमएल के व्यवहार संबंधी विशिष्टताओं का उपयोग करते हैं। क्योंकि विशिष्टताओं को जावा प्रोग्राम फ़ाइलों में एनोटेशन के रूप में लिखा जा सकता है, या अलग-अलग विनिर्देश फ़ाइलों में संग्रहीत किया जा सकता है, जेएमएल विनिर्देशों वाले जावा मॉड्यूल को किसी भी जावा कंपाइलर के साथ अपरिवर्तित संकलित किया जा सकता है।

सिंटेक्स

जेएमएल (JML) विनिर्देशों को टिप्पणियों में एनोटेशन के रूप में जावा कोड में जोड़ा जाता है। जावा टिप्पणियों को जेएमएल एनोटेशन के रूप में समझा जाता है जब वे @ चिह्न से प्रारंभ होते हैं। यानी फॉर्म की टिप्पणियाँ

//@ <JML specification>

या

/*@ <JML specification> @*/

बेसिक जेएमएल सिंटैक्स निम्नलिखित कीवर्ड प्रदान करता है

requires

निम्नलिखित विधि (कंप्यूटर विज्ञान) पर एक पूर्व शर्त को परिभाषित करता है।

ensures

निम्नलिखित विधि पर एक पोस्टकंडीशन को परिभाषित करता है।

signals

एक पोस्टकंडीशन को परिभाषित करता है जब किसी दिए गए अपवाद हैंडलिंग को निम्न विधि द्वारा प्रस्तुत दिया जाता है।

signals_only

परिभाषित करता है कि दी गई पूर्व शर्त लागू होने पर कौन से अपवाद प्रस्तुत किये जा सकते हैं।

assignable

निम्नलिखित विधि द्वारा परिभाषित करता है कि किन फ़ील्ड्स को असाइन करने की अनुमति है।

pure

एक विधि को दुष्प्रभाव मुक्त घोषित करता है (जैसे assignable \nothing लेकिन अपवाद भी प्रस्तुत सकते हैं)। इसके अतिरिक्त, माना जाता है कि एक शुद्ध विधि हमेशा या तो सामान्य रूप से समाप्त हो जाती है या एक अपवाद प्रस्तुत देती है।

invariant

एक वर्ग अपरिवर्तनीय को परिभाषित करें।

loop_invariant

एक लूप के लिए एक लूप अपरिवर्तनीय को परिभाषित करता है।

also

विनिर्देश मामलों को संयोजित करता है और यह भी घोषित कर सकता है कि एक विधि अपने सुपरटाइप्स से विशिष्टताओं को प्राप्त कर रही है।

assert

एक जेएमएल अभिकथन (कंप्यूटिंग) को परिभाषित करता है।

spec_public

विनिर्देश प्रयोजनों के लिए एक संरक्षित या निजी चर को सार्वजनिक घोषित करता है।

बेसिक जेएमएल निम्नलिखित अभिव्यक्तियाँ भी प्रदान करता है

\result

अनुसरण की जाने वाली विधि के रिटर्न मान के लिए एक पहचानकर्ता।

\old(<expression>)

के मान को संदर्भित करने के लिए एक संशोधक <expression> किसी विधि में प्रवेश के समय.

(\forall <decl>; <range-exp>; <body-exp>)

सार्वभौमिक परिमाणक (यूनिवर्सल क्वान्टिफिएर)

(\exists <decl>; <range-exp>; <body-exp>)

अस्तित्वगत परिमाणक (एक्सिस्टेंटिअल क्वान्टिफिएर)

a ==> b

a तात्पर्य b

a <== b

a द्वारा निहित है b

a <==> b

a यदि और केवल यदि b

साथ ही तार्किक और, या, और नहीं के लिए मानक जावा सिंटैक्स है। जेएमएल एनोटेशन के पास जावा ऑब्जेक्ट्स, ऑब्जेक्ट विधियों और ऑपरेटरों तक भी पहुंच है जो एनोटेट की जा रही विधि के दायरे में हैं और जिनकी उचित दृश्यता है। इन्हें क्लासेज, फ़ील्ड्स और मेथड्स के गुणों की औपचारिक विशिष्टताएँ प्रदान करने के लिए संयोजित किया गया है। उदाहरण के लिए, एक साधारण बैंकिंग वर्ग का एक एनोटेटेड उदाहरण ऐसा लग सकता है।

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 संदर्भ मैनुअल में।

उपकरण समर्थन

विभिन्न प्रकार के उपकरण जेएमएल एनोटेशन के आधार पर कार्यक्षमता प्रदान करते हैं। आयोवा स्टेट जेएमएल उपकरण एक दावा जाँच कंपाइलर प्रदान करते हैं jmlc जो जेएमएल एनोटेशन को रनटाइम दावे, एक डॉक्यूमेंट जनरेटर में परिवर्तित करता है jmldoc जो जेएमएल एनोटेशन और एक यूनिट परीक्षण जनरेटर से अतिरिक्त जानकारी के साथ संवर्धित जावाडोक डॉक्यूमेंट तैयार करता है jmlunit जो JML एनोटेशन से JUnit परीक्षण कोड उत्पन्न करता है।

स्वतंत्र समूह ऐसे टूल पर काम कर रहे हैं जो जेएमएल एनोटेशन का उपयोग करते हैं। इसमे सम्मिलित है:

• ESC/Java2 [1], एक विस्तारित स्टेटिक चेकर जो अन्यथा संभव की तुलना में अधिक कठिन स्टेटिक जाँच करने की (KEY) लिए JML एनोटेशन का उपयोग करता है।
• OpenJML स्वयं को ESC/Java2 का उत्तराधिकारी घोषित करता है।
• Daikon, एक डायनामिक अपरिवर्तनीय जनरेटर है।
• KeY, जो JML के वाक्य - विन्यास पर प्रकाश डालना के समर्थन के साथ JML फ्रंट-एंड और एक एक्लिप्स (सॉफ़्टवेयर) प्लग-इन (JML Editing) के साथ एक ओपन सोर्स प्रमेय कहावत प्रदान करता है।
• क्रैकटोआ, एक स्थिर सत्यापन उपकरण जो क्यों (Why) सत्यापन प्लेटफॉर्म पर आधारित है और Coq प्रूफ सहायक का उपयोग करता है।
• JMLEclipse, जेएमएल सिंटैक्स और जेएमएल एनोटेशन का उपयोग करने वाले विभिन्न उपकरणों के इंटरफेस के समर्थन के साथ एक्लिप्स एकीकृत विकास वातावरण के लिए एक प्लगइन है।
• Sireum/Kiasan, एक प्रतीकात्मक निष्पादन आधारित स्टेटिक विश्लेषक जो अनुबंध लैंग्वेज के रूप में JML का समर्थन करता है।
• JMLUnit, JML एनोटेटेड जावा फ़ाइलों पर JUnit परीक्षण चलाने के लिए फ़ाइलें उत्पन्न करने का एक उपकरण है।
• TACO, एक ओपन सोर्स प्रोग्राम विश्लेषण उपकरण जो जावा मॉडलिंग लैंग्वेज विनिर्देश के विरुद्ध जावा प्रोग्राम के अनुपालन की सांख्यिकीय रूप से जांच करता है।

संदर्भ

• Gary T. Leavens and Yoonsik Cheon. Design by Contract with JML; Draft tutorial.
• Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design; in Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, Kluwer, 1999, chapter 12, pages 175-188.
• Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML Reference Manual (DRAFT), September 2009. HTML
• Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel. Formal specification with JML. 2014. download (CC-BY-NC-ND)

बाहरी संबंध

• JML website