वियना विकास विधि: Difference between revisions
From Vigyanwiki
(Created page with "{{short description|Formal method for the development of computer-based systems}} वियना विकास विधि (वीडीएम) कंप्यूटर-...") |
No edit summary |
||
| (12 intermediate revisions by 3 users not shown) | |||
| Line 1: | Line 1: | ||
{{short description|Formal method for the development of computer-based systems}} | {{short description|Formal method for the development of computer-based systems}} | ||
वियना | '''वियना डेवलपमेंट मेथड''' (वीडीएम) कंप्यूटर-बेस्ड सिस्टम्स के डेवलपमेंट के लिए सबसे लंबे समय से स्थापित फॉर्मल मेथड में से है। [[आईबीएम प्रयोगशाला वियना]] में किए गए कार्य से उत्पन्न <ref>Some idea of that work, including a technical report TR 25.139 on "[https://link.springer.com/content/pdf/10.1007%2FBFb0048942.pdf A Formal Definition of a PL/1 Subset]", dated 20 December 1974, is reprinted in Jones 1984, p.107-155. Of particular note is the list of authors in order: H. Bekič, D. Bjørner, W. Henhapl, C. B. Jones, P. Lucas.</ref> 1970 के दशक में, यह फॉर्मल स्पेसिफिकेशन लैंग्वेज -वीडीएम स्पेसिफिकेशन लैंग्वेज (वीडीएम-एसएल) पर बेस्ड तकनीकों और उपकरणों के समूह को सम्मिलित करने के लिए विकसित हुआ है। इसका विस्तारित रूप है, वीडीएम++,<ref>The double plus is adopted from the [[C++]] objected oriented programming language based on C.</ref> जो [[ वस्तु के उन्मुख |ऑब्जेक्ट-ओरिएंटेड]] और कांकररेंट सिस्टम्स के मॉडलिंग का समर्थन करता है। वीडीएम के समर्थन में मॉडलों का विश्लेषण करने के लिए वाणिज्यिक और अकादमिक उपकरण सम्मिलित हैं, जिसमें मॉडलों के गुणों का परीक्षण और सिद्ध करने और मान्य वीडीएम मॉडल से प्रोग्राम कोड उत्पन्न करने के लिए समर्थन सम्मिलित है। वीडीएम और उसके उपकरणों के औद्योगिक उपयोग का इतिहास है और फॉर्मल में अनुसंधान के बढ़ते समूह ने महत्वपूर्ण सिस्टम्स, [[संकलनकर्ता|संएल्गोरिथ्म कर्ता]], कांकररेंट सिस्टम्स की इंजीनियरिंग और [[कंप्यूटर विज्ञान]] के लिए [[तर्क|लॉजिक]] में उल्लेखनीय योगदान दिया है। | ||
== | ==फिलोसॉफी== | ||
प्रोग्रामिंग | प्रोग्रामिंग लैंग्वेज ओं का उपयोग करके प्राप्त करने योग्य की तुलना में कंप्यूटिंग सिस्टम को वीडीएम-एसएल में एब्सट्रेक्शन के उच्च स्तर पर मॉडलिंग किया जा सकता है, जिससे सिस्टम डेवलपमेंट के प्रारंभिक फेज में डिज़ाइन के विश्लेषण और दोषों सहित प्रमुख विशेषताओं की पहचान की अनुमति मिलती है। जिन मॉडलों को मान्य किया गया है उन्हें शोधन प्रक्रिया के माध्यम से विस्तृत सिस्टम डिज़ाइन में परिवर्तित किया जा सकता है। लैंग्वेज में फॉर्मल शब्दार्थ है, जो उच्च स्तर के आश्वासन के लिए मॉडल के गुणों का प्रमाण देना संभव बनाता है। इसमें निष्पादन योग्य सबसेट भी है, जिससे मॉडल का परीक्षण करके विश्लेषण किया जा सकता है और ग्राफिकल यूजर इंटरफेस के माध्यम से निष्पादित किया जा सकता है, जिससे मॉडल का मूल्यांकन उन विशेषज्ञों द्वारा किया जा सके जो आवश्यक रूप से मॉडलिंग लैंग्वेज से परिचित नहीं हैं। | ||
==इतिहास== | ==इतिहास== | ||
वीडीएम-एसएल की उत्पत्ति [[वियना]] में [[आईबीएम]] प्रयोगशाला में हुई जहां | वीडीएम-एसएल की उत्पत्ति [[वियना]] में [[आईबीएम]] प्रयोगशाला में हुई जहां लैंग्वेज के पहले संस्करण को वियना डेफिनिशन लैंग्वेज (वीडीएल) कहा जाता था।<ref>Bjørner&Jones 1978, [https://link.springer.com/content/pdf/bfm%3A978-3-540-35836-7%2F1.pdf Introduction], p.ix</ref> वीडीएल का उपयोग अनिवार्य रूप से वीडीएम - मेटा-IV के विपरीत [[परिचालन शब्दार्थ|ऑपरेशनल सेमांटिक्स]] डिस्क्रिप्शन देने के लिए किया गया था, जो [[सांकेतिक शब्दार्थ|डिनोटैस्नल]] [[परिचालन शब्दार्थ|सेमांटिक्स]] प्रदान करता था।<ref>Introductory remarks by Cliff B. Jones (editor) in Bekič 1984, p.vii</ref> | ||
«1972 के अंत में वियना समूह ने फिर से लैंग्वेज डिफ्निसन से कम्पाइलर को व्यवस्थित रूप से विकसित करने की समस्या पर अपना ध्यान केंद्रित किया था। अपनाए गए समग्र दृष्टिकोण को वियना डेवलपमेंट मेथड कहा गया है ... वास्तव में अपनाई गई मेटा-लैंग्वेज (मेटा-IV) का उपयोग पीएल/1 के प्रमुख भागो को परिभाषित करने के लिए किया जाता है (जैसा कि ईसीएमए 74 में दिया गया है - रौचक बात यह है कि एब्सट्रेक्ट इंटरप्रेटर के रूप में लिखा गया फॉर्मल मानक डॉक्यूमेंट ) BEKIČ 74 में।<ref>Bjørner&Jones 1978, [https://link.springer.com/content/pdf/bfm%3A978-3-540-35836-7%2F1.pdf Introduction], p.xi</ref> | |||
भाषा के लिए मानकीकरण मानक के लिए | |||
[[मेटा-IV]] के बीच कोई संबंध नहीं है,<ref>Bjørner&Jones 1978, p.24.</ref> और शोर्रे की मेटा II लैंग्वेज , या इसकी उत्तराधिकारी [[ वृक्ष मेटा |ट्री मेटा]] ; ये फॉर्मल समस्या विवरण के लिए उपयुक्त होने के अतिरिक्त [[ संकलक-संकलक |कम्पाइलर -कम्पाइलर]] सिस्टम थे। | |||
इसलिए मेटा-IV का उपयोग पीएल/आई प्रोग्रामिंग लैंग्वेज के प्रमुख भागों को परिभाषित करने के लिए किया गया था। मेटा-IV और वीडीएम-एसएल का उपयोग करके पूर्वव्यापी रूप से वर्णित या आंशिक रूप से वर्णित अन्य प्रोग्रामिंग लैंग्वेज ओं में [[बुनियादी प्रोग्रामिंग भाषा|बेसिक प्रोग्रामिंग लैंग्वेज]] , [[फोरट्रान]], [[एपीएल प्रोग्रामिंग भाषा|एपीएल प्रोग्रामिंग लैंग्वेज]] ,एल्गोल 60, [[एडा प्रोग्रामिंग भाषा|एडा प्रोग्रामिंग लैंग्वेज]] और [[पास्कल प्रोग्रामिंग भाषा|पास्कल प्रोग्रामिंग लैंग्वेज]] सम्मिलित हैं। मेटा-IV कई टाइप में विकसित हुआ, जिन्हें समान्यत: डेनिश, अंग्रेजी और आयरिश स्कूलों के रूप में वर्णित किया गया है। | |||
इंग्लिश स्कूल वीडीएम के उन मेथड पर [[क्लिफ जोन्स (कंप्यूटर वैज्ञानिक)]] के कार्य से प्राप्त हुआ है जो विशेष रूप से लैंग्वेज डिफ्निसन और कंपाइलर डिजाइन से संबंधित नहीं हैं (जोन्स 1980, 1990)। यह निरंतर मॉडलिंग पर बल देता है <ref>See the article on [[Persistence (computer science)|persistence]] for its use within computer science.</ref> आधार टाइप के समृद्ध स्टोर से निर्मित डेटा टाइप के उपयोग के माध्यम से बताएं। कार्यक्षमता को समान्यत: उन ऑपरेशन के माध्यम से वर्णित किया जाता है जिनके स्टेट पर दुष्प्रभाव हो सकते हैं और जो अधिकतर पूर्व नियम और पोस्टकंडिशन का उपयोग करके अंतर्निहित रूप से निर्दिष्ट होते हैं। डेनिश स्कूल (डाइन्स ब्योर्नर या ब्योर्नर एट अल. 1982) ने अधिक सीमा तक उपयोग किए जाने वाले स्पष्ट परिचालन स्पेसिफिकेशन के साथ रचनात्मक दृष्टिकोण पर बल दिया है। डेनिश स्कूल में कार्य करने से पहला यूरोपीय मान्य एडा प्रोग्रामिंग लैंग्वेज कंपाइलर तैयार हुआ था। | |||
लैंग्वेज के लिए मानकीकरण मानक के लिए अंतर्राष्ट्रीय संगठन 1996 में प्रारंभ किया गया था (आईएसओ, 1996)। | |||
==वीडीएम सुविधाएँ== | ==वीडीएम सुविधाएँ== | ||
वीडीएम-एसएल और वीडीएम++ सिंटैक्स और शब्दार्थ का वर्णन वीडीएमटूल्स लैंग्वेज मैनुअल और उपलब्ध टेक्स्ट में विस्तार से किया गया है। आईएसओ मानक में लैंग्वेज के शब्दार्थ की फॉर्मल डिफ्निसन सम्मिलित है। इस आलेख के शेष भाग में, आईएसओ-परिभाषित इंटरचेंज (एएससीआईआई) सिंटैक्स का उपयोग किया गया है। कुछ टेक्स्ट अधिक संक्षिप्त [[गणितीय संकेतन]] को प्राथमिकता देते हैं। | |||
वीडीएम-एसएल मॉडल डेटा पर निष्पादित कार्यक्षमता के | वीडीएम-एसएल मॉडल डेटा पर निष्पादित कार्यक्षमता के कॉन्टेक्स्ट में दिया गया सिस्टम विवरण है। इसमें डेटा टाइप और उन पर निष्पादित कार्यों या संचालन की डिफ्निसन ओं की श्रृंखला सम्मिलित है। | ||
===मूल प्रकार: संख्यात्मक, वर्ण, टोकन और | ===मूल प्रकार: संख्यात्मक, वर्ण, टोकन और कोटे प्रकार=== | ||
वीडीएम-एसएल में | वीडीएम-एसएल में बेसिक टाइप के मॉडलिंग नंबर और अक्षर इस टाइप सम्मिलित हैं: | ||
{| border="1" class="wikitable" | {| border="1" class="wikitable" | ||
|+ style="background:#ffdead;" | | |+ style="background:#ffdead;" | बेसिक टाइप | ||
|- | |- | ||
| <code>bool</code> || | | <code>bool</code> || बूलियन डाटा टाइप || {{mono|false, true}} | ||
|- | |- | ||
| <code>nat</code> || [[natural number]] | | <code>nat</code> || [[natural number|नेचुरल नंबर]] (शून्य सहित) || {{mono|0, 1, 2, 3, 4, 5 ...}} | ||
|- | |- | ||
| <code>nat1</code> || | | <code>nat1</code> || नेचुरल नंबर (शून्य छोड़कर) || {{mono|1, 2, 3, 4, 5, ...}} | ||
|- | |- | ||
| <code>int</code> || | | <code>int</code> ||इन्टिजर | ||
| {{mono|..., −3, −2, −1, 0, 1, 2, 3, ...}} | |||
|- | |- | ||
| <code>rat</code> || [[rational number]] | | <code>rat</code> || [[rational number|रैशनल नंबर]] || {{mono|a/b}}, जहां {{mono|a}} और {{mono|b}} पूर्णांक हैं, {{mono|b}} {{mono|0}} नहीं है | ||
|- | |- | ||
| <code>real</code> || [[real number]] | | <code>real</code> || [[real number|रियल नंबर]] || {{mono|...}} | ||
|- | |- | ||
| <code>char</code> || | | <code>char</code> || करैक्टर || {{mono|A, B, C, ...}} | ||
|- | |- | ||
| <code>token</code> || | | <code>token</code> || स्ट्रक्चरलेस टोकन || {{mono|...}} | ||
|- | |- | ||
| <code><A></code> || | | <code><A></code> ||कोटे टाइप जिसमें मान <A> है | ||
| {{mono|...}} | |||
|} | |} | ||
डेटा | डेटा टाइप को मॉडल किए गए सिस्टम के मुख्य डेटा का प्रतिनिधित्व करने के लिए परिभाषित किया गया है। प्रत्येक टाइप की डिफ्निसन नए टाइप के नाम का परिचय देती है और मूल टाइप के कॉन्टेक्स्ट में या पहले से प्रस्तुत किए गए टाइप के कॉन्टेक्स्ट में प्रतिनिधित्व देती है। उदाहरण के लिए, लॉग-इन मैनेजमेंट सिस्टम के लिए टाइप के मॉडलिंग उपयोगकर्ता पहचानकर्ता को निम्नानुसार परिभाषित किया जा सकता है: | ||
types | |||
UserId = nat | |||
डेटा | डेटा टाइप से संबंधित मूल्यों में परिवर्तन करने के लिए, ऑपरेटरों को मूल्यों पर परिभाषित किया जाता है। इस प्रकार, प्राकृतिक संख्या जोड़, घटाव आदि प्रदान किए जाते हैं, जैसे कि समानता और असमानता जैसे बूलियन ऑपरेटर होते हैं। लैंग्वेज अधिकतम या न्यूनतम प्रतिनिधित्व योग्य संख्या या वास्तविक संख्याओं के लिए कोई परिशुद्धता तय नहीं करती है। ऐसी बाधाओं को परिभाषित किया जाता है जहां डेटा टाइप के इनवेरिएंट के माध्यम से प्रत्येक मॉडल में उनकी आवश्यकता होती है - बूलियन अभिव्यक्तियां उन स्थितियों को दर्शाती हैं जिनका परिभाषित टाइप के सभी कॉम्पोनेन्टं द्वारा सम्मान किया जाना चाहिए। उदाहरण के लिए, आवश्यकता कि उपयोगकर्ता पहचानकर्ता 9999 से अधिक नहीं होने चाहिए, निम्नानुसार व्यक्त की जाएगी (जहां <code><=</code> प्राकृतिक संख्याओं पर बूलियन ऑपरेटर से कम या उसके समान है): | ||
UserId = nat | |||
inv uid == uid <= 9999 | |||
चूंकि अपरिवर्तनीय | चूंकि अपरिवर्तनीय इच्छित रूप से काम्प्लेक्स लॉजिक अभिव्यक्ति हो सकते हैं, और परिभाषित टाइप की सदस्यता केवल उन मूल्यों तक सीमित है जो अपरिवर्तनीय को संतुष्ट करते हैं, वीडीएम-एसएल में टाइप की शुद्धता सभी स्थितियों में स्वचालित रूप से निर्णय लेने योग्य नहीं है। | ||
अन्य | अन्य बेसिक टाइप में वर्णों के लिए वर्ण सम्मिलित हैं। कुछ स्थितियों में, किसी टाइप का प्रतिनिधित्व मॉडल के उद्देश्य के लिए प्रासंगिक नहीं है और इससे केवल काम्प्लेक्स बढ़ेगी। ऐसे स्थितियों में, टाइप के सदस्यों को संरचनाहीन टोकन के रूप में दर्शाया जा सकता है। टोकन टाइप के मूल्यों की तुलना केवल समानता के लिए की जा सकती है - उन पर कोई अन्य ऑपरेटर परिभाषित नहीं हैं। जहां विशिष्ट नामित मानों की आवश्यकता होती है, उन्हें कोटे टाइप के रूप में प्रस्तुत किया जाता है। प्रत्येक कोटे टाइप में टाइप के समान नाम का नामित मान होता है। कोटे टाइप के मान (कोटे शाब्दिक के रूप में जाना जाता है) की तुलना केवल समानता के लिए की जा सकती है। | ||
उदाहरण के लिए, ट्रैफ़िक सिग्नल | उदाहरण के लिए, ट्रैफ़िक सिग्नल कंट्रोलर के मॉडलिंग में, ट्रैफ़िक सिग्नल के रंगों को कोटे टाइप के रूप में दर्शाने के लिए मानों को परिभाषित करना सुविधाजनक हो सकता है: | ||
< | <Red>, <Amber>, <FlashingAmber>, <Green> | ||
=== | ===कंस्ट्रक्शन टाइप: यूनियन, प्रोडक्ट और कम्पोजिट टाइप === | ||
केवल मूल | केवल मूल टाइप ही सीमित मूल्य के हैं। नए, अधिक संरचित डेटा टाइप टाइप कंस्ट्रक्टर का उपयोग करके बनाए जाते हैं। | ||
{| border="1" class="wikitable" | {| border="1" class="wikitable" | ||
|+ style="background:#ffdead;" | | |+ style="background:#ffdead;" | बेसिक टाइप कंस्ट्रक्शन | ||
|- | |- | ||
| <code><nowiki>T1 | T2 | ... | Tn</nowiki></code> || | | <code><nowiki>T1 | T2 | ... | Tn</nowiki></code> || यूनियन टाइप <code>T1,...,Tn</code> | ||
|- | |- | ||
| <code>T1*T2*...*Tn</code> || | | <code>T1*T2*...*Tn</code> || टाइप के कार्टेशियन प्रोडक्ट <code>T1,...,Tn</code> | ||
|- | |- | ||
| <code>T :: f1:T1 ... fn:Tn</code> || | | <code>T :: f1:T1 ... fn:Tn</code> ||समग्र (रिकॉर्ड) प्रकार | ||
|} | |} | ||
सबसे | सबसे बेसिक टाइप का कंस्ट्रक्टर दो पूर्वनिर्धारित टाइप का मिलन बनाता है। प्ररूप <code>(A|B)</code> इसमें A टाइप के सभी कॉम्पोनेन्ट और टाइप के सभी कॉम्पोनेन्ट सम्मिलित हैं <code>B</code>. ट्रैफ़िक सिग्नल कंट्रोलर उदाहरण में, ट्रैफ़िक सिग्नल के रंग मॉडलिंग के टाइप को निम्नानुसार परिभाषित किया जा सकता है: | ||
SignalColour = <Red> | <Amber> | <FlashingAmber> | <Green> | |||
वीडीएम-एसएल में [[प्रगणित प्रकार]] | वीडीएम-एसएल में [[प्रगणित प्रकार|प्रगणित]] टाइप को कोटे टाइप पर यूनियनों के रूप में ऊपर दिखाए गए अनुसार परिभाषित किया गया है। | ||
कार्टेशियन | कार्टेशियन प्रोडक्ट टाइप को वीडीएम-एसएल में भी परिभाषित किया जा सकता है। प्ररूप <code>(A1*…*An)</code> मानों के सभी टुपल्स से बना टाइप है, जिसका पहला कॉम्पोनेन्ट टाइप से है <code>A1</code> और दूसरा टाइप से <code>A2</code> और इसी तरह मिश्रित या रिकॉर्ड टाइप कार्टेशियन प्रोडक्ट है जिसमें फ़ील्ड के लिए लेबल होते हैं। प्ररूप | ||
T :: f1:A1 | |||
f2:A2 | |||
... | |||
fn:An | |||
<code>f1,…,fn</code> लेबल वाले फ़ील्ड वाला कार्टेशियन प्रोडक्ट है। टाइप <code>T</code> का कॉम्पोनेन्ट उसके घटक भागों से कंस्ट्रक्टर द्वारा बनाया जा सकता है, जिसे <code>mk_T</code> लिखा जाता है। इसके विपरीत, टाइप <code>T</code>का कॉम्पोनेन्ट दिए जाने पर, नामित घटक का चयन करने के लिए फ़ील्ड नामों का उपयोग किया जा सकता है। उदाहरण के लिए, प्रकार | |||
Date :: day:nat1 | |||
month:nat1 | |||
year:nat | |||
inv mk_Date(d,m,y) == d <=31 and m<=12 | |||
एक साधारण दिनांक | एक साधारण दिनांक टाइप मॉडल करता है। मान <code>mk_Date(1,4,2001)</code> 1 अप्रैल 2001 से मेल खाता है। दिनांक <code>d</code> दी गई है अभिव्यक्ति <code>d.month</code> महीने का प्रतिनिधित्व करने वाली प्राकृतिक संख्या है। यदि चाहें तो प्रति माह दिनों और लीप वर्ष पर प्रतिबंध को अपरिवर्तनीय में सम्मिलित किया जा सकता है। इनका संयोजन: | ||
mk_Date(1,4,2001). | mk_Date(1,4,2001).month = 4 | ||
=== | ===कलेक्शन्स === | ||
स्टोर टाइप मानो के मॉडल समूह सेट परिमित अव्यवस्थित स्टोर हैं जिनमें मानों के बीच दोहराव को दबा दिया जाता है। अनुक्रम परिमित क्रमित स्टोर (सूचियाँ) हैं जिनमें दोहराव हो सकता है और मैपिंग मानों के दो सेटों के बीच परिमित कॉरेस्पोंडेंस का प्रतिनिधित्व करते हैं। | |||
==== सेट ==== | ==== सेट ==== | ||
सेट | सेट टाइप का कंस्ट्रक्टर (<code>T</code> का लिखित <code>set of T</code> पूर्वनिर्धारित टाइप है) टाइप <code>T</code> से खींचे गए मानों के सभी परिमित सेटों से बना टाइप का निर्माण करता है। उदाहरण के लिए टाइप की परिभाषा<syntaxhighlight> | ||
UGroup = set of UserId | |||
</syntaxhighlight><code>UserId</code>मानों के सभी परिमित सेटों से बना टाइप <code>UGroup</code> को परिभाषित करता है। विभिन्न ऑपरेटरों को उनके संघ, प्रतिच्छेदन, उचित और गैर-सख्त सबसेट संबंधों का निर्धारण आदि के लिए सेट पर परिभाषित किया गया है। | |||
{| | {| class="wikitable" border="1" | ||
|+ style="background:#ffdead;" | | |+ style="background:#ffdead;" |सेट पर मुख्य ऑपरेटर (s, s1, s2 सेट हैं) | ||
|- | |- | ||
| <code>{a, b, c}</code> || | | <code>{a, b, c}</code> || गणना सेट करें: एलिमेंट का सेट <code>a</code>, <code>b</code> और <code>c</code> | ||
|- | |- | ||
| <code><nowiki>{x | x:T & P(x)}</nowiki></code> || | | <code><nowiki>{x | x:T & P(x)}</nowiki></code> || सेट कॉम्प्रिहेंशन: का सेट <code>x</code> का प्रकार <code>T</code> ऐसा है कि <code>P(x)</code> | ||
|- | |- | ||
| <code>{i, ..., j}</code> || | | <code>{i, ..., j}</code> || <code>i</code> से <code>j</code> की सीमा में पूर्णांकों का समुच्चय | ||
|- | |- | ||
| <code>e in set s</code> || <code>e</code> | | <code>e in set s</code> || <code>e</code> सेट <code>s</code> का एलिमेंट है | ||
|- | |- | ||
| <code>e not in set s</code> || <code>e</code> | | <code>e not in set s</code> || <code>e</code> सेट <code>s</code> का एलिमेंट नहीं है | ||
|- | |- | ||
| <code>s1 union s2</code> || | | <code>s1 union s2</code> || सेट <code>s1</code> और <code>s2</code> का यूनियन | ||
|- | |- | ||
| <code>s1 inter s2</code> || | | <code>s1 inter s2</code> || सेट <code>s1</code> और <code>s2</code> का प्रतिच्छेदन | ||
|- | |- | ||
| <code>s1 \ s2</code> || | | <code>s1 \ s2</code> || सेट s1 और s2 का अंतर निर्धारित करें | ||
|- | |- | ||
| <code>dunion s</code> || | | <code>dunion s</code> || सेट के सेट का डिस्ट्रीब्यूटेड यूनियन s | ||
|- | |- | ||
| <code>s1 psubset s2</code> || s1 | | <code>s1 psubset s2</code> || s1, <code>s2</code> का एक (प्रोपर) सबसेट है | ||
|- | |- | ||
| <code>s1 subset s2</code> || s1 | | <code>s1 subset s2</code> || s1 , <code>s2</code> का एक (अशक्त) सबसेट है | ||
|- | |- | ||
| <code>card s</code> || | | <code>card s</code> || सेट <code>s</code> की कार्डिनैलिटी | ||
|} | |} | ||
==== अनुक्रम ==== | ==== अनुक्रम ==== | ||
परिमित अनुक्रम | परिमित अनुक्रम टाइप कंस्ट्रक्टर (लिखित) <code>seq of T</code> जहाँ <code>T</code> पूर्वनिर्धारित टाइप है) टाइप से निकाले गए मानों की सभी सीमित सूचियों से बना टाइप <code>T</code> बनाता है . उदाहरण के लिए, टाइप की डिफ्निसन | ||
String = seq of char | |||
एक | एक टाइप को परिभाषित करता है <code>String</code> वर्णों की सभी सीमित श्रृंखलाओं से बना है। विभिन्न ऑपरेटरों को संयोजन के निर्माण, कॉम्पोनेन्टं और उसके पश्चात् के अनुक्रम आदि के चयन के लिए अनुक्रमों पर परिभाषित किया गया है। इनमें से कई ऑपरेटर इस अर्थ में आंशिक हैं कि उन्हें कुछ अनुप्रयोगों के लिए परिभाषित नहीं किया गया है। उदाहरण के लिए, किसी अनुक्रम के 5वें कॉम्पोनेन्ट का चयन करना जिसमें केवल तीन कॉम्पोनेन्ट हैं, अपरिभाषित है। | ||
इसलिए, | इसलिए, क्रम में वस्तुओं का क्रम और पुनरावृत्ति महत्वपूर्ण है <code>[a, b]</code> के समान नहीं है <code>[b, a]</code>, और <code>[a]</code> के समान नहीं है <code>[a, a]</code>. | ||
{| border="1" class="wikitable" | {| border="1" class="wikitable" | ||
|+ style="background:#ffdead;" | | |+ style="background:#ffdead;" |अनुक्रमों पर मुख्य संचालक (s, s1,s2 अनुक्रम हैं) | ||
|- | |- | ||
| <code>[a, b, c]</code> || | | <code>[a, b, c]</code> || अनुक्रम गणना: कॉम्पोनेन्टं <code>a</code>, <code>b</code> and <code>c</code> का अनुक्रम | ||
|- | |- | ||
| <code><nowiki>[f(x) | x:T & P(x)]</nowiki></code> || | | <code><nowiki>[f(x) | x:T & P(x)]</nowiki></code> || अनुक्रम बोध: (संख्यात्मक) प्रकार T के प्रत्येक x के लिए अभिव्यक्ति f(x) का अनुक्रम इस प्रकार है कि P(x) बना रहे | ||
(x मान संख्यात्मक क्रम में लिया गया है) | |||
|- | |- | ||
| <code>hd s</code> || | | <code>hd s</code> || <code>s</code>का प्रमुख (प्रथम अवयव) | ||
|- | |- | ||
| <code>tl s</code> || | | <code>tl s</code> ||<code>s</code>की पूँछ (सिर हटाने के पश्चात् शेष क्रम)। | ||
|- | |- | ||
| <code>len s</code> || | | <code>len s</code> ||<code>s</code>की लंबाई | ||
|- | |- | ||
| <code>elems s</code> || | | <code>elems s</code> ||<code>s</code>के कॉम्पोनेन्टं का सेट | ||
|- | |- | ||
| <code>s(i)</code> || | | <code>s(i)</code> || <code>s का i<sup>th</sup> अवयव</code> | ||
|- | |- | ||
| <code>inds s</code> || | | <code>inds s</code> ||अनुक्रम के लिए सूचकांकों का सेट <code>s</code> | ||
|- | |- | ||
| <code>s1^s2</code> || | | <code>s1^s2</code> || अनुक्रम s1 और s2 को जोड़ने से बना अनुक्रम | ||
|} | |} | ||
==== मानचित्र ==== | ==== मानचित्र ==== | ||
एक परिमित मानचित्रण दो सेटों, डोमेन और रेंज के बीच, रेंज के डोमेन अनुक्रमण | एक परिमित मानचित्रण दो सेटों, डोमेन और रेंज के बीच, रेंज के डोमेन अनुक्रमण कॉम्पोनेन्टं के साथ कॉरेस्पोंडेंस है। इसलिए यह परिमित कार्य के समान है। वीडीएम-एसएल में मैपिंग टाइप का कंस्ट्रक्टर (लिखित) <code>map T1 to T2</code> जहाँ <code>T1</code> और <code>T2</code> पूर्वनिर्धारित टाइप हैं) सेट से सभी परिमित मैपिंग से बने टाइप का निर्माण करता है जिसमे<code>T1</code> के सेट के लिए मान <code>T2</code> मूल्य. उदाहरण के लिए, टाइप की डिफ्निसन | ||
Birthdays = map String to Date | |||
एक | एक टाइप को परिभाषित करता है <code>Birthdays</code> जो कैरेक्टर स्ट्रिंग्स को मैप करता है <code>Date</code>. फिर से, मैपिंग में अनुक्रमण, मैपिंग को मर्ज करने, उप-मैपिंग को निकालने के लिए ओवरराइटिंग के लिए ऑपरेटरों को मैपिंग पर परिभाषित किया जाता है। | ||
{| border="1" class="wikitable" | {| border="1" class="wikitable" | ||
|+ style="background:#ffdead;" | | |+ style="background:#ffdead;" |मैपिंग पर मुख्य ऑपरेटर | ||
|- | |- | ||
| <code><nowiki>{a |-> r, b |-> s}</nowiki></code> || | | <code><nowiki>{a |-> r, b |-> s}</nowiki></code> || मैपिंग गणना: <code>a</code> मैप्स टू <code>r</code>, <code>b</code> मैप्स टू <code>s</code> | ||
|- | |- | ||
| <code><nowiki>{x |-> f(x) | x:T & P(x)}</nowiki></code> || | | <code><nowiki>{x |-> f(x) | x:T & P(x)}</nowiki></code> || मैपिंग कॉम्प्रिहेंशन: <code>x</code> प्रकार <code>T</code> के लिए सभी <code>x</code> के लिए <code>f(x)</code> पर मैप करता है, जैसे कि<code>P(x</code>): | ||
|- | |- | ||
| <code>dom m</code> || | | <code>dom m</code> || <code>m</code> का डोमेन | ||
|- | |- | ||
| <code>rng m</code> || | | <code>rng m</code> || <code>m की रेंज</code> | ||
|- | |- | ||
| <code>m(x)</code> || <code>m</code> | | <code>m(x)</code> || <code>m</code> <code>x</code> पर प्रयुक्त होता है | ||
|- | |- | ||
| <code>m1 munion m2</code> || | | <code>m1 munion m2</code> || मैपिंग <code>m1</code> और <code>m2</code> (<code>m1</code>, <code>m2</code> जहां वह ओवरलैप होते हैं वहां सुसंगत होना चाहिए) | ||
|- | |- | ||
| <code>m1 ++ m2</code> || <code>m1</code> | | <code>m1 ++ m2</code> || <code>m1</code> को <code>m2</code> द्वारा अधिलेखित किया गया | ||
|} | |} | ||
===संरचना=== | ===संरचना=== | ||
वीडीएम-एसएल और वीडीएम++ नोटेशन के बीच मुख्य अंतर संरचना से सामना करने के मेथड में है। वीडीएम-एसएल में पारंपरिक मॉड्यूलर एक्सटेंशन है जबकि वीडीएम++ में क्लास और इनहेरिटेंस के साथ पारंपरिक ऑब्जेक्ट-ओरिएंटेड संरचना तंत्र है। | |||
====वीडीएम-एसएल में संरचना==== | ====वीडीएम-एसएल में संरचना==== | ||
वीडीएम-एसएल के लिए आईएसओ मानक में | वीडीएम-एसएल के लिए आईएसओ मानक में सूचनात्मक अनुबंध है जिसमें विभिन्न संरचना सिद्धांत सम्मिलित हैं। ये सभी मॉड्यूल के साथ पारंपरिक जानकारी छिपाने के सिद्धांतों का पालन करते हैं और इन्हें इस टाइप कॉम्प्रिहेंशनाया जा सकता है: | ||
* मॉड्यूल नामकरण: प्रत्येक मॉड्यूल वाक्यात्मक रूप से कीवर्ड से | * मॉड्यूल नामकरण: प्रत्येक मॉड्यूल वाक्यात्मक रूप से कीवर्ड से प्रारंभ होता है <code>module</code> इसके पश्चात् मॉड्यूल का नाम आता है। मॉड्यूल के अंत में कीवर्ड <code>end</code> मॉड्यूल के नाम के पश्चात् फिर से लिखा गया है। | ||
* आयात करना: अन्य मॉड्यूल से निर्यात की गई | * आयात करना: अन्य मॉड्यूल से निर्यात की गई डिफ्निसन ओं को आयात करना संभव है। यह ''आयात अनुभाग'' में किया जाता है जिसकी प्रारंभिक कीवर्ड से होती है <code>imports</code> और उसके पश्चात् विभिन्न मॉड्यूल से आयात का क्रम चलता है। इनमें से प्रत्येक मॉड्यूल आयात कीवर्ड से प्रारंभ होता है <code>from</code> उसके पश्चात् मॉड्यूल का नाम और मॉड्यूल हस्ताक्षर आता है। मॉड्यूल हस्ताक्षर या तो केवल कीवर्ड हो सकता है <code>all</code> उस मॉड्यूल से निर्यात की गई सभी डिफ्निसन ओं के आयात को निरुपित करना, या यह आयात हस्ताक्षरों का क्रम हो सकता है। आयात हस्ताक्षर प्रकार, मान, फ़ंक्शन और संचालन के लिए विशिष्ट होते हैं और इनमें से प्रत्येक संबंधित कीवर्ड से प्रारंभ होते हैं। इसके अतिरिक्त ये आयात हस्ताक्षर उन निर्माणों का नाम देते हैं जिन तक पहुंच प्राप्त करने की इच्छा है। इसके अतिरिक्त वैकल्पिक टाइप की जानकारी उपस्थित हो सकती है और अंततः आयात पर प्रत्येक निर्माण का नाम परिवर्तित करना संभव है। टाइप के लिए कीवर्ड का भी उपयोग करना होगा <code>struct</code> यदि कोई किसी विशेष टाइप की आंतरिक संरचना तक पहुंच प्राप्त करना चाहता है। | ||
* 'निर्यात': | * 'निर्यात': मॉड्यूल की डिफ्निसन, जिन तक कोई अन्य मॉड्यूल की पहुंच चाहता है, कीवर्ड का उपयोग करके निर्यात की जाती हैं <code>exports</code> इसके पश्चात् निर्यात मॉड्यूल हस्ताक्षर होगा। निर्यात मॉड्यूल हस्ताक्षर में या तो केवल कीवर्ड सम्मिलित हो सकता है <code>all</code> या निर्यात हस्ताक्षरों के अनुक्रम के रूप में। ऐसे निर्यात हस्ताक्षर प्रकार, मान, फ़ंक्शन और संचालन के लिए विशिष्ट होते हैं और इनमें से प्रत्येक संबंधित कीवर्ड से प्रारंभ होते हैं। यदि कोई किसी टाइप की कीवर्ड की आंतरिक संरचना को निर्यात करना चाहता है <code>struct</code> उपयोग किया जाना चाहिए। | ||
* अधिक विदेशी विशेषताएं: वीडीएम-एसएल टूल के पुराने संस्करणों में पैरामीटरयुक्त मॉड्यूल और ऐसे मॉड्यूल के इंस्टेंटेशन के लिए भी समर्थन था। | * अधिक विदेशी विशेषताएं: वीडीएम-एसएल टूल के पुराने संस्करणों में पैरामीटरयुक्त मॉड्यूल और ऐसे मॉड्यूल के इंस्टेंटेशन के लिए भी समर्थन था। चूँकि , इन सुविधाओं को 2000 के आसपास वीडीएमटूल्स से हटा दिया गया था क्योंकि इनका उपयोग संभवतः ही कभी औद्योगिक अनुप्रयोगों में किया गया था और इन सुविधाओं के साथ बड़ी संख्या में टूल चुनौतियाँ थीं। | ||
=== | === वीडीएम++ में संरचना === | ||
वीडीएम++ में क्लास और एकाधिक इनहेरिटेंस का उपयोग करके संरचना की जाती है। प्रमुख अवधारणाएँ हैं: | |||
* क्लास: प्रत्येक क्लास वाक्यात्मक रूप से कीवर्ड से | * क्लास: प्रत्येक क्लास वाक्यात्मक रूप से कीवर्ड से प्रारंभ होती है <code>class</code> इसके पश्चात् वर्ग का नाम आता है। कक्षा के अंत में कीवर्ड <code>end</code> इसके पश्चात् फिर से कक्षा का नाम लिखा जाता है। | ||
* | * इनहेरिटेंस: यदि किसी वर्ग को अन्य वर्गों से संरचनाएं इनहेरिटेंस में मिलती हैं तो वर्ग शीर्षक में वर्ग नाम के पश्चात् कीवर्ड का उपयोग किया जा सकता है <code>is subclass of</code> उसके पश्चात् सुपरक्लास के नामों की अल्पविराम से अलग की गई सूची। | ||
* एक्सेस संशोधक: | * एक्सेस संशोधक: वीडीएम++ में जानकारी हिडेन करना उसी तरह से किया जाता है जैसे अधिकांश ऑब्जेक्ट ओरिएंटेड लैंग्वेज ओं में एक्सेस संशोधक का उपयोग करके किया जाता है। वीडीएम++ में डिफ्निसन एँ डिफ़ॉल्ट रूप से निजी होती हैं किंतु सभी डिफ्निसन ओं के सामने एक्सेस संशोधक कीवर्ड <code>private</code>, <code>public</code> और <code>protected</code> में से किसी का उपयोग करना संभव है:. | ||
==मॉडलिंग कार्यक्षमता== | ==मॉडलिंग कार्यक्षमता== | ||
| Line 216: | Line 222: | ||
===कार्यात्मक मॉडलिंग=== | ===कार्यात्मक मॉडलिंग=== | ||
वीडीएम-एसएल में, फ़ंक्शन को मॉडल में परिभाषित डेटा | वीडीएम-एसएल में, फ़ंक्शन को मॉडल में परिभाषित डेटा टाइप पर परिभाषित किया जाता है। एब्सट्रक्टन के लिए समर्थन के लिए आवश्यक है कि किसी फ़ंक्शन की गणना किए जाने वाले परिणाम को चिह्नित करना संभव हो, बिना यह बताए कि इसकी गणना कैसे की जानी चाहिए। ऐसा करने का मुख्य तंत्र अंतर्निहित फ़ंक्शन डिफ्निसन है, जिसमें किसी परिणाम की गणना करने वाले सूत्र के अतिरिक्त, इनपुट और परिणाम वेरिएबल पर लॉजिक विधेय, जिसे पोस्टकंडिशन कहा जाता है, परिणाम के गुण देता है। उदाहरण के लिए, फ़ंक्शन <code>SQRT</code> किसी प्राकृत संख्या के वर्गमूल की गणना के लिए इसे इस टाइप परिभाषित किया जा सकता है: | ||
SQRT(x:nat)r: | SQRT(x:nat)r:real | ||
post r*r = x | |||
यहां पोस्टकंडिशन परिणाम की गणना के लिए | यहां पोस्टकंडिशन परिणाम की गणना के लिए मेथड <code>r</code> परिभाषित नहीं करता है किंतु यह बताता है कि इसके पास कौन से गुण माने जा सकते हैं। ध्यान दें कि यह फ़ंक्शन को परिभाषित करता है जो वैध वर्गमूल लौटाता है; इसकी कोई आवश्यकता नहीं है कि यह धनात्मक या ऋणात्मक मूल होना चाहिए। उपरोक्त स्पेसिफिकेशन संतुष्ट होंगे, उदाहरण के लिए फ़ंक्शन द्वारा जो 4 का ऋणात्मक मूल किंतु अन्य सभी वैध इनपुट का धनात्मक मूल लौटाता है। ध्यान दें कि वीडीएम-एसएल में फ़ंक्शंस को नियतात्मक होना आवश्यक है जिससे ऊपर दिए गए उदाहरण स्पेसिफिकेशन को संतुष्ट करने वाला फ़ंक्शन सदैव समान इनपुट के लिए समान परिणाम लौटाए गए। | ||
पोस्टकंडीशन को | पोस्टकंडीशन को प्रबल करके अधिक बाधित फ़ंक्शन स्पेसिफिकेशन प्राप्त किया जाता है। उदाहरण के लिए, निम्नलिखित डिफ्निसन फ़ंक्शन को धनात्मक रूट वापस करने के लिए बाध्य करती है। | ||
SQRT(x:nat)r: | SQRT(x:nat)r:real | ||
post r*r = x and r>=0 | |||
सभी फ़ंक्शन | सभी फ़ंक्शन स्पेसिफिकेशन को उन पूर्व नियमो द्वारा प्रतिबंधित किया जा सकता है जो केवल इनपुट वेरिएबल पर लॉजिक विधेय हैं और जो उन बाधाओं का वर्णन करते हैं जिन्हें फ़ंक्शन निष्पादित होने पर संतुष्ट माना जाता है। उदाहरण के लिए, वर्गमूल गणना फ़ंक्शन जो केवल धनात्मक वास्तविक संख्याओं पर कार्य करता है, उसे निम्नानुसार निर्दिष्ट किया जा सकता है: | ||
SQRTP(x: | SQRTP(x:real)r:real | ||
pre x >=0 | |||
post r*r = x and r>=0 | |||
पूर्व | पूर्व नियम और उत्तर नियम मिलकर अनुबंध बनाते हैं जिसे फ़ंक्शन को प्रयुक्त करने का दावा करने वाले किसी भी प्रोग्राम द्वारा संतुष्ट किया जाना चाहिए। पूर्व नियम उन धारणाओं को रिकॉर्ड करती है जिसके अनुसार फ़ंक्शन पोस्ट नियम को संतुष्ट करने वाले परिणाम को वापस करने की गारंटी देता है। यदि किसी फ़ंक्शन को ऐसे इनपुट पर कॉल किया जाता है जो उसकी पूर्व नियम को पूरा नहीं करता है, तो परिणाम अपरिभाषित है (वास्तव में, समाप्ति की गारंटी भी नहीं है)। | ||
वीडीएम-एसएल कार्यात्मक प्रोग्रामिंग | वीडीएम-एसएल कार्यात्मक प्रोग्रामिंग लैंग्वेज के मेथड से निष्पादन योग्य कार्यों की डिफ्निसन का भी समर्थन करता है। स्पष्ट फ़ंक्शन डिफ्निसन में, परिणाम को इनपुट पर अभिव्यक्ति के माध्यम से परिभाषित किया जाता है। उदाहरण के लिए, फ़ंक्शन जो संख्याओं की सूची के वर्गों की सूची तैयार करता है, उसे निम्नानुसार परिभाषित किया जा सकता है: | ||
SqList: nat | SqList: seq of nat -> seq of nat | ||
SqList(s) == | SqList(s) == if s = [] then [] else [(hd s)**2] ^ SqList(tl s) | ||
इस पुनरावर्ती | इस पुनरावर्ती डिफ्निसन में फ़ंक्शन हस्ताक्षर होता है जो इनपुट और परिणाम के टाइप और फ़ंक्शन बॉडी देता है। समान फ़ंक्शन की अंतर्निहित डिफ्निसन निम्नलिखित रूप ले सकती है: | ||
SqListImp(s:seq of nat)r:seq of nat | SqListImp(s:seq of nat)r:seq of nat | ||
post len r = len s and | |||
forall i in set inds s & r(i) = s(i)**2 | |||
स्पष्ट | स्पष्ट डिफ्निसन सरल अर्थ में अंतर्निहित रूप से निर्दिष्ट फ़ंक्शन का कार्यान्वयन है। अंतर्निहित स्पेसिफिकेशन के संबंध में स्पष्ट फ़ंक्शन डिफ्निसन की शुद्धता को निम्नानुसार परिभाषित किया जा सकता है। | ||
एक अंतर्निहित | एक अंतर्निहित स्पेसिफिकेशन दी गई: | ||
f(p:T_p)r:T_r | f(p:T_p)r:T_r | ||
pre pre-f(p) | |||
post post-f(p, r) | |||
और | और स्पष्ट कार्य: | ||
f:T_p -> T_r | f:T_p -> T_r | ||
हम कहते हैं कि यह | हम कहते हैं कि यह स्पेसिफिकेशन को पूरा करता है यदि: | ||
forall p in set T_p & pre-f(p) => f(p):T_r and post-f(p, f(p)) | |||
इसलिए,<code>f</code> | |||
इसलिए,<code>f</code> सही कार्यान्वयन है के रूप में व्याख्या की जानी चाहिए<code>f</code> स्पेसिफिकेशन को पूरा करता है. | |||
=== | ===स्टेट-बेस्ड मॉडलिंग=== | ||
वीडीएम-एसएल में, फ़ंक्शंस के दुष्प्रभाव नहीं होते हैं जैसे कि | वीडीएम-एसएल में, फ़ंक्शंस के दुष्प्रभाव नहीं होते हैं जैसे कि निरंतर ग्लोबल वेरिएबल की स्थिति को परिवर्तित करना। यह कई प्रोग्रामिंग लैंग्वेज ओं में उपयोगी क्षमता है, इसलिए समान अवधारणा उपस्थित है; फ़ंक्शंस के अतिरिक्त , ऑपरेशन का उपयोग 'स्टेट वेरिएबल्स' (जिसे ग्लोबल्स के रूप में भी जाना जाता है) को बदलने के लिए किया जाता है। | ||
उदाहरण के लिए, यदि हमारे पास | उदाहरण के लिए, यदि हमारे पास एकल वेरिएबल से युक्त स्टेट है <code>someStateRegister : nat</code>, हम इसे वीडीएम-एसएल में इस टाइप परिभाषित कर सकते हैं: | ||
state Register of | |||
someStateRegister : nat | |||
end | |||
इसके | इसके अतिरिक्त वीडीएम++ में इसे इस टाइप परिभाषित किया जाएगा: | ||
instance variables | |||
someStateRegister : nat | |||
इस वेरिएबल में मान लोड करने के लिए | इस वेरिएबल में मान लोड करने के लिए ऑपरेशन को इस टाइप निर्दिष्ट किया जा सकता है: | ||
LOAD(i:nat) | |||
ext wr someStateRegister:nat | ext wr someStateRegister:nat | ||
post someStateRegister = i | |||
बाहरी खंड (<code>ext</code>) निर्दिष्ट करता है कि ऑपरेशन द्वारा | बाहरी खंड (<code>ext</code>) निर्दिष्ट करता है कि ऑपरेशन द्वारा स्टेट के किन भागो तक पहुँचा जा सकता है; <code>rd</code> केवल-पठन पहुंच का संकेत और <code>wr</code> पढ़ने/लिखने की पहुंच। | ||
कभी-कभी किसी | कभी-कभी किसी स्टेट को संशोधित करने से पहले उसके मूल्य का उल्लेख करना महत्वपूर्ण होता है; उदाहरण के लिए, वैरिएबल में मान जोड़ने के लिए ऑपरेशन को इस टाइप निर्दिष्ट किया जा सकता है: | ||
ADD(i:nat) | |||
ext wr | ext wr someStateRegister : nat | ||
someStateRegister = someStateRegister~ + i | post someStateRegister = someStateRegister~ + i | ||
जहां <code>~</code> पोस्टकंडिशन में स्टेट वेरिएबल पर प्रतीक ऑपरेशन के निष्पादन से पहले स्टेट वेरिएबल का मान | जहां <code>~</code> पोस्टकंडिशन में स्टेट वेरिएबल पर प्रतीक ऑपरेशन के निष्पादन से पहले स्टेट वेरिएबल का मान निरुपित करता है। | ||
==उदाहरण== | ==उदाहरण== | ||
{{Further| | {{Further|मेटा-IV (विनिर्देश लैंग्वेज) }} | ||
===अधिकतम फ़ंक्शन=== | ===अधिकतम फ़ंक्शन=== | ||
यह | यह अंतर्निहित फ़ंक्शन डिफ्निसन का उदाहरण है। फ़ंक्शन धनात्मक पूर्णांकों के सेट से सबसे बड़ा कॉम्पोनेन्ट लौटाता है: | ||
max(s:set of nat)r:nat | |||
pre card s > 0 | |||
post r in set s and | |||
forall r' in set s & r' <= r | |||
पोस्टकंडिशन परिणाम को प्राप्त करने के लिए एल्गोरिदम को परिभाषित करने के | पोस्टकंडिशन परिणाम को प्राप्त करने के लिए एल्गोरिदम को परिभाषित करने के अतिरिक्त उसे चित्रित करता है। पूर्व नियम की आवश्यकता है क्योंकि सेट रिक्त होने पर कोई भी फ़ंक्शन सेट s में r वापस नहीं कर सकता है। | ||
===प्राकृतिक संख्या गुणन=== | ===प्राकृतिक संख्या गुणन=== | ||
multp(i,j:nat)r:nat | |||
pre true | |||
post r = i*j | |||
प्रमाण दायित्व | प्रमाण दायित्व प्रयुक्त करना <code>forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))</code> की स्पष्ट डिफ्निसन के लिए <code>multp</code>: | ||
multp(i,j) == | |||
if i=0 | |||
then 0 | |||
else if is-even(i) | |||
then 2*multp(i/2,j) | |||
else j+multp(i-1,j) | |||
तब प्रमाण दायित्व बन जाता है: | तब प्रमाण दायित्व बन जाता है: | ||
forall i, j : nat & multp(i,j):nat and multp(i, j) = i*j | |||
इसे इसके द्वारा सही दिखाया जा सकता है: | इसे इसके द्वारा सही दिखाया जा सकता है: | ||
# यह | # यह सिद्ध करना कि पुनरावृत्ति समाप्त हो जाती है (इसके बदले में यह सिद्ध करना आवश्यक है कि संख्याएँ प्रत्येक फेज में छोटी हो जाती हैं) | ||
# [[गणितीय प्रेरण]] | # [[गणितीय प्रेरण]] | ||
=== | ===पंक्ति सार डेटा टाइप === | ||
यह | यह प्रसिद्ध डेटा संरचना के स्टेट -बेस्ड मॉडल में अंतर्निहित ऑपरेशन स्पेसिफिकेशन के उपयोग को दर्शाने वाला मौलिक उदाहरण है। पंक्ति को टाइप के कॉम्पोनेन्टं से बने अनुक्रम के रूप में तैयार किया गया है <code>Qelt</code>. प्रतिनिधित्व है <code>Qelt</code> सारहीन है और इसलिए इसे टोकन टाइप के रूप में परिभाषित किया गया है। | ||
types | |||
Qelt = token; | |||
Queue = seq of Qelt; | |||
state TheQueue of | |||
q : Queue | |||
end | |||
operations | |||
ENQUEUE(e:Qelt) | |||
ext wr q: | ext wr q:Queue | ||
post q = q~ ^ [e]; | |||
DEQUEUE()e:Qelt | DEQUEUE()e:Qelt | ||
ext wr q: | ext wr q:Queue | ||
pre q <> [] | |||
post q~ = [e]^q; | |||
IS-EMPTY()r:bool | |||
ext rd q:Queue | |||
post r <=> (len q = 0) | |||
===बैंक सिस्टम उदाहरण=== | |||
वीडीएम-एसएल मॉडल के बहुत ही सरल उदाहरण के रूप में, ग्राहक बैंक खाते का विवरण बनाए रखने के लिए सिस्टम पर विचार करें। ग्राहकों को ग्राहक संख्या (CustNum) द्वारा मॉडल किया जाता है, खातों को खाता संख्या (AccNum) द्वारा मॉडल किया जाता है। ग्राहक संख्या का प्रतिनिधित्व सारहीन माना जाता है और इसलिए इसे टोकन टाइप के आधार पर तैयार किया जाता है। शेष राशि और ओवरड्राफ्ट को संख्यात्मक टाइप के आधार पर तैयार किया जाता है। | |||
AccNum = | AccNum = token; | ||
CustNum = token; | |||
Balance = int; | |||
Overdraft = nat; | |||
AccData :: owner : CustNum | |||
balance : Balance | |||
state Bank of | |||
accountMap : map AccNum to AccData | |||
overdraftMap : map CustNum to Overdraft | |||
inv mk_Bank( | inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and | ||
a.balance >= -overdraftMap(a.owner) | |||
संचालन के साथ: | संचालन के साथ: | ||
एनईडब्ल्यूसी नया ग्राहक नंबर आवंटित करता है: | |||
NEWC( | |||
ext wr | operations | ||
NEWC(od : Overdraft)r : CustNum | |||
ext wr overdraftMap : map CustNum to Overdraft | |||
post r not in set dom ~overdraftMap and overdraftMap = ~overdraftMap ++ { r |-> od}; | |||
एनईडब्ल्यूएसी नया खाता नंबर आवंटित करता है और शेष राशि को शून्य पर सेट करता है: | |||
NEWAC( | NEWAC(cu : CustNum)r : AccNum | ||
ext wr | ext wr accountMap : map AccNum to AccData | ||
rd overdraftMap map CustNum to Overdraft | |||
pre cu in set dom overdraftMap | |||
post r not in set dom accountMap~ and accountMap = accountMap~ ++ {r|-> mk_AccData(cu,0)} | |||
एसीआईएनएफ ग्राहक के सभी खातों की सभी शेष राशि, शेष राशि के खाता संख्या के मानचित्र के रूप में लौटाता है: | |||
ACINF( | ACINF(cu : CustNum)r : map AccNum to Balance | ||
ext rd accountMap : map AccNum to AccData | |||
post r = {an |-> accountMap(an).balance | an in set dom accountMap & accountMap(an).owner = cu} | |||
==उपकरण समर्थन== | ==उपकरण समर्थन== | ||
कई अलग-अलग उपकरण | कई अलग-अलग उपकरण वीडीएम का समर्थन करते हैं: | ||
* [http://www.vdmtools.jp/en | * [http://www.vdmtools.jp/en वीडीएमटूल्स] वीडीएम और वीडीएम++ के लिए अग्रणी व्यावसायिक उपकरण था, जिसका स्वामित्व, विपणन, रखरखाव और डेवलपमेंट [http://www.csk.com CSK Systems] द्वारा किया गया था, जो डेनिश कंपनी आईएफएडी द्वारा विकसित पुराने संस्करणों पर बेस्ड था। [http://www.vdmtools.jp/en/modules/tinyd2/index.php?id=2 मैनुअल] और व्यावहारिक [http://www.vdmportal.org/twiki/pub/Main/WebHome/tutorial1.pdf ट्यूटोरियल] उपलब्ध हैं। टूल के पूर्ण संस्करण के लिए सभी लाइसेंस निःशुल्क उपलब्ध हैं। पूर्ण संस्करण में जावा और सी++ के लिए स्वचालित कोड जनरेशन, डायनेमिक लिंक लाइब्रेरी और कोरबा समर्थन सम्मिलित है। | ||
* [http://www.overturetool.org/ | * [http://www.overturetool.org/ ओवर]वेरिएबल समुदाय-बेस्ड ओपन सोर्स पहल है जिसका उद्देश्य सभी वीडीएम बोलियों (वीडीएम-एसएल, वीडीएम++ और वीडीएम-आरटी) के लिए मूल रूप से एक्लिप्स प्लेटफॉर्म के शीर्ष पर किंतु पश्चात् में विजुअल स्टूडियो कोड प्लेटफॉर्म के शीर्ष पर स्वतंत्र रूप से उपलब्ध टूल समर्थन प्रदान करना है। इसका उद्देश्य इंटरऑपरेबल टूल के लिए प्रारूप विकसित करना है जो औद्योगिक अनुप्रयोग, अनुसंधान और शिक्षा के लिए उपयोगी होगा। | ||
* [https://github.com/peterwvj/vdm-mode | * [https://github.com/peterwvj/vdm-mode वीडीएम-mode] वीडीएम-एसएल, वीडीएम++ और वीडीएम-आरटी का उपयोग करके वीडीएम स्पेसिफिकेशन लिखने के लिए इमैक्स पैकेजों का स्टोर है। यह सिंटैक्स हाइलाइटिंग और संपादन, ऑन-द-फ्लाई सिंटैक्स चेकिंग, टेम्पलेट पूर्णता और इन्टेरोपेराबल समर्थन का समर्थन करता है। | ||
* [http://www.adelard.com/web/hnav/services/SoftwareTools/SpecBox/index.html SpecBox]: एडेलार्ड से सिंटैक्स जांच, कुछ सरल सिमेंटिक जांच और | * [http://www.adelard.com/web/hnav/services/SoftwareTools/SpecBox/index.html SpecBox]: एडेलार्ड से सिंटैक्स जांच, कुछ सरल सिमेंटिक जांच और [[LaTeX]] फ़ाइल का निर्माण प्रदान किया जाता है, जो स्पेसिफिकेशन को गणितीय नोटेशन में मुद्रित करने में सक्षम बनाता है। यह उपकरण निःशुल्क उपलब्ध है किंतु इसका रखरखाव नहीं किया जा रहा है। | ||
* आईएसओ मानक | * आईएसओ मानक लैंग्वेज के गणितीय वाक्यविन्यास में वीडीएम मॉडल की प्रस्तुति का समर्थन करने के लिए LaTeX और LaTeX2e मैक्रोज़ उपलब्ध हैं। इन्हें यूके में राष्ट्रीय भौतिक प्रयोगशाला द्वारा विकसित और रखरखाव किया गया है। [http://ftp.npl.co.uk/pub/latex/macros/vdm-sl/README डॉक्यूमेंटीकरण] और [http://ftp.npl.co.uk/pub/latex/macros/vdm-sl/ मैक्रोज़] ऑनलाइन उपलब्ध हैं। | ||
==औद्योगिक अनुभव== | ==औद्योगिक अनुभव== | ||
वीडीएम को विभिन्न एप्लिकेशन डोमेन में व्यापक रूप से | वीडीएम को विभिन्न एप्लिकेशन डोमेन में व्यापक रूप से प्रयुक्त किया गया है। इनमें से सबसे प्रसिद्ध अनुप्रयोग हैं: | ||
* Ada (प्रोग्रामिंग | * Ada (प्रोग्रामिंग लैंग्वेज ) और [[CHILL|सीएचआईएलएल]] [[ संकलक |कम्पाइलर]]: पहला यूरोपीय मान्य Ada कंपाइलर वीडीएम का उपयोग करके Dansk डेटामैटिक सेंटर द्वारा विकसित किया गया था।<ref>{{cite journal | title=Retargeting and rehosting the DDC Ada compiler system: A case study – the Honeywell DPS 6 | first=Geert B. | last=Clemmensen | journal=ACM SIGAda Ada Letters | volume=6 | issue=1 | date=January 1986 | pages=22–28|doi = 10.1145/382256.382794| s2cid=16337448 }}</ref> इसी टाइप सीएचआईएलएल और [[Modula-2|मॉड्यूला-2]] के शब्दार्थ को वीडीएम का उपयोग करके उनके मानकों में वर्णित किया गया था। | ||
* कॉनफॉर्म: ब्रिटिश एयरोस्पेस में | * कॉनफॉर्म: ब्रिटिश एयरोस्पेस में प्रयोग जिसमें विश्वसनीय गेटवे के पारंपरिक डेवलपमेंट की तुलना वीडीएम का उपयोग करके किए गए डेवलपमेंट से की गई है। | ||
* धूल-विशेषज्ञ: सुरक्षा संबंधी अनुप्रयोग के लिए [[यूके]] में एडेलार्ड द्वारा चलाया गया | * धूल-विशेषज्ञ: सुरक्षा संबंधी अनुप्रयोग के लिए [[यूके]] में एडेलार्ड द्वारा चलाया गया प्रोजेक्ट जो यह निर्धारित करता है कि औद्योगिक संयंत्रों के लेआउट में सुरक्षा उपयुक्त है। | ||
* | * वीडीएमटूल्स का विकास: वीडीएमटूल्स टूल सूट के अधिकांश घटक स्वयं वीडीएम का उपयोग करके विकसित किए गए हैं। यह डेवलपमेंट [[डेनमार्क]] में [http://www.ifad.dk/ आईएफएडी] और [[जापान]] में [[सीएसके होल्डिंग्स कॉर्पोरेशन]] में किया गया है।<ref>Peter Gorm Larsen, [http://www.jucs.org/jucs_7_8/ten_years_of_historical;internal&action=noaction&Parameter=1189241867787 "Ten Years of Historical Development "Bootstrapping" VDMTools"] {{Webarchive|url=https://web.archive.org/web/20210123052449/http://www.jucs.org/jucs_7_8/ten_years_of_historical%3Binternal%26action%3Dnoaction%26Parameter%3D1189241867787 |date=23 January 2021 }}, In ''Journal of Universal Computer Science'', volume 7(8), 2001</ref> | ||
* ट्रेडवन: जापानी स्टॉक एक्सचेंज के लिए सीएसके सिस्टम द्वारा विकसित ट्रेडवन बैक-ऑफिस सिस्टम के कुछ प्रमुख घटक वीडीएम का उपयोग करके विकसित किए गए थे। पारंपरिक रूप से विकसित कोड बनाम वीडीएम-विकसित घटकों की डेवलपर उत्पादकता और दोष घनत्व के लिए तुलनात्मक माप | * ट्रेडवन: जापानी स्टॉक एक्सचेंज के लिए सीएसके सिस्टम द्वारा विकसित ट्रेडवन बैक-ऑफिस सिस्टम के कुछ प्रमुख घटक वीडीएम का उपयोग करके विकसित किए गए थे। पारंपरिक रूप से विकसित कोड बनाम वीडीएम-विकसित घटकों की डेवलपर उत्पादकता और दोष घनत्व के लिए तुलनात्मक माप उपस्थित हैं। | ||
* फेलिका नेटवर्क्स ने [[सेलुलर टेलीफोन]] अनुप्रयोगों के लिए | * फेलिका नेटवर्क्स ने [[सेलुलर टेलीफोन]] अनुप्रयोगों के लिए एकीकृत सर्किट के लिए [[ऑपरेटिंग सिस्टम]] के डेवलपमेंट की सूचना दी है। | ||
== | ==रेफिनमेन्ट == | ||
वीडीएम का उपयोग | वीडीएम का उपयोग बहुत ही एब्सट्रेक्ट (कंप्यूटर विज्ञान) मॉडल से प्रारंभ होता है और इसे कार्यान्वयन में विकसित करता है। प्रत्येक फेज में डेटा रेफिकेशन , फिर ऑपरेशन अपघटन सम्मिलित है। | ||
डेटा रीफिकेशन [[अमूर्त डेटा प्रकार]] | डेटा रीफिकेशन [[अमूर्त डेटा प्रकार|एब्सट्रेक्ट डेटा]] टाइप को अधिक ठोस [[डेटा संरचना]]ओं में विकसित करता है, जबकि ऑपरेशन अपघटन संचालन और कार्यों के (एब्सट्रक्ट) अंतर्निहित विनिर्देशों को [[कलन विधि|एल्गोरिथ्म]] मेथड में विकसित करता है जिन्हें सीधे पसंद की कंप्यूटर लैंग्वेज में प्रयुक्त किया जा सकता है। | ||
:<math>\begin{array}{|rcl|} | :<math>\begin{array}{|rcl|} | ||
| Line 431: | Line 440: | ||
===डेटा | ===डेटा रीफिकेशन === | ||
डेटा पुनरीक्षण (चरणबद्ध शोधन) में | डेटा पुनरीक्षण (चरणबद्ध शोधन) में स्पेसिफिकेशन में उपयोग किए गए एब्सट्रेक्ट डेटा टाइप का अधिक ठोस प्रतिनिधित्व खोजना सम्मिलित है। कार्यान्वयन तक पहुँचने से पहले कई फेज हो सकते हैं। एब्सट्रेक्ट डेटा प्रतिनिधित्व के लिए प्रत्येक पुनरीक्षण फेज <code>ABS_REP</code> इसमें नया प्रतिनिधित्व प्रस्तावित करना सम्मिलित है <code>NEW_REP</code>. यह दिखाने के लिए कि नया प्रतिनिधित्व स्पष्ट है, पुनर्प्राप्ति फ़ंक्शन परिभाषित किया गया है जो संबंधित है <code>NEW_REP</code> को <code>ABS_REP</code>, अर्थात। <code>retr : NEW_REP -> ABS_REP</code>. डेटा रेफिकेशन की शुद्धता पर्याप्तता सिद्ध करने पर निर्भर करती है, अथार्त । | ||
forall a:ABS_REP & exists r:NEW_REP & a = retr(r) | |||
चूँकि डेटा प्रतिनिधित्व बदल गया है, संचालन और कार्यों को अद्यतन करना आवश्यक है जिससे वे कार्य करते रहें जिससे <code>NEW_REP</code>. नए प्रतिनिधित्व पर किसी भी डेटा टाइप के इनवेरिएंट (कंप्यूटर विज्ञान) को संरक्षित करने के लिए नए संचालन और कार्यों को दिखाया जाना चाहिए। यह सिद्ध करने के लिए कि नए संचालन और फ़ंक्शन मॉडल मूल स्पेसिफिकेशन में पाए गए हैं, दो प्रमाण दायित्वों का निर्वहन करना आवश्यक है: | |||
*डोमेन नियम: | *डोमेन नियम: | ||
forall r: NEW_REP & pre-OPA(retr(r)) => pre-OPR(r) | |||
* मॉडलिंग नियम: | * मॉडलिंग नियम: | ||
* | |||
forall ~r,r:NEW_REP & pre-OPA(retr(~r)) and post-OPR(~r,r) => post-OPA(retr(~r,), retr(r)) | |||
====उदाहरण डेटा | ====उदाहरण डेटा रेफिकेशन ==== | ||
व्यवसाय सुरक्षा | व्यवसाय सुरक्षा सिस्टम में, श्रमिकों को आईडी कार्ड दिए जाते हैं; इन्हें फ़ैक्टरी में प्रवेश करने और बाहर निकलने पर कार्ड रीडर में फीड किया जाता है। संचालन आवश्यक:' | ||
संचालन आवश्यक: | * <code>INIT()</code> सिस्टम को इनिशियलाइज़ करता है, मानता है कि फ़ैक्टरी रिक्त है | ||
* <code>INIT()</code> सिस्टम को इनिशियलाइज़ करता है, मानता है कि फ़ैक्टरी | * <code>ENTER(p : Person)</code> रिकॉर्ड करता है कि एम्प्लोयी फ़ैक्टरी में प्रवेश कर रहा है; श्रमिकों का विवरण आईडी कार्ड से पढ़ा जाता है) | ||
* <code>ENTER(p : Person)</code> रिकॉर्ड करता है कि | * <code>EXIT(p : Person)</code> रिकॉर्ड करता है कि एम्प्लोयी फ़ैक्टरी से बाहर निकल रहा है | ||
* <code>EXIT(p : Person)</code> रिकॉर्ड करता है कि | * <code>IS-PRESENT(p : Person) r : bool</code> यह देखने के लिए जाँच करता है कि कोई निर्दिष्ट एम्प्लोयी फ़ैक्टरी में है या नहीं | ||
* <code>IS-PRESENT(p : Person) r : bool</code> यह देखने के लिए जाँच करता है कि कोई निर्दिष्ट | |||
फॉर्मल रूप से, यह होगा: | |||
types | |||
Person = token; | |||
Workers = set of Person; | |||
state AWCCS of | |||
pres: Workers | |||
end | |||
operations | |||
INIT() | |||
ext wr pres: Workers | |||
post pres = {}; | |||
ENTER(p : Person) | |||
ext wr pres : Workers | |||
pre p not in set pres | |||
post pres = pres~ union {p}; | |||
EXIT(p : Person) | |||
ext wr pres : Workers | |||
pre p in set pres | |||
post pres = pres~\{p}; | |||
IS-PRESENT(p : Person) r : bool | |||
ext rd pres : Workers | |||
सेट | post r <=> p in set pres~ | ||
चूँकि अधिकांश प्रोग्रामिंग लैंग्वेज ओं में सेट ( अधिकांशतः सरणी के रूप में) की तुलना में अवधारणा होती है, स्पेसिफिकेशन से पहला कदम अनुक्रम के कॉन्टेक्स्ट में डेटा का प्रतिनिधित्व करना है। इन अनुक्रमों को पुनरावृत्ति की अनुमति नहीं देनी चाहिए, क्योंकि हम नहीं चाहते कि ही कार्यकर्ता दो बार दिखाई दे, इसलिए हमें नए डेटा टाइप में इनवेरिएंट (कंप्यूटर विज्ञान) जोड़ना होगा। इस स्थिति में, ऑर्डर देना महत्वपूर्ण नहीं है, इसलिए <code>[a,b]</code> वैसा ही है जैसा कि <code>[b,a]</code>.के समान है। | |||
वियना डेवलपमेंट पद्धति मॉडल-बेस्ड सिस्टम्स के लिए मूल्यवान है। यदि व्यवस्था समय बेस्ड है तो यह उचित नहीं है। ऐसे स्थितियों के लिए, [[संचार प्रणालियों की गणना|कम्युनिकेटिंग सिस्टम्स की गणना]] (सीसीएस) अधिक उपयोगी है। | |||
वियना | |||
==यह भी देखें== | ==यह भी देखें== | ||
* | * फॉर्मल मेथड्स | ||
* [[औपचारिक विशिष्टता]] | * [[औपचारिक विशिष्टता|फॉर्मल]] [[Z विशिष्टता भाषा|स्पेसिफिकेशन]] | ||
* [[पिजिन कोड]] | * [[पिजिन कोड]] | ||
* [[विधेय तर्क]] | * [[विधेय तर्क|विधेय लॉजिक]] | ||
* [[प्रस्तावात्मक कलन]] | * [[प्रस्तावात्मक कलन|प्रस्तावात्मक एल्गोरिथ्म]] | ||
* [[Z विशिष्टता भाषा]], | * [[Z विशिष्टता भाषा|जेड स्पेसिफिकेशन लैंग्वेज]] , वीडीएम-एसएल का मुख्य विकल्प (तुलना करें) | ||
* [http://www.compass-research.eu/approach.html कम्पास मॉडलिंग | * [http://www.compass-research.eu/approach.html कम्पास मॉडलिंग लैंग्वेज] {{Webarchive|url=https://web.archive.org/web/20200219205126/http://www.compass-research.eu/approach.html |date=19 February 2020 }} (सीएमएल), [[प्रोग्रामिंग के एकीकृत सिद्धांत]] पर बेस्ड संचार अनुक्रमिक प्रक्रियाओं के साथ वीडीएम-एसएल का संयोजन, सिस्टम ऑफ मॉडलिंग (एसओएस) के लिए विकसित किया गया है। | ||
==अग्रिम पठन== | ==अग्रिम पठन== | ||
| Line 500: | Line 509: | ||
* [[John Fitzgerald (computer scientist)|Fitzgerald, J.S.]] and Larsen, P.G., ''Modelling Systems: Practical Tools and Techniques in Software Engineering''. [[Cambridge University Press]], 1998 {{ISBN|0-521-62348-0}} (Japanese Edition pub. [[Iwanami Shoten]] 2003 {{ISBN|4-00-005609-3}}).<ref>[http://www.csr.ncl.ac.uk/modelling-book/ ''Modelling Systems: Practical Tools and Techniques in Software Engineering'']</ref> | * [[John Fitzgerald (computer scientist)|Fitzgerald, J.S.]] and Larsen, P.G., ''Modelling Systems: Practical Tools and Techniques in Software Engineering''. [[Cambridge University Press]], 1998 {{ISBN|0-521-62348-0}} (Japanese Edition pub. [[Iwanami Shoten]] 2003 {{ISBN|4-00-005609-3}}).<ref>[http://www.csr.ncl.ac.uk/modelling-book/ ''Modelling Systems: Practical Tools and Techniques in Software Engineering'']</ref> | ||
* [[John Fitzgerald (computer scientist)|Fitzgerald, J.S.]], Larsen, P.G., Mukherjee, P., Plat, N. and Verhoef,M., ''Validated Designs for Object-oriented Systems''. [[Springer Verlag]] 2005. {{ISBN|1-85233-881-4}}. Supporting web site [http://www.vdmbook.com] includes examples and free tool support.<ref>[http://www.vdmbook.com/ ''Validated Designs for Object-oriented Systems'']</ref> | * [[John Fitzgerald (computer scientist)|Fitzgerald, J.S.]], Larsen, P.G., Mukherjee, P., Plat, N. and Verhoef,M., ''Validated Designs for Object-oriented Systems''. [[Springer Verlag]] 2005. {{ISBN|1-85233-881-4}}. Supporting web site [http://www.vdmbook.com] includes examples and free tool support.<ref>[http://www.vdmbook.com/ ''Validated Designs for Object-oriented Systems'']</ref> | ||
* [[Cliff Jones (computer scientist)|Jones, C.B.]], ''Systematic Software Development using | * [[Cliff Jones (computer scientist)|Jones, C.B.]], ''Systematic Software Development using वीडीएम'', [[Prentice Hall]] 1990. {{ISBN|0-13-880733-7}}. Also available on-line and free of charge: [http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip http://www.csr.ncl.ac.uk/वीडीएम/ssdवीडीएम.pdf.zip] | ||
* [[Dines Bjørner|Bjørner, D.]] and [[Cliff Jones (computer scientist)|Jones, C.B.]], ''Formal Specification and Software Development'' [[Prentice Hall]] International, 1982. {{ISBN|0-13-880733-7}} | * [[Dines Bjørner|Bjørner, D.]] and [[Cliff Jones (computer scientist)|Jones, C.B.]], ''Formal Specification and Software Development'' [[Prentice Hall]] International, 1982. {{ISBN|0-13-880733-7}} | ||
* J. Dawes, ''The | * J. Dawes, ''The वीडीएम-एसएल Reference Guide'', [[Pitman (publisher)|Pitman]] 1991. {{ISBN|0-273-03151-1}} | ||
* [[International Organization for Standardization]], ''Information technology – Programming languages, their environments and system software interfaces – Vienna Development Method – Specification Language – Part 1: Base language'' International Standard | * [[International Organization for Standardization]], ''Information technology – Programming languages, their environments and system software interfaces – Vienna Development Method – Specification Language – Part 1: Base language'' International Standard आईएसओ/IEC 13817-1, December 1996. | ||
* [[Cliff Jones (computer scientist)|Jones, C.B.]], ''Software Development: A Rigorous Approach'', Prentice Hall International, 1980. {{ISBN|0-13-821884-6}} | * [[Cliff Jones (computer scientist)|Jones, C.B.]], ''Software Development: A Rigorous Approach'', Prentice Hall International, 1980. {{ISBN|0-13-821884-6}} | ||
* [[Cliff Jones (computer scientist)|Jones, C.B.]] and Shaw, R.C. (eds.), ''Case Studies in Systematic Software Development'', Prentice Hall International, 1990. {{ISBN|0-13-880733-7}} | * [[Cliff Jones (computer scientist)|Jones, C.B.]] and Shaw, R.C. (eds.), ''Case Studies in Systematic Software Development'', Prentice Hall International, 1990. {{ISBN|0-13-880733-7}} | ||
* Bicarregui, J.C., [[John Fitzgerald (computer scientist)|Fitzgerald, J.S.]], Lindsay, P.A., Moore, R. and Ritchie, B., ''Proof in | * Bicarregui, J.C., [[John Fitzgerald (computer scientist)|Fitzgerald, J.S.]], Lindsay, P.A., Moore, R. and Ritchie, B., ''Proof in वीडीएम: a Practitioner's Guide''. [[Springer Verlag]] Formal Approaches to Computing and Information Technology (FACIT), 1994. {{ISBN|3-540-19813-X}} . | ||
== | ==कॉन्टेक्स्ट== | ||
{{reflist|30em}} | {{reflist|30em}} | ||
==बाहरी संबंध== | ==बाहरी संबंध== | ||
* [https://web.archive.org/web/20080828013815/http://www.vdmportal.org/ Information on | * [https://web.archive.org/web/20080828013815/http://www.vdmportal.org/ Information on वीडीएम and वीडीएम++ (archived copy at archive.org)] | ||
* [http://hopl.murdoch.edu.au/showlanguage2.prx?exp=598 Vienna Definition Language (VDL)] | * [http://hopl.murdoch.edu.au/showlanguage2.prx?exp=598 Vienna Definition Language (VDL)] | ||
[[Category: | [[Category:Articles with hatnote templates targeting a nonexistent page]] | ||
[[Category:Created On 25/07/2023]] | [[Category:Created On 25/07/2023]] | ||
[[Category:Lua-based templates]] | |||
[[Category:Machine Translated Page]] | |||
[[Category:Pages with script errors]] | |||
[[Category:Pages with syntax highlighting errors]] | |||
[[Category:Short description with empty Wikidata description]] | |||
[[Category:Templates Vigyan Ready]] | |||
[[Category:Templates that add a tracking category]] | |||
[[Category:Templates that generate short descriptions]] | |||
[[Category:Templates using TemplateData]] | |||
[[Category:Webarchive template wayback links]] | |||
[[Category:औपचारिक तरीके]] | |||
[[Category:औपचारिक विशिष्टता भाषाएँ]] | |||
Latest revision as of 10:47, 14 August 2023
वियना डेवलपमेंट मेथड (वीडीएम) कंप्यूटर-बेस्ड सिस्टम्स के डेवलपमेंट के लिए सबसे लंबे समय से स्थापित फॉर्मल मेथड में से है। आईबीएम प्रयोगशाला वियना में किए गए कार्य से उत्पन्न [1] 1970 के दशक में, यह फॉर्मल स्पेसिफिकेशन लैंग्वेज -वीडीएम स्पेसिफिकेशन लैंग्वेज (वीडीएम-एसएल) पर बेस्ड तकनीकों और उपकरणों के समूह को सम्मिलित करने के लिए विकसित हुआ है। इसका विस्तारित रूप है, वीडीएम++,[2] जो ऑब्जेक्ट-ओरिएंटेड और कांकररेंट सिस्टम्स के मॉडलिंग का समर्थन करता है। वीडीएम के समर्थन में मॉडलों का विश्लेषण करने के लिए वाणिज्यिक और अकादमिक उपकरण सम्मिलित हैं, जिसमें मॉडलों के गुणों का परीक्षण और सिद्ध करने और मान्य वीडीएम मॉडल से प्रोग्राम कोड उत्पन्न करने के लिए समर्थन सम्मिलित है। वीडीएम और उसके उपकरणों के औद्योगिक उपयोग का इतिहास है और फॉर्मल में अनुसंधान के बढ़ते समूह ने महत्वपूर्ण सिस्टम्स, संएल्गोरिथ्म कर्ता, कांकररेंट सिस्टम्स की इंजीनियरिंग और कंप्यूटर विज्ञान के लिए लॉजिक में उल्लेखनीय योगदान दिया है।
फिलोसॉफी
प्रोग्रामिंग लैंग्वेज ओं का उपयोग करके प्राप्त करने योग्य की तुलना में कंप्यूटिंग सिस्टम को वीडीएम-एसएल में एब्सट्रेक्शन के उच्च स्तर पर मॉडलिंग किया जा सकता है, जिससे सिस्टम डेवलपमेंट के प्रारंभिक फेज में डिज़ाइन के विश्लेषण और दोषों सहित प्रमुख विशेषताओं की पहचान की अनुमति मिलती है। जिन मॉडलों को मान्य किया गया है उन्हें शोधन प्रक्रिया के माध्यम से विस्तृत सिस्टम डिज़ाइन में परिवर्तित किया जा सकता है। लैंग्वेज में फॉर्मल शब्दार्थ है, जो उच्च स्तर के आश्वासन के लिए मॉडल के गुणों का प्रमाण देना संभव बनाता है। इसमें निष्पादन योग्य सबसेट भी है, जिससे मॉडल का परीक्षण करके विश्लेषण किया जा सकता है और ग्राफिकल यूजर इंटरफेस के माध्यम से निष्पादित किया जा सकता है, जिससे मॉडल का मूल्यांकन उन विशेषज्ञों द्वारा किया जा सके जो आवश्यक रूप से मॉडलिंग लैंग्वेज से परिचित नहीं हैं।
इतिहास
वीडीएम-एसएल की उत्पत्ति वियना में आईबीएम प्रयोगशाला में हुई जहां लैंग्वेज के पहले संस्करण को वियना डेफिनिशन लैंग्वेज (वीडीएल) कहा जाता था।[3] वीडीएल का उपयोग अनिवार्य रूप से वीडीएम - मेटा-IV के विपरीत ऑपरेशनल सेमांटिक्स डिस्क्रिप्शन देने के लिए किया गया था, जो डिनोटैस्नल सेमांटिक्स प्रदान करता था।[4]
«1972 के अंत में वियना समूह ने फिर से लैंग्वेज डिफ्निसन से कम्पाइलर को व्यवस्थित रूप से विकसित करने की समस्या पर अपना ध्यान केंद्रित किया था। अपनाए गए समग्र दृष्टिकोण को वियना डेवलपमेंट मेथड कहा गया है ... वास्तव में अपनाई गई मेटा-लैंग्वेज (मेटा-IV) का उपयोग पीएल/1 के प्रमुख भागो को परिभाषित करने के लिए किया जाता है (जैसा कि ईसीएमए 74 में दिया गया है - रौचक बात यह है कि एब्सट्रेक्ट इंटरप्रेटर के रूप में लिखा गया फॉर्मल मानक डॉक्यूमेंट ) BEKIČ 74 में।[5]
मेटा-IV के बीच कोई संबंध नहीं है,[6] और शोर्रे की मेटा II लैंग्वेज , या इसकी उत्तराधिकारी ट्री मेटा ; ये फॉर्मल समस्या विवरण के लिए उपयुक्त होने के अतिरिक्त कम्पाइलर -कम्पाइलर सिस्टम थे।
इसलिए मेटा-IV का उपयोग पीएल/आई प्रोग्रामिंग लैंग्वेज के प्रमुख भागों को परिभाषित करने के लिए किया गया था। मेटा-IV और वीडीएम-एसएल का उपयोग करके पूर्वव्यापी रूप से वर्णित या आंशिक रूप से वर्णित अन्य प्रोग्रामिंग लैंग्वेज ओं में बेसिक प्रोग्रामिंग लैंग्वेज , फोरट्रान, एपीएल प्रोग्रामिंग लैंग्वेज ,एल्गोल 60, एडा प्रोग्रामिंग लैंग्वेज और पास्कल प्रोग्रामिंग लैंग्वेज सम्मिलित हैं। मेटा-IV कई टाइप में विकसित हुआ, जिन्हें समान्यत: डेनिश, अंग्रेजी और आयरिश स्कूलों के रूप में वर्णित किया गया है।
इंग्लिश स्कूल वीडीएम के उन मेथड पर क्लिफ जोन्स (कंप्यूटर वैज्ञानिक) के कार्य से प्राप्त हुआ है जो विशेष रूप से लैंग्वेज डिफ्निसन और कंपाइलर डिजाइन से संबंधित नहीं हैं (जोन्स 1980, 1990)। यह निरंतर मॉडलिंग पर बल देता है [7] आधार टाइप के समृद्ध स्टोर से निर्मित डेटा टाइप के उपयोग के माध्यम से बताएं। कार्यक्षमता को समान्यत: उन ऑपरेशन के माध्यम से वर्णित किया जाता है जिनके स्टेट पर दुष्प्रभाव हो सकते हैं और जो अधिकतर पूर्व नियम और पोस्टकंडिशन का उपयोग करके अंतर्निहित रूप से निर्दिष्ट होते हैं। डेनिश स्कूल (डाइन्स ब्योर्नर या ब्योर्नर एट अल. 1982) ने अधिक सीमा तक उपयोग किए जाने वाले स्पष्ट परिचालन स्पेसिफिकेशन के साथ रचनात्मक दृष्टिकोण पर बल दिया है। डेनिश स्कूल में कार्य करने से पहला यूरोपीय मान्य एडा प्रोग्रामिंग लैंग्वेज कंपाइलर तैयार हुआ था।
लैंग्वेज के लिए मानकीकरण मानक के लिए अंतर्राष्ट्रीय संगठन 1996 में प्रारंभ किया गया था (आईएसओ, 1996)।
वीडीएम सुविधाएँ
वीडीएम-एसएल और वीडीएम++ सिंटैक्स और शब्दार्थ का वर्णन वीडीएमटूल्स लैंग्वेज मैनुअल और उपलब्ध टेक्स्ट में विस्तार से किया गया है। आईएसओ मानक में लैंग्वेज के शब्दार्थ की फॉर्मल डिफ्निसन सम्मिलित है। इस आलेख के शेष भाग में, आईएसओ-परिभाषित इंटरचेंज (एएससीआईआई) सिंटैक्स का उपयोग किया गया है। कुछ टेक्स्ट अधिक संक्षिप्त गणितीय संकेतन को प्राथमिकता देते हैं।
वीडीएम-एसएल मॉडल डेटा पर निष्पादित कार्यक्षमता के कॉन्टेक्स्ट में दिया गया सिस्टम विवरण है। इसमें डेटा टाइप और उन पर निष्पादित कार्यों या संचालन की डिफ्निसन ओं की श्रृंखला सम्मिलित है।
मूल प्रकार: संख्यात्मक, वर्ण, टोकन और कोटे प्रकार
वीडीएम-एसएल में बेसिक टाइप के मॉडलिंग नंबर और अक्षर इस टाइप सम्मिलित हैं:
bool |
बूलियन डाटा टाइप | false, true |
nat |
नेचुरल नंबर (शून्य सहित) | 0, 1, 2, 3, 4, 5 ... |
nat1 |
नेचुरल नंबर (शून्य छोड़कर) | 1, 2, 3, 4, 5, ... |
int |
इन्टिजर | ..., −3, −2, −1, 0, 1, 2, 3, ... |
rat |
रैशनल नंबर | a/b, जहां a और b पूर्णांक हैं, b 0 नहीं है |
real |
रियल नंबर | ... |
char |
करैक्टर | A, B, C, ... |
token |
स्ट्रक्चरलेस टोकन | ... |
<A> |
कोटे टाइप जिसमें मान <A> है | ... |
डेटा टाइप को मॉडल किए गए सिस्टम के मुख्य डेटा का प्रतिनिधित्व करने के लिए परिभाषित किया गया है। प्रत्येक टाइप की डिफ्निसन नए टाइप के नाम का परिचय देती है और मूल टाइप के कॉन्टेक्स्ट में या पहले से प्रस्तुत किए गए टाइप के कॉन्टेक्स्ट में प्रतिनिधित्व देती है। उदाहरण के लिए, लॉग-इन मैनेजमेंट सिस्टम के लिए टाइप के मॉडलिंग उपयोगकर्ता पहचानकर्ता को निम्नानुसार परिभाषित किया जा सकता है:
types UserId = nat
डेटा टाइप से संबंधित मूल्यों में परिवर्तन करने के लिए, ऑपरेटरों को मूल्यों पर परिभाषित किया जाता है। इस प्रकार, प्राकृतिक संख्या जोड़, घटाव आदि प्रदान किए जाते हैं, जैसे कि समानता और असमानता जैसे बूलियन ऑपरेटर होते हैं। लैंग्वेज अधिकतम या न्यूनतम प्रतिनिधित्व योग्य संख्या या वास्तविक संख्याओं के लिए कोई परिशुद्धता तय नहीं करती है। ऐसी बाधाओं को परिभाषित किया जाता है जहां डेटा टाइप के इनवेरिएंट के माध्यम से प्रत्येक मॉडल में उनकी आवश्यकता होती है - बूलियन अभिव्यक्तियां उन स्थितियों को दर्शाती हैं जिनका परिभाषित टाइप के सभी कॉम्पोनेन्टं द्वारा सम्मान किया जाना चाहिए। उदाहरण के लिए, आवश्यकता कि उपयोगकर्ता पहचानकर्ता 9999 से अधिक नहीं होने चाहिए, निम्नानुसार व्यक्त की जाएगी (जहां <= प्राकृतिक संख्याओं पर बूलियन ऑपरेटर से कम या उसके समान है):
UserId = nat inv uid == uid <= 9999
चूंकि अपरिवर्तनीय इच्छित रूप से काम्प्लेक्स लॉजिक अभिव्यक्ति हो सकते हैं, और परिभाषित टाइप की सदस्यता केवल उन मूल्यों तक सीमित है जो अपरिवर्तनीय को संतुष्ट करते हैं, वीडीएम-एसएल में टाइप की शुद्धता सभी स्थितियों में स्वचालित रूप से निर्णय लेने योग्य नहीं है।
अन्य बेसिक टाइप में वर्णों के लिए वर्ण सम्मिलित हैं। कुछ स्थितियों में, किसी टाइप का प्रतिनिधित्व मॉडल के उद्देश्य के लिए प्रासंगिक नहीं है और इससे केवल काम्प्लेक्स बढ़ेगी। ऐसे स्थितियों में, टाइप के सदस्यों को संरचनाहीन टोकन के रूप में दर्शाया जा सकता है। टोकन टाइप के मूल्यों की तुलना केवल समानता के लिए की जा सकती है - उन पर कोई अन्य ऑपरेटर परिभाषित नहीं हैं। जहां विशिष्ट नामित मानों की आवश्यकता होती है, उन्हें कोटे टाइप के रूप में प्रस्तुत किया जाता है। प्रत्येक कोटे टाइप में टाइप के समान नाम का नामित मान होता है। कोटे टाइप के मान (कोटे शाब्दिक के रूप में जाना जाता है) की तुलना केवल समानता के लिए की जा सकती है।
उदाहरण के लिए, ट्रैफ़िक सिग्नल कंट्रोलर के मॉडलिंग में, ट्रैफ़िक सिग्नल के रंगों को कोटे टाइप के रूप में दर्शाने के लिए मानों को परिभाषित करना सुविधाजनक हो सकता है:
<Red>, <Amber>, <FlashingAmber>, <Green>
कंस्ट्रक्शन टाइप: यूनियन, प्रोडक्ट और कम्पोजिट टाइप
केवल मूल टाइप ही सीमित मूल्य के हैं। नए, अधिक संरचित डेटा टाइप टाइप कंस्ट्रक्टर का उपयोग करके बनाए जाते हैं।
T1 | T2 | ... | Tn |
यूनियन टाइप T1,...,Tn
|
T1*T2*...*Tn |
टाइप के कार्टेशियन प्रोडक्ट T1,...,Tn
|
T :: f1:T1 ... fn:Tn |
समग्र (रिकॉर्ड) प्रकार |
सबसे बेसिक टाइप का कंस्ट्रक्टर दो पूर्वनिर्धारित टाइप का मिलन बनाता है। प्ररूप (A|B) इसमें A टाइप के सभी कॉम्पोनेन्ट और टाइप के सभी कॉम्पोनेन्ट सम्मिलित हैं B. ट्रैफ़िक सिग्नल कंट्रोलर उदाहरण में, ट्रैफ़िक सिग्नल के रंग मॉडलिंग के टाइप को निम्नानुसार परिभाषित किया जा सकता है:
SignalColour = <Red> | <Amber> | <FlashingAmber> | <Green>
वीडीएम-एसएल में प्रगणित टाइप को कोटे टाइप पर यूनियनों के रूप में ऊपर दिखाए गए अनुसार परिभाषित किया गया है।
कार्टेशियन प्रोडक्ट टाइप को वीडीएम-एसएल में भी परिभाषित किया जा सकता है। प्ररूप (A1*…*An) मानों के सभी टुपल्स से बना टाइप है, जिसका पहला कॉम्पोनेन्ट टाइप से है A1 और दूसरा टाइप से A2 और इसी तरह मिश्रित या रिकॉर्ड टाइप कार्टेशियन प्रोडक्ट है जिसमें फ़ील्ड के लिए लेबल होते हैं। प्ररूप
T :: f1:A1 f2:A2 ... fn:An
f1,…,fn लेबल वाले फ़ील्ड वाला कार्टेशियन प्रोडक्ट है। टाइप T का कॉम्पोनेन्ट उसके घटक भागों से कंस्ट्रक्टर द्वारा बनाया जा सकता है, जिसे mk_T लिखा जाता है। इसके विपरीत, टाइप Tका कॉम्पोनेन्ट दिए जाने पर, नामित घटक का चयन करने के लिए फ़ील्ड नामों का उपयोग किया जा सकता है। उदाहरण के लिए, प्रकार
Date :: day:nat1 month:nat1 year:nat inv mk_Date(d,m,y) == d <=31 and m<=12
एक साधारण दिनांक टाइप मॉडल करता है। मान mk_Date(1,4,2001) 1 अप्रैल 2001 से मेल खाता है। दिनांक d दी गई है अभिव्यक्ति d.month महीने का प्रतिनिधित्व करने वाली प्राकृतिक संख्या है। यदि चाहें तो प्रति माह दिनों और लीप वर्ष पर प्रतिबंध को अपरिवर्तनीय में सम्मिलित किया जा सकता है। इनका संयोजन:
mk_Date(1,4,2001).month = 4
कलेक्शन्स
स्टोर टाइप मानो के मॉडल समूह सेट परिमित अव्यवस्थित स्टोर हैं जिनमें मानों के बीच दोहराव को दबा दिया जाता है। अनुक्रम परिमित क्रमित स्टोर (सूचियाँ) हैं जिनमें दोहराव हो सकता है और मैपिंग मानों के दो सेटों के बीच परिमित कॉरेस्पोंडेंस का प्रतिनिधित्व करते हैं।
सेट
सेट टाइप का कंस्ट्रक्टर (T का लिखित set of T पूर्वनिर्धारित टाइप है) टाइप T से खींचे गए मानों के सभी परिमित सेटों से बना टाइप का निर्माण करता है। उदाहरण के लिए टाइप की परिभाषा
UGroup = set of UserIdUserIdमानों के सभी परिमित सेटों से बना टाइप UGroup को परिभाषित करता है। विभिन्न ऑपरेटरों को उनके संघ, प्रतिच्छेदन, उचित और गैर-सख्त सबसेट संबंधों का निर्धारण आदि के लिए सेट पर परिभाषित किया गया है।
{a, b, c} |
गणना सेट करें: एलिमेंट का सेट a, b और c
|
{x | x:T & P(x)} |
सेट कॉम्प्रिहेंशन: का सेट x का प्रकार T ऐसा है कि P(x)
|
{i, ..., j} |
i से j की सीमा में पूर्णांकों का समुच्चय
|
e in set s |
e सेट s का एलिमेंट है
|
e not in set s |
e सेट s का एलिमेंट नहीं है
|
s1 union s2 |
सेट s1 और s2 का यूनियन
|
s1 inter s2 |
सेट s1 और s2 का प्रतिच्छेदन
|
s1 \ s2 |
सेट s1 और s2 का अंतर निर्धारित करें |
dunion s |
सेट के सेट का डिस्ट्रीब्यूटेड यूनियन s |
s1 psubset s2 |
s1, s2 का एक (प्रोपर) सबसेट है
|
s1 subset s2 |
s1 , s2 का एक (अशक्त) सबसेट है
|
card s |
सेट s की कार्डिनैलिटी
|
अनुक्रम
परिमित अनुक्रम टाइप कंस्ट्रक्टर (लिखित) seq of T जहाँ T पूर्वनिर्धारित टाइप है) टाइप से निकाले गए मानों की सभी सीमित सूचियों से बना टाइप T बनाता है . उदाहरण के लिए, टाइप की डिफ्निसन
String = seq of char
एक टाइप को परिभाषित करता है String वर्णों की सभी सीमित श्रृंखलाओं से बना है। विभिन्न ऑपरेटरों को संयोजन के निर्माण, कॉम्पोनेन्टं और उसके पश्चात् के अनुक्रम आदि के चयन के लिए अनुक्रमों पर परिभाषित किया गया है। इनमें से कई ऑपरेटर इस अर्थ में आंशिक हैं कि उन्हें कुछ अनुप्रयोगों के लिए परिभाषित नहीं किया गया है। उदाहरण के लिए, किसी अनुक्रम के 5वें कॉम्पोनेन्ट का चयन करना जिसमें केवल तीन कॉम्पोनेन्ट हैं, अपरिभाषित है।
इसलिए, क्रम में वस्तुओं का क्रम और पुनरावृत्ति महत्वपूर्ण है [a, b] के समान नहीं है [b, a], और [a] के समान नहीं है [a, a].
[a, b, c] |
अनुक्रम गणना: कॉम्पोनेन्टं a, b and c का अनुक्रम
|
[f(x) | x:T & P(x)] |
अनुक्रम बोध: (संख्यात्मक) प्रकार T के प्रत्येक x के लिए अभिव्यक्ति f(x) का अनुक्रम इस प्रकार है कि P(x) बना रहे
(x मान संख्यात्मक क्रम में लिया गया है) |
hd s |
sका प्रमुख (प्रथम अवयव)
|
tl s |
sकी पूँछ (सिर हटाने के पश्चात् शेष क्रम)।
|
len s |
sकी लंबाई
|
elems s |
sके कॉम्पोनेन्टं का सेट
|
s(i) |
s का ith अवयव
|
inds s |
अनुक्रम के लिए सूचकांकों का सेट s
|
s1^s2 |
अनुक्रम s1 और s2 को जोड़ने से बना अनुक्रम |
मानचित्र
एक परिमित मानचित्रण दो सेटों, डोमेन और रेंज के बीच, रेंज के डोमेन अनुक्रमण कॉम्पोनेन्टं के साथ कॉरेस्पोंडेंस है। इसलिए यह परिमित कार्य के समान है। वीडीएम-एसएल में मैपिंग टाइप का कंस्ट्रक्टर (लिखित) map T1 to T2 जहाँ T1 और T2 पूर्वनिर्धारित टाइप हैं) सेट से सभी परिमित मैपिंग से बने टाइप का निर्माण करता है जिसमेT1 के सेट के लिए मान T2 मूल्य. उदाहरण के लिए, टाइप की डिफ्निसन
Birthdays = map String to Date
एक टाइप को परिभाषित करता है Birthdays जो कैरेक्टर स्ट्रिंग्स को मैप करता है Date. फिर से, मैपिंग में अनुक्रमण, मैपिंग को मर्ज करने, उप-मैपिंग को निकालने के लिए ओवरराइटिंग के लिए ऑपरेटरों को मैपिंग पर परिभाषित किया जाता है।
{a |-> r, b |-> s} |
मैपिंग गणना: a मैप्स टू r, b मैप्स टू s
|
{x |-> f(x) | x:T & P(x)} |
मैपिंग कॉम्प्रिहेंशन: x प्रकार T के लिए सभी x के लिए f(x) पर मैप करता है, जैसे किP(x):
|
dom m |
m का डोमेन
|
rng m |
m की रेंज
|
m(x) |
m x पर प्रयुक्त होता है
|
m1 munion m2 |
मैपिंग m1 और m2 (m1, m2 जहां वह ओवरलैप होते हैं वहां सुसंगत होना चाहिए)
|
m1 ++ m2 |
m1 को m2 द्वारा अधिलेखित किया गया
|
संरचना
वीडीएम-एसएल और वीडीएम++ नोटेशन के बीच मुख्य अंतर संरचना से सामना करने के मेथड में है। वीडीएम-एसएल में पारंपरिक मॉड्यूलर एक्सटेंशन है जबकि वीडीएम++ में क्लास और इनहेरिटेंस के साथ पारंपरिक ऑब्जेक्ट-ओरिएंटेड संरचना तंत्र है।
वीडीएम-एसएल में संरचना
वीडीएम-एसएल के लिए आईएसओ मानक में सूचनात्मक अनुबंध है जिसमें विभिन्न संरचना सिद्धांत सम्मिलित हैं। ये सभी मॉड्यूल के साथ पारंपरिक जानकारी छिपाने के सिद्धांतों का पालन करते हैं और इन्हें इस टाइप कॉम्प्रिहेंशनाया जा सकता है:
- मॉड्यूल नामकरण: प्रत्येक मॉड्यूल वाक्यात्मक रूप से कीवर्ड से प्रारंभ होता है
moduleइसके पश्चात् मॉड्यूल का नाम आता है। मॉड्यूल के अंत में कीवर्डendमॉड्यूल के नाम के पश्चात् फिर से लिखा गया है। - आयात करना: अन्य मॉड्यूल से निर्यात की गई डिफ्निसन ओं को आयात करना संभव है। यह आयात अनुभाग में किया जाता है जिसकी प्रारंभिक कीवर्ड से होती है
importsऔर उसके पश्चात् विभिन्न मॉड्यूल से आयात का क्रम चलता है। इनमें से प्रत्येक मॉड्यूल आयात कीवर्ड से प्रारंभ होता हैfromउसके पश्चात् मॉड्यूल का नाम और मॉड्यूल हस्ताक्षर आता है। मॉड्यूल हस्ताक्षर या तो केवल कीवर्ड हो सकता हैallउस मॉड्यूल से निर्यात की गई सभी डिफ्निसन ओं के आयात को निरुपित करना, या यह आयात हस्ताक्षरों का क्रम हो सकता है। आयात हस्ताक्षर प्रकार, मान, फ़ंक्शन और संचालन के लिए विशिष्ट होते हैं और इनमें से प्रत्येक संबंधित कीवर्ड से प्रारंभ होते हैं। इसके अतिरिक्त ये आयात हस्ताक्षर उन निर्माणों का नाम देते हैं जिन तक पहुंच प्राप्त करने की इच्छा है। इसके अतिरिक्त वैकल्पिक टाइप की जानकारी उपस्थित हो सकती है और अंततः आयात पर प्रत्येक निर्माण का नाम परिवर्तित करना संभव है। टाइप के लिए कीवर्ड का भी उपयोग करना होगाstructयदि कोई किसी विशेष टाइप की आंतरिक संरचना तक पहुंच प्राप्त करना चाहता है। - 'निर्यात': मॉड्यूल की डिफ्निसन, जिन तक कोई अन्य मॉड्यूल की पहुंच चाहता है, कीवर्ड का उपयोग करके निर्यात की जाती हैं
exportsइसके पश्चात् निर्यात मॉड्यूल हस्ताक्षर होगा। निर्यात मॉड्यूल हस्ताक्षर में या तो केवल कीवर्ड सम्मिलित हो सकता हैallया निर्यात हस्ताक्षरों के अनुक्रम के रूप में। ऐसे निर्यात हस्ताक्षर प्रकार, मान, फ़ंक्शन और संचालन के लिए विशिष्ट होते हैं और इनमें से प्रत्येक संबंधित कीवर्ड से प्रारंभ होते हैं। यदि कोई किसी टाइप की कीवर्ड की आंतरिक संरचना को निर्यात करना चाहता हैstructउपयोग किया जाना चाहिए। - अधिक विदेशी विशेषताएं: वीडीएम-एसएल टूल के पुराने संस्करणों में पैरामीटरयुक्त मॉड्यूल और ऐसे मॉड्यूल के इंस्टेंटेशन के लिए भी समर्थन था। चूँकि , इन सुविधाओं को 2000 के आसपास वीडीएमटूल्स से हटा दिया गया था क्योंकि इनका उपयोग संभवतः ही कभी औद्योगिक अनुप्रयोगों में किया गया था और इन सुविधाओं के साथ बड़ी संख्या में टूल चुनौतियाँ थीं।
वीडीएम++ में संरचना
वीडीएम++ में क्लास और एकाधिक इनहेरिटेंस का उपयोग करके संरचना की जाती है। प्रमुख अवधारणाएँ हैं:
- क्लास: प्रत्येक क्लास वाक्यात्मक रूप से कीवर्ड से प्रारंभ होती है
classइसके पश्चात् वर्ग का नाम आता है। कक्षा के अंत में कीवर्डendइसके पश्चात् फिर से कक्षा का नाम लिखा जाता है। - इनहेरिटेंस: यदि किसी वर्ग को अन्य वर्गों से संरचनाएं इनहेरिटेंस में मिलती हैं तो वर्ग शीर्षक में वर्ग नाम के पश्चात् कीवर्ड का उपयोग किया जा सकता है
is subclass ofउसके पश्चात् सुपरक्लास के नामों की अल्पविराम से अलग की गई सूची। - एक्सेस संशोधक: वीडीएम++ में जानकारी हिडेन करना उसी तरह से किया जाता है जैसे अधिकांश ऑब्जेक्ट ओरिएंटेड लैंग्वेज ओं में एक्सेस संशोधक का उपयोग करके किया जाता है। वीडीएम++ में डिफ्निसन एँ डिफ़ॉल्ट रूप से निजी होती हैं किंतु सभी डिफ्निसन ओं के सामने एक्सेस संशोधक कीवर्ड
private,publicऔरprotectedमें से किसी का उपयोग करना संभव है:.
मॉडलिंग कार्यक्षमता
कार्यात्मक मॉडलिंग
वीडीएम-एसएल में, फ़ंक्शन को मॉडल में परिभाषित डेटा टाइप पर परिभाषित किया जाता है। एब्सट्रक्टन के लिए समर्थन के लिए आवश्यक है कि किसी फ़ंक्शन की गणना किए जाने वाले परिणाम को चिह्नित करना संभव हो, बिना यह बताए कि इसकी गणना कैसे की जानी चाहिए। ऐसा करने का मुख्य तंत्र अंतर्निहित फ़ंक्शन डिफ्निसन है, जिसमें किसी परिणाम की गणना करने वाले सूत्र के अतिरिक्त, इनपुट और परिणाम वेरिएबल पर लॉजिक विधेय, जिसे पोस्टकंडिशन कहा जाता है, परिणाम के गुण देता है। उदाहरण के लिए, फ़ंक्शन SQRT किसी प्राकृत संख्या के वर्गमूल की गणना के लिए इसे इस टाइप परिभाषित किया जा सकता है:
SQRT(x:nat)r:real post r*r = x
यहां पोस्टकंडिशन परिणाम की गणना के लिए मेथड r परिभाषित नहीं करता है किंतु यह बताता है कि इसके पास कौन से गुण माने जा सकते हैं। ध्यान दें कि यह फ़ंक्शन को परिभाषित करता है जो वैध वर्गमूल लौटाता है; इसकी कोई आवश्यकता नहीं है कि यह धनात्मक या ऋणात्मक मूल होना चाहिए। उपरोक्त स्पेसिफिकेशन संतुष्ट होंगे, उदाहरण के लिए फ़ंक्शन द्वारा जो 4 का ऋणात्मक मूल किंतु अन्य सभी वैध इनपुट का धनात्मक मूल लौटाता है। ध्यान दें कि वीडीएम-एसएल में फ़ंक्शंस को नियतात्मक होना आवश्यक है जिससे ऊपर दिए गए उदाहरण स्पेसिफिकेशन को संतुष्ट करने वाला फ़ंक्शन सदैव समान इनपुट के लिए समान परिणाम लौटाए गए।
पोस्टकंडीशन को प्रबल करके अधिक बाधित फ़ंक्शन स्पेसिफिकेशन प्राप्त किया जाता है। उदाहरण के लिए, निम्नलिखित डिफ्निसन फ़ंक्शन को धनात्मक रूट वापस करने के लिए बाध्य करती है।
SQRT(x:nat)r:real post r*r = x and r>=0
सभी फ़ंक्शन स्पेसिफिकेशन को उन पूर्व नियमो द्वारा प्रतिबंधित किया जा सकता है जो केवल इनपुट वेरिएबल पर लॉजिक विधेय हैं और जो उन बाधाओं का वर्णन करते हैं जिन्हें फ़ंक्शन निष्पादित होने पर संतुष्ट माना जाता है। उदाहरण के लिए, वर्गमूल गणना फ़ंक्शन जो केवल धनात्मक वास्तविक संख्याओं पर कार्य करता है, उसे निम्नानुसार निर्दिष्ट किया जा सकता है:
SQRTP(x:real)r:real pre x >=0 post r*r = x and r>=0
पूर्व नियम और उत्तर नियम मिलकर अनुबंध बनाते हैं जिसे फ़ंक्शन को प्रयुक्त करने का दावा करने वाले किसी भी प्रोग्राम द्वारा संतुष्ट किया जाना चाहिए। पूर्व नियम उन धारणाओं को रिकॉर्ड करती है जिसके अनुसार फ़ंक्शन पोस्ट नियम को संतुष्ट करने वाले परिणाम को वापस करने की गारंटी देता है। यदि किसी फ़ंक्शन को ऐसे इनपुट पर कॉल किया जाता है जो उसकी पूर्व नियम को पूरा नहीं करता है, तो परिणाम अपरिभाषित है (वास्तव में, समाप्ति की गारंटी भी नहीं है)।
वीडीएम-एसएल कार्यात्मक प्रोग्रामिंग लैंग्वेज के मेथड से निष्पादन योग्य कार्यों की डिफ्निसन का भी समर्थन करता है। स्पष्ट फ़ंक्शन डिफ्निसन में, परिणाम को इनपुट पर अभिव्यक्ति के माध्यम से परिभाषित किया जाता है। उदाहरण के लिए, फ़ंक्शन जो संख्याओं की सूची के वर्गों की सूची तैयार करता है, उसे निम्नानुसार परिभाषित किया जा सकता है:
SqList: seq of nat -> seq of nat SqList(s) == if s = [] then [] else [(hd s)**2] ^ SqList(tl s)
इस पुनरावर्ती डिफ्निसन में फ़ंक्शन हस्ताक्षर होता है जो इनपुट और परिणाम के टाइप और फ़ंक्शन बॉडी देता है। समान फ़ंक्शन की अंतर्निहित डिफ्निसन निम्नलिखित रूप ले सकती है:
SqListImp(s:seq of nat)r:seq of nat post len r = len s and forall i in set inds s & r(i) = s(i)**2
स्पष्ट डिफ्निसन सरल अर्थ में अंतर्निहित रूप से निर्दिष्ट फ़ंक्शन का कार्यान्वयन है। अंतर्निहित स्पेसिफिकेशन के संबंध में स्पष्ट फ़ंक्शन डिफ्निसन की शुद्धता को निम्नानुसार परिभाषित किया जा सकता है।
एक अंतर्निहित स्पेसिफिकेशन दी गई:
f(p:T_p)r:T_r pre pre-f(p) post post-f(p, r)
और स्पष्ट कार्य:
f:T_p -> T_r
हम कहते हैं कि यह स्पेसिफिकेशन को पूरा करता है यदि:
forall p in set T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))
इसलिए,f सही कार्यान्वयन है के रूप में व्याख्या की जानी चाहिएf स्पेसिफिकेशन को पूरा करता है.
स्टेट-बेस्ड मॉडलिंग
वीडीएम-एसएल में, फ़ंक्शंस के दुष्प्रभाव नहीं होते हैं जैसे कि निरंतर ग्लोबल वेरिएबल की स्थिति को परिवर्तित करना। यह कई प्रोग्रामिंग लैंग्वेज ओं में उपयोगी क्षमता है, इसलिए समान अवधारणा उपस्थित है; फ़ंक्शंस के अतिरिक्त , ऑपरेशन का उपयोग 'स्टेट वेरिएबल्स' (जिसे ग्लोबल्स के रूप में भी जाना जाता है) को बदलने के लिए किया जाता है।
उदाहरण के लिए, यदि हमारे पास एकल वेरिएबल से युक्त स्टेट है someStateRegister : nat, हम इसे वीडीएम-एसएल में इस टाइप परिभाषित कर सकते हैं:
state Register of someStateRegister : nat end
इसके अतिरिक्त वीडीएम++ में इसे इस टाइप परिभाषित किया जाएगा:
instance variables someStateRegister : nat
इस वेरिएबल में मान लोड करने के लिए ऑपरेशन को इस टाइप निर्दिष्ट किया जा सकता है:
LOAD(i:nat) ext wr someStateRegister:nat post someStateRegister = i
बाहरी खंड (ext) निर्दिष्ट करता है कि ऑपरेशन द्वारा स्टेट के किन भागो तक पहुँचा जा सकता है; rd केवल-पठन पहुंच का संकेत और wr पढ़ने/लिखने की पहुंच।
कभी-कभी किसी स्टेट को संशोधित करने से पहले उसके मूल्य का उल्लेख करना महत्वपूर्ण होता है; उदाहरण के लिए, वैरिएबल में मान जोड़ने के लिए ऑपरेशन को इस टाइप निर्दिष्ट किया जा सकता है:
ADD(i:nat) ext wr someStateRegister : nat post someStateRegister = someStateRegister~ + i
जहां ~ पोस्टकंडिशन में स्टेट वेरिएबल पर प्रतीक ऑपरेशन के निष्पादन से पहले स्टेट वेरिएबल का मान निरुपित करता है।
उदाहरण
अधिकतम फ़ंक्शन
यह अंतर्निहित फ़ंक्शन डिफ्निसन का उदाहरण है। फ़ंक्शन धनात्मक पूर्णांकों के सेट से सबसे बड़ा कॉम्पोनेन्ट लौटाता है:
max(s:set of nat)r:nat pre card s > 0 post r in set s and forall r' in set s & r' <= r
पोस्टकंडिशन परिणाम को प्राप्त करने के लिए एल्गोरिदम को परिभाषित करने के अतिरिक्त उसे चित्रित करता है। पूर्व नियम की आवश्यकता है क्योंकि सेट रिक्त होने पर कोई भी फ़ंक्शन सेट s में r वापस नहीं कर सकता है।
प्राकृतिक संख्या गुणन
multp(i,j:nat)r:nat pre true post r = i*j
प्रमाण दायित्व प्रयुक्त करना forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p)) की स्पष्ट डिफ्निसन के लिए multp:
multp(i,j) == if i=0 then 0 else if is-even(i) then 2*multp(i/2,j) else j+multp(i-1,j)
तब प्रमाण दायित्व बन जाता है:
forall i, j : nat & multp(i,j):nat and multp(i, j) = i*j
इसे इसके द्वारा सही दिखाया जा सकता है:
- यह सिद्ध करना कि पुनरावृत्ति समाप्त हो जाती है (इसके बदले में यह सिद्ध करना आवश्यक है कि संख्याएँ प्रत्येक फेज में छोटी हो जाती हैं)
- गणितीय प्रेरण
पंक्ति सार डेटा टाइप
यह प्रसिद्ध डेटा संरचना के स्टेट -बेस्ड मॉडल में अंतर्निहित ऑपरेशन स्पेसिफिकेशन के उपयोग को दर्शाने वाला मौलिक उदाहरण है। पंक्ति को टाइप के कॉम्पोनेन्टं से बने अनुक्रम के रूप में तैयार किया गया है Qelt. प्रतिनिधित्व है Qelt सारहीन है और इसलिए इसे टोकन टाइप के रूप में परिभाषित किया गया है।
types
Qelt = token; Queue = seq of Qelt;
state TheQueue of q : Queue end
operations
ENQUEUE(e:Qelt) ext wr q:Queue post q = q~ ^ [e];
DEQUEUE()e:Qelt ext wr q:Queue pre q <> [] post q~ = [e]^q;
IS-EMPTY()r:bool ext rd q:Queue post r <=> (len q = 0)
बैंक सिस्टम उदाहरण
वीडीएम-एसएल मॉडल के बहुत ही सरल उदाहरण के रूप में, ग्राहक बैंक खाते का विवरण बनाए रखने के लिए सिस्टम पर विचार करें। ग्राहकों को ग्राहक संख्या (CustNum) द्वारा मॉडल किया जाता है, खातों को खाता संख्या (AccNum) द्वारा मॉडल किया जाता है। ग्राहक संख्या का प्रतिनिधित्व सारहीन माना जाता है और इसलिए इसे टोकन टाइप के आधार पर तैयार किया जाता है। शेष राशि और ओवरड्राफ्ट को संख्यात्मक टाइप के आधार पर तैयार किया जाता है।
AccNum = token; CustNum = token; Balance = int; Overdraft = nat;
AccData :: owner : CustNum balance : Balance
state Bank of accountMap : map AccNum to AccData overdraftMap : map CustNum to Overdraft inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and a.balance >= -overdraftMap(a.owner)
संचालन के साथ:
एनईडब्ल्यूसी नया ग्राहक नंबर आवंटित करता है:
operations
NEWC(od : Overdraft)r : CustNum
ext wr overdraftMap : map CustNum to Overdraft
post r not in set dom ~overdraftMap and overdraftMap = ~overdraftMap ++ { r |-> od};
एनईडब्ल्यूएसी नया खाता नंबर आवंटित करता है और शेष राशि को शून्य पर सेट करता है:
NEWAC(cu : CustNum)r : AccNum
ext wr accountMap : map AccNum to AccData
rd overdraftMap map CustNum to Overdraft
pre cu in set dom overdraftMap
post r not in set dom accountMap~ and accountMap = accountMap~ ++ {r|-> mk_AccData(cu,0)}
एसीआईएनएफ ग्राहक के सभी खातों की सभी शेष राशि, शेष राशि के खाता संख्या के मानचित्र के रूप में लौटाता है:
ACINF(cu : CustNum)r : map AccNum to Balance
ext rd accountMap : map AccNum to AccData
post r = {an |-> accountMap(an).balance | an in set dom accountMap & accountMap(an).owner = cu}
उपकरण समर्थन
कई अलग-अलग उपकरण वीडीएम का समर्थन करते हैं:
- वीडीएमटूल्स वीडीएम और वीडीएम++ के लिए अग्रणी व्यावसायिक उपकरण था, जिसका स्वामित्व, विपणन, रखरखाव और डेवलपमेंट CSK Systems द्वारा किया गया था, जो डेनिश कंपनी आईएफएडी द्वारा विकसित पुराने संस्करणों पर बेस्ड था। मैनुअल और व्यावहारिक ट्यूटोरियल उपलब्ध हैं। टूल के पूर्ण संस्करण के लिए सभी लाइसेंस निःशुल्क उपलब्ध हैं। पूर्ण संस्करण में जावा और सी++ के लिए स्वचालित कोड जनरेशन, डायनेमिक लिंक लाइब्रेरी और कोरबा समर्थन सम्मिलित है।
- ओवरवेरिएबल समुदाय-बेस्ड ओपन सोर्स पहल है जिसका उद्देश्य सभी वीडीएम बोलियों (वीडीएम-एसएल, वीडीएम++ और वीडीएम-आरटी) के लिए मूल रूप से एक्लिप्स प्लेटफॉर्म के शीर्ष पर किंतु पश्चात् में विजुअल स्टूडियो कोड प्लेटफॉर्म के शीर्ष पर स्वतंत्र रूप से उपलब्ध टूल समर्थन प्रदान करना है। इसका उद्देश्य इंटरऑपरेबल टूल के लिए प्रारूप विकसित करना है जो औद्योगिक अनुप्रयोग, अनुसंधान और शिक्षा के लिए उपयोगी होगा।
- वीडीएम-mode वीडीएम-एसएल, वीडीएम++ और वीडीएम-आरटी का उपयोग करके वीडीएम स्पेसिफिकेशन लिखने के लिए इमैक्स पैकेजों का स्टोर है। यह सिंटैक्स हाइलाइटिंग और संपादन, ऑन-द-फ्लाई सिंटैक्स चेकिंग, टेम्पलेट पूर्णता और इन्टेरोपेराबल समर्थन का समर्थन करता है।
- SpecBox: एडेलार्ड से सिंटैक्स जांच, कुछ सरल सिमेंटिक जांच और LaTeX फ़ाइल का निर्माण प्रदान किया जाता है, जो स्पेसिफिकेशन को गणितीय नोटेशन में मुद्रित करने में सक्षम बनाता है। यह उपकरण निःशुल्क उपलब्ध है किंतु इसका रखरखाव नहीं किया जा रहा है।
- आईएसओ मानक लैंग्वेज के गणितीय वाक्यविन्यास में वीडीएम मॉडल की प्रस्तुति का समर्थन करने के लिए LaTeX और LaTeX2e मैक्रोज़ उपलब्ध हैं। इन्हें यूके में राष्ट्रीय भौतिक प्रयोगशाला द्वारा विकसित और रखरखाव किया गया है। डॉक्यूमेंटीकरण और मैक्रोज़ ऑनलाइन उपलब्ध हैं।
औद्योगिक अनुभव
वीडीएम को विभिन्न एप्लिकेशन डोमेन में व्यापक रूप से प्रयुक्त किया गया है। इनमें से सबसे प्रसिद्ध अनुप्रयोग हैं:
- Ada (प्रोग्रामिंग लैंग्वेज ) और सीएचआईएलएल कम्पाइलर: पहला यूरोपीय मान्य Ada कंपाइलर वीडीएम का उपयोग करके Dansk डेटामैटिक सेंटर द्वारा विकसित किया गया था।[8] इसी टाइप सीएचआईएलएल और मॉड्यूला-2 के शब्दार्थ को वीडीएम का उपयोग करके उनके मानकों में वर्णित किया गया था।
- कॉनफॉर्म: ब्रिटिश एयरोस्पेस में प्रयोग जिसमें विश्वसनीय गेटवे के पारंपरिक डेवलपमेंट की तुलना वीडीएम का उपयोग करके किए गए डेवलपमेंट से की गई है।
- धूल-विशेषज्ञ: सुरक्षा संबंधी अनुप्रयोग के लिए यूके में एडेलार्ड द्वारा चलाया गया प्रोजेक्ट जो यह निर्धारित करता है कि औद्योगिक संयंत्रों के लेआउट में सुरक्षा उपयुक्त है।
- वीडीएमटूल्स का विकास: वीडीएमटूल्स टूल सूट के अधिकांश घटक स्वयं वीडीएम का उपयोग करके विकसित किए गए हैं। यह डेवलपमेंट डेनमार्क में आईएफएडी और जापान में सीएसके होल्डिंग्स कॉर्पोरेशन में किया गया है।[9]
- ट्रेडवन: जापानी स्टॉक एक्सचेंज के लिए सीएसके सिस्टम द्वारा विकसित ट्रेडवन बैक-ऑफिस सिस्टम के कुछ प्रमुख घटक वीडीएम का उपयोग करके विकसित किए गए थे। पारंपरिक रूप से विकसित कोड बनाम वीडीएम-विकसित घटकों की डेवलपर उत्पादकता और दोष घनत्व के लिए तुलनात्मक माप उपस्थित हैं।
- फेलिका नेटवर्क्स ने सेलुलर टेलीफोन अनुप्रयोगों के लिए एकीकृत सर्किट के लिए ऑपरेटिंग सिस्टम के डेवलपमेंट की सूचना दी है।
रेफिनमेन्ट
वीडीएम का उपयोग बहुत ही एब्सट्रेक्ट (कंप्यूटर विज्ञान) मॉडल से प्रारंभ होता है और इसे कार्यान्वयन में विकसित करता है। प्रत्येक फेज में डेटा रेफिकेशन , फिर ऑपरेशन अपघटन सम्मिलित है।
डेटा रीफिकेशन एब्सट्रेक्ट डेटा टाइप को अधिक ठोस डेटा संरचनाओं में विकसित करता है, जबकि ऑपरेशन अपघटन संचालन और कार्यों के (एब्सट्रक्ट) अंतर्निहित विनिर्देशों को एल्गोरिथ्म मेथड में विकसित करता है जिन्हें सीधे पसंद की कंप्यूटर लैंग्वेज में प्रयुक्त किया जा सकता है।
डेटा रीफिकेशन
डेटा पुनरीक्षण (चरणबद्ध शोधन) में स्पेसिफिकेशन में उपयोग किए गए एब्सट्रेक्ट डेटा टाइप का अधिक ठोस प्रतिनिधित्व खोजना सम्मिलित है। कार्यान्वयन तक पहुँचने से पहले कई फेज हो सकते हैं। एब्सट्रेक्ट डेटा प्रतिनिधित्व के लिए प्रत्येक पुनरीक्षण फेज ABS_REP इसमें नया प्रतिनिधित्व प्रस्तावित करना सम्मिलित है NEW_REP. यह दिखाने के लिए कि नया प्रतिनिधित्व स्पष्ट है, पुनर्प्राप्ति फ़ंक्शन परिभाषित किया गया है जो संबंधित है NEW_REP को ABS_REP, अर्थात। retr : NEW_REP -> ABS_REP. डेटा रेफिकेशन की शुद्धता पर्याप्तता सिद्ध करने पर निर्भर करती है, अथार्त ।
forall a:ABS_REP & exists r:NEW_REP & a = retr(r)
चूँकि डेटा प्रतिनिधित्व बदल गया है, संचालन और कार्यों को अद्यतन करना आवश्यक है जिससे वे कार्य करते रहें जिससे NEW_REP. नए प्रतिनिधित्व पर किसी भी डेटा टाइप के इनवेरिएंट (कंप्यूटर विज्ञान) को संरक्षित करने के लिए नए संचालन और कार्यों को दिखाया जाना चाहिए। यह सिद्ध करने के लिए कि नए संचालन और फ़ंक्शन मॉडल मूल स्पेसिफिकेशन में पाए गए हैं, दो प्रमाण दायित्वों का निर्वहन करना आवश्यक है:
- डोमेन नियम:
forall r: NEW_REP & pre-OPA(retr(r)) => pre-OPR(r)
- मॉडलिंग नियम:
forall ~r,r:NEW_REP & pre-OPA(retr(~r)) and post-OPR(~r,r) => post-OPA(retr(~r,), retr(r))
उदाहरण डेटा रेफिकेशन
व्यवसाय सुरक्षा सिस्टम में, श्रमिकों को आईडी कार्ड दिए जाते हैं; इन्हें फ़ैक्टरी में प्रवेश करने और बाहर निकलने पर कार्ड रीडर में फीड किया जाता है। संचालन आवश्यक:'
INIT()सिस्टम को इनिशियलाइज़ करता है, मानता है कि फ़ैक्टरी रिक्त हैENTER(p : Person)रिकॉर्ड करता है कि एम्प्लोयी फ़ैक्टरी में प्रवेश कर रहा है; श्रमिकों का विवरण आईडी कार्ड से पढ़ा जाता है)EXIT(p : Person)रिकॉर्ड करता है कि एम्प्लोयी फ़ैक्टरी से बाहर निकल रहा हैIS-PRESENT(p : Person) r : boolयह देखने के लिए जाँच करता है कि कोई निर्दिष्ट एम्प्लोयी फ़ैक्टरी में है या नहीं
फॉर्मल रूप से, यह होगा:
types
Person = token; Workers = set of Person;
state AWCCS of pres: Workers end
operations
INIT()
ext wr pres: Workers
post pres = {};
ENTER(p : Person)
ext wr pres : Workers
pre p not in set pres
post pres = pres~ union {p};
EXIT(p : Person)
ext wr pres : Workers
pre p in set pres
post pres = pres~\{p};
IS-PRESENT(p : Person) r : bool ext rd pres : Workers post r <=> p in set pres~
चूँकि अधिकांश प्रोग्रामिंग लैंग्वेज ओं में सेट ( अधिकांशतः सरणी के रूप में) की तुलना में अवधारणा होती है, स्पेसिफिकेशन से पहला कदम अनुक्रम के कॉन्टेक्स्ट में डेटा का प्रतिनिधित्व करना है। इन अनुक्रमों को पुनरावृत्ति की अनुमति नहीं देनी चाहिए, क्योंकि हम नहीं चाहते कि ही कार्यकर्ता दो बार दिखाई दे, इसलिए हमें नए डेटा टाइप में इनवेरिएंट (कंप्यूटर विज्ञान) जोड़ना होगा। इस स्थिति में, ऑर्डर देना महत्वपूर्ण नहीं है, इसलिए [a,b] वैसा ही है जैसा कि [b,a].के समान है।
वियना डेवलपमेंट पद्धति मॉडल-बेस्ड सिस्टम्स के लिए मूल्यवान है। यदि व्यवस्था समय बेस्ड है तो यह उचित नहीं है। ऐसे स्थितियों के लिए, कम्युनिकेटिंग सिस्टम्स की गणना (सीसीएस) अधिक उपयोगी है।
यह भी देखें
- फॉर्मल मेथड्स
- फॉर्मल स्पेसिफिकेशन
- पिजिन कोड
- विधेय लॉजिक
- प्रस्तावात्मक एल्गोरिथ्म
- जेड स्पेसिफिकेशन लैंग्वेज , वीडीएम-एसएल का मुख्य विकल्प (तुलना करें)
- कम्पास मॉडलिंग लैंग्वेज Archived 19 February 2020 at the Wayback Machine (सीएमएल), प्रोग्रामिंग के एकीकृत सिद्धांत पर बेस्ड संचार अनुक्रमिक प्रक्रियाओं के साथ वीडीएम-एसएल का संयोजन, सिस्टम ऑफ मॉडलिंग (एसओएस) के लिए विकसित किया गया है।
अग्रिम पठन
- Bjørner, Dines; Cliff B. Jones (1978). The Vienna Development Method: The Meta-Language, Lecture Notes in Computer Science 61. Berlin, Heidelberg, New York: Springer. ISBN 978-0-387-08766-5.
- O'Regan, Gerard (2006). Mathematical Approaches to Software Quality. London: Springer. ISBN 978-1-84628-242-3.
- Cliff B. Jones, ed. (1984). Programming Languages and Their Definition — H. Bekič (1936-1982). Lecture Notes in Computer Science. Vol. 177. Berlin, Heidelberg, New York, Tokyo: Springer-Verlag. doi:10.1007/BFb0048933. ISBN 978-3-540-13378-0. S2CID 7488558.
- Fitzgerald, J.S. and Larsen, P.G., Modelling Systems: Practical Tools and Techniques in Software Engineering. Cambridge University Press, 1998 ISBN 0-521-62348-0 (Japanese Edition pub. Iwanami Shoten 2003 ISBN 4-00-005609-3).[10]
- Fitzgerald, J.S., Larsen, P.G., Mukherjee, P., Plat, N. and Verhoef,M., Validated Designs for Object-oriented Systems. Springer Verlag 2005. ISBN 1-85233-881-4. Supporting web site [1] includes examples and free tool support.[11]
- Jones, C.B., Systematic Software Development using वीडीएम, Prentice Hall 1990. ISBN 0-13-880733-7. Also available on-line and free of charge: http://www.csr.ncl.ac.uk/वीडीएम/ssdवीडीएम.pdf.zip
- Bjørner, D. and Jones, C.B., Formal Specification and Software Development Prentice Hall International, 1982. ISBN 0-13-880733-7
- J. Dawes, The वीडीएम-एसएल Reference Guide, Pitman 1991. ISBN 0-273-03151-1
- International Organization for Standardization, Information technology – Programming languages, their environments and system software interfaces – Vienna Development Method – Specification Language – Part 1: Base language International Standard आईएसओ/IEC 13817-1, December 1996.
- Jones, C.B., Software Development: A Rigorous Approach, Prentice Hall International, 1980. ISBN 0-13-821884-6
- Jones, C.B. and Shaw, R.C. (eds.), Case Studies in Systematic Software Development, Prentice Hall International, 1990. ISBN 0-13-880733-7
- Bicarregui, J.C., Fitzgerald, J.S., Lindsay, P.A., Moore, R. and Ritchie, B., Proof in वीडीएम: a Practitioner's Guide. Springer Verlag Formal Approaches to Computing and Information Technology (FACIT), 1994. ISBN 3-540-19813-X .
कॉन्टेक्स्ट
- ↑ Some idea of that work, including a technical report TR 25.139 on "A Formal Definition of a PL/1 Subset", dated 20 December 1974, is reprinted in Jones 1984, p.107-155. Of particular note is the list of authors in order: H. Bekič, D. Bjørner, W. Henhapl, C. B. Jones, P. Lucas.
- ↑ The double plus is adopted from the C++ objected oriented programming language based on C.
- ↑ Bjørner&Jones 1978, Introduction, p.ix
- ↑ Introductory remarks by Cliff B. Jones (editor) in Bekič 1984, p.vii
- ↑ Bjørner&Jones 1978, Introduction, p.xi
- ↑ Bjørner&Jones 1978, p.24.
- ↑ See the article on persistence for its use within computer science.
- ↑ Clemmensen, Geert B. (January 1986). "Retargeting and rehosting the DDC Ada compiler system: A case study – the Honeywell DPS 6". ACM SIGAda Ada Letters. 6 (1): 22–28. doi:10.1145/382256.382794. S2CID 16337448.
- ↑ Peter Gorm Larsen, "Ten Years of Historical Development "Bootstrapping" VDMTools" Archived 23 January 2021 at the Wayback Machine, In Journal of Universal Computer Science, volume 7(8), 2001
- ↑ Modelling Systems: Practical Tools and Techniques in Software Engineering
- ↑ Validated Designs for Object-oriented Systems
