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

{{Short description|Specification language for Java programs}}
'''जावा मॉडलिंग लैंग्वेज (जेएमएल)''' [[ जावा (प्रोग्रामिंग भाषा) |जावा (प्रोग्रामिंग लैंग्वेज)]] प्रोग्रामों के लिए एक विनिर्देश लैंग्वेज है, जो होरे स्टाइल प्री- और पोस्टकंडिशन और इनवेरिएंट का उपयोग करती है, जो अनुबंध प्रतिमान द्वारा डिजाइन का पालन करती है। विशिष्टताओं को सोर्स फ़ाइलों पर जावा एनोटेशन टिप्पणियों के रूप में लिखा जाता है, जिसे किसी भी जावा [[कंपाइलर का अनुकूलन|कंपाइलर]] के साथ संकलित किया जा सकता है।


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

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

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

 //@ <JML specification>

या

 /*@ <JML specification> @*/

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

; <code>requires</code> : निम्नलिखित विधि (कंप्यूटर विज्ञान) पर एक पूर्व शर्त को परिभाषित करता है।
; <code>ensures</code> : निम्नलिखित विधि पर एक पोस्टकंडीशन को परिभाषित करता है।
; <code>signals</code> : एक पोस्टकंडीशन को परिभाषित करता है जब किसी दिए गए अपवाद हैंडलिंग को निम्न विधि द्वारा प्रस्तुत दिया जाता है।
; <code>signals_only</code> : परिभाषित करता है कि दी गई पूर्व शर्त लागू होने पर कौन से अपवाद प्रस्तुत किये जा सकते हैं।
; <code>assignable</code> : निम्नलिखित विधि द्वारा परिभाषित करता है कि किन फ़ील्ड्स को असाइन करने की अनुमति है।
; <code>pure</code> : एक विधि को दुष्प्रभाव मुक्त घोषित करता है (जैसे <code>assignable \nothing</code> लेकिन अपवाद भी प्रस्तुत सकते हैं)। इसके अतिरिक्त, माना जाता है कि एक शुद्ध विधि हमेशा या तो सामान्य रूप से समाप्त हो जाती है या एक अपवाद प्रस्तुत देती है।
; <code>invariant</code> : एक [[वर्ग अपरिवर्तनीय]] को परिभाषित करें।
; <code>loop_invariant</code> : एक लूप के लिए एक [[ लूप अपरिवर्तनीय |लूप अपरिवर्तनीय]]  को परिभाषित करता है।
; <code>also</code> : विनिर्देश मामलों को संयोजित करता है और यह भी घोषित कर सकता है कि एक विधि अपने सुपरटाइप्स से विशिष्टताओं को प्राप्त कर रही है।
; <code>assert</code> : एक जेएमएल अभिकथन (कंप्यूटिंग) को परिभाषित करता है।
; <code>spec_public</code> : विनिर्देश प्रयोजनों के लिए एक संरक्षित या निजी चर को सार्वजनिक घोषित करता है।

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

; <code>\result</code> : अनुसरण की जाने वाली विधि के रिटर्न मान के लिए एक पहचानकर्ता।
; <code>\old(<expression>)</code> : के मान को संदर्भित करने के लिए एक संशोधक <code><expression></code> किसी विधि में प्रवेश के समय.
; <code>(\forall <decl>; <range-exp>; <body-exp>)</code> : सार्वभौमिक परिमाणक (यूनिवर्सल क्वान्टिफिएर)
; <code>(\exists <decl>; <range-exp>; <body-exp>)</code> : अस्तित्वगत परिमाणक (एक्सिस्टेंटिअल क्वान्टिफिएर)
; <code>a ==> b</code> : <code>a</code> तात्पर्य <code>b</code>
; <code>a <== b</code> : <code>a</code> द्वारा निहित है <code>b</code>
; <code>a <==> b</code> : <code>a</code> यदि और केवल यदि <code>b</code>
साथ ही तार्किक और, या, और नहीं के लिए मानक जावा सिंटैक्स है। जेएमएल एनोटेशन के पास जावा ऑब्जेक्ट्स, ऑब्जेक्ट विधियों और ऑपरेटरों तक भी पहुंच है जो एनोटेट की जा रही विधि के दायरे में हैं और जिनकी उचित दृश्यता है। इन्हें क्लासेज, फ़ील्ड्स और मेथड्स के गुणों की औपचारिक विशिष्टताएँ प्रदान करने के लिए संयोजित किया गया है। उदाहरण के लिए, एक साधारण बैंकिंग वर्ग का एक एनोटेटेड उदाहरण ऐसा लग सकता है। 
<syntaxhighlight lang="java">
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();
        }
    }
}
</syntaxhighlight>
जेएमएल सिंटैक्स का पूर्ण डॉक्यूमेंटीकरण उपलब्ध है [http://jmlspecs.org/jmlrefman/jmlrefman_toc.html JML संदर्भ मैनुअल में]।












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

स्वतंत्र समूह ऐसे टूल पर काम कर रहे हैं जो जेएमएल एनोटेशन का उपयोग करते हैं। इसमे सम्मिलित है:
* ESC/Java2 [https://web.archive.org/web/20051016013145/http://secure.ucd.ie/products/opensource/ESCJava2/], एक विस्तारित स्टेटिक चेकर जो अन्यथा संभव की तुलना में अधिक कठिन स्टेटिक जाँच करने की (KEY) लिए JML एनोटेशन का उपयोग करता है।
* [http://www.openjml.org/ OpenJML] स्वयं को ESC/Java2 का उत्तराधिकारी घोषित करता है।
* [http://pag.csAIL.mit.edu/daikon/ Daikon], एक डायनामिक अपरिवर्तनीय जनरेटर है।
* KeY, जो JML के [[ वाक्य - विन्यास पर प्रकाश डालना ]] के समर्थन के साथ JML फ्रंट-एंड और एक एक्लिप्स (सॉफ़्टवेयर) प्लग-इन ([http://www.key-project.org/eclipse/JMLEditing/ JML Editing]) के साथ एक ओपन सोर्स प्रमेय कहावत प्रदान करता है।
* [http://krakatoa.lri.fr क्रैकटोआ], एक स्थिर सत्यापन उपकरण जो [http://why.lri.fr क्यों] (Why) सत्यापन प्लेटफॉर्म पर आधारित है और Coq प्रूफ सहायक का उपयोग करता है।
* [http://jmleclipse.projects.cis.ksu.edu/ JMLEclipse], जेएमएल सिंटैक्स और जेएमएल एनोटेशन का उपयोग करने वाले विभिन्न उपकरणों के इंटरफेस के समर्थन के साथ एक्लिप्स एकीकृत विकास वातावरण के लिए एक प्लगइन है।
* [http://www.sireum.org/?q=node/21/ Sireum/Kiasan], एक प्रतीकात्मक निष्पादन आधारित स्टेटिक विश्लेषक जो अनुबंध लैंग्वेज के रूप में JML का समर्थन करता है।
* [http://www.eecs.ucf.edu/~leavens/JML2/docs/man/jmlunit.html JMLUnit], JML एनोटेटेड जावा फ़ाइलों पर JUnit परीक्षण चलाने के लिए फ़ाइलें उत्पन्न करने का एक उपकरण है।
* [https://web.archive.org/web/20110706084805/http://www.dc.uba.ar/inv/grupos/rfm_folder/TACO 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. [http://www.jmlspecs.org/jmlrefman/jmlrefman_toc.html HTML]
* [[Marieke Huisman]], Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel.  ''Formal specification with JML''. 2014. [http://primo.bibliothek.kit.edu/primo_library/libweb/action/dlDisplay.do?vid=KIT&docId=KITSRCE1000041881&tab=kit_evastar&srt=date download (CC-BY-NC-ND)]
== बाहरी संबंध ==
* [http://www.eecs.ucf.edu/~leavens/JML/index.shtml JML website]

[[Category:Created On 24/07/2023]]
[[Category:Lua-based templates]]
[[Category:Machine Translated Page]]
[[Category:Pages with script errors|Short description/doc]]
[[Category:Short description with empty Wikidata description]]
[[Category:Template documentation pages|Short description/doc]]
[[Category:Templates Vigyan Ready]]
[[Category:Templates that add a tracking category]]
[[Category:Templates that generate short descriptions]]
[[Category:Templates using TemplateData]]
[[Category:उदाहरण जावा कोड वाले लेख]]
[[Category:औपचारिक विशिष्टता भाषाएँ]]
[[Category:जावा प्लेटफार्म]]