जावा मॉडलिंग भाषा: Difference between revisions

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




Line 6: Line 6:


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


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


  //@ <JML specification>
  //@ <JML specification>
Line 19: Line 19:
बेसिक जेएमएल सिंटैक्स निम्नलिखित कीवर्ड प्रदान करता है
बेसिक जेएमएल सिंटैक्स निम्नलिखित कीवर्ड प्रदान करता है


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


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


[[Category:Created On 24/07/2023]]
[[Category:Created On 24/07/2023]]
Line 112: Line 112:


== उपकरण समर्थन ==
== उपकरण समर्थन ==
विभिन्न प्रकार के उपकरण जेएमएल एनोटेशन के आधार पर कार्यक्षमता प्रदान करते हैं। आयोवा स्टेट जेएमएल उपकरण एक दावा जाँच कंपाइलर प्रदान करते हैं <code>jmlc</code> जो जेएमएल एनोटेशन को रनटाइम दावे, एक दस्तावेज़ जनरेटर में परिवर्तित करता है <code>jmldoc</code> जो जेएमएल एनोटेशन और एक यूनिट परीक्षण जनरेटर से अतिरिक्त जानकारी के साथ संवर्धित [[जावाडोक]] दस्तावेज़ तैयार करता है <code>jmlunit</code> जो JML एनोटेशन से [[JUnit]] परीक्षण कोड उत्पन्न करता है।
विभिन्न प्रकार के उपकरण जेएमएल एनोटेशन के आधार पर कार्यक्षमता प्रदान करते हैं। आयोवा स्टेट जेएमएल उपकरण एक दावा जाँच कंपाइलर प्रदान करते हैं <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/], एक विस्तारित स्थैतिक चेकर जो अन्यथा संभव की तुलना में अधिक कठोर स्थैतिक जाँच करने [[ चाबी ]] लिए JML एनोटेशन का उपयोग करता है।
* 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://www.openjml.org/ OpenJML] स्वयं को ESC/Java2 का उत्तराधिकारी घोषित करता है।
* [http://pag.csAIL.mit.edu/daikon/ Daikon], एक गतिशील अपरिवर्तनीय जनरेटर।
* [http://pag.csAIL.mit.edu/daikon/ Daikon], एक डायनामिक अपरिवर्तनीय जनरेटर है।
* KeY, जो JML के [[ वाक्य - विन्यास पर प्रकाश डालना ]] के समर्थन के साथ JML फ्रंट-एंड और एक एक्लिप्स (सॉफ़्टवेयर) प्लग-इन ([http://www.key-project.org/eclipse/JMLEditing/ JML Editing]) के साथ एक ओपन सोर्स प्रमेय कहावत प्रदान करता है।
* KeY, जो JML के [[ वाक्य - विन्यास पर प्रकाश डालना ]] के समर्थन के साथ JML फ्रंट-एंड और एक एक्लिप्स (सॉफ़्टवेयर) प्लग-इन ([http://www.key-project.org/eclipse/JMLEditing/ JML Editing]) के साथ एक ओपन सोर्स प्रमेय कहावत प्रदान करता है।
* [http://krakatoa.lri.fr क्रैकटोआ], एक स्थिर सत्यापन उपकरण जो [http://why.lri.fr क्यों] सत्यापन प्लेटफॉर्म पर आधारित है और [[Coq]] प्रूफ सहायक का उपयोग करता है।
* [http://krakatoa.lri.fr क्रैकटोआ], एक स्थिर सत्यापन उपकरण जो [http://why.lri.fr क्यों] (Why) सत्यापन प्लेटफॉर्म पर आधारित है और Coq प्रूफ सहायक का उपयोग करता है।
* [http://jmleclipse.projects.cis.ksu.edu/ JMLEclipse], जेएमएल सिंटैक्स और जेएमएल एनोटेशन का उपयोग करने वाले विभिन्न उपकरणों के इंटरफेस के समर्थन के साथ एक्लिप्स एकीकृत विकास वातावरण के लिए एक प्लगइन।
* [http://jmleclipse.projects.cis.ksu.edu/ JMLEclipse], जेएमएल सिंटैक्स और जेएमएल एनोटेशन का उपयोग करने वाले विभिन्न उपकरणों के इंटरफेस के समर्थन के साथ एक्लिप्स एकीकृत विकास वातावरण के लिए एक प्लगइन।
* [http://www.sireum.org/?q=node/21/ Sireum/Kiasan], एक प्रतीकात्मक निष्पादन आधारित स्थैतिक विश्लेषक जो अनुबंध भाषा के रूप में JML का समर्थन करता है।
* [http://www.sireum.org/?q=node/21/ Sireum/Kiasan], एक प्रतीकात्मक निष्पादन आधारित स्टेटिक विश्लेषक जो अनुबंध लैंग्वेज के रूप में JML का समर्थन करता है।
* [http://www.eecs.ucf.edu/~leavens/JML2/docs/man/jmlunit.html JMLUnit], JML एनोटेटेड जावा फ़ाइलों पर JUnit परीक्षण चलाने के लिए फ़ाइलें उत्पन्न करने का एक उपकरण।
* [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], एक खुला स्रोत प्रोग्राम विश्लेषण उपकरण जो जावा मॉडलिंग भाषा विनिर्देश के विरुद्ध जावा प्रोग्राम के अनुपालन की सांख्यिकीय रूप से जांच करता है।
* [https://web.archive.org/web/20110706084805/http://www.dc.uba.ar/inv/grupos/rfm_folder/TACO TACO], एक ओपन सोर्स प्रोग्राम विश्लेषण उपकरण जो जावा मॉडलिंग लैंग्वेज विनिर्देश के विरुद्ध जावा प्रोग्राम के अनुपालन की सांख्यिकीय रूप से जांच करता है।


== संदर्भ ==
== संदर्भ ==

Revision as of 15:58, 6 August 2023

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


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

अवलोकन

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

सिंटेक्स

जेएमएल (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)


बाहरी संबंध

Retrieved from ‘https://www.vigyanwiki.in/index.php?title=जावा_मॉडलिंग_भाषा&oldid=246747’