वियना विकास विधि: Difference between revisions

From Vigyanwiki
No edit summary
No edit summary
 
(9 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 के दशक में, यह एक औपचारिक स्पेसिफिकेशन लैंग्वेज -वीडीएम विशिष्टता लैंग्वेज (वीडीएम-एसएल) पर आधारित तकनीकों और उपकरणों के एक समूह को सम्मिलित करने के लिए विकसित हुआ है। इसका एक विस्तारित रूप है, VDM++,<ref>The double plus is adopted from the [[C++]] objected oriented programming language based on C.</ref> जो [[ वस्तु के उन्मुख | ऑब्जेक्ट-ओरिएंटेड]] और समवर्ती प्रणालियों के मॉडलिंग का समर्थन करता है। वीडीएम के समर्थन में मॉडलों का विश्लेषण करने के लिए वाणिज्यिक और अकादमिक उपकरण सम्मिलित हैं, जिसमें मॉडलों के गुणों का परीक्षण और सिद्ध करने और मान्य वीडीएम मॉडल से प्रोग्राम कोड उत्पन्न करने के लिए समर्थन सम्मिलित है। वीडीएम और उसके उपकरणों के औद्योगिक उपयोग का एक इतिहास है और औपचारिकता में अनुसंधान के बढ़ते समूह ने महत्वपूर्ण प्रणालियों, [[संकलनकर्ता]], समवर्ती प्रणालियों की इंजीनियरिंग और [[कंप्यूटर विज्ञान]] के लिए [[तर्क|लॉजिक]] में उल्लेखनीय योगदान दिया है।
'''वियना डेवलपमेंट मेथड''' (वीडीएम) कंप्यूटर-बेस्ड सिस्टम्स के डेवलपमेंट के लिए सबसे लंबे समय से स्थापित फॉर्मल मेथड में से है। [[आईबीएम प्रयोगशाला वियना]] में किए गए कार्य से उत्पन्न <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>
वीडीएम-एसएल की उत्पत्ति [[वियना]] में [[आईबीएम]] प्रयोगशाला में हुई जहां लैंग्वेज के पहले संस्करण को वियना डेफिनिशन लैंग्वेज (वीडीएल) कहा जाता था।<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>


'''</ब्लॉककोट>'''
«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 और वीडीएम-एसएल का उपयोग करके पूर्वव्यापी रूप से वर्णित या आंशिक रूप से वर्णित अन्य प्रोग्रामिंग लैंग्वेज ओं में [[बुनियादी प्रोग्रामिंग भाषा|बेसिक प्रोग्रामिंग लैंग्वेज]] , [[फोरट्रान]], [[एपीएल प्रोग्रामिंग भाषा|एपीएल प्रोग्रामिंग लैंग्वेज]] , [[ALGOL]] 60, [[एडा प्रोग्रामिंग भाषा|एडा प्रोग्रामिंग लैंग्वेज]]  और [[पास्कल प्रोग्रामिंग भाषा|पास्कल प्रोग्रामिंग लैंग्वेज]]  सम्मिलित हैं। मेटा-IV कई टाइप में विकसित हुआ, जिन्हें समान्यत: डेनिश, अंग्रेजी और आयरिश स्कूलों के रूप में वर्णित किया गया है।


इंग्लिश स्कूल वीडीएम के उन विधियों पर [[क्लिफ जोन्स (कंप्यूटर वैज्ञानिक)]] के काम से प्राप्त हुआ है जो विशेष रूप से लैंग्वेज  डिफ्निसन  और कंपाइलर डिजाइन से संबंधित नहीं हैं (जोन्स 1980, 1990)। यह निरंतर मॉडलिंग पर जोर देता है<ref>See the article on [[Persistence (computer science)|persistence]] for its use within computer science.</ref> आधार टाइप के समृद्ध संग्रह से निर्मित डेटा टाइप के उपयोग के माध्यम से बताएं। कार्यक्षमता को समान्यत: उन ऑपरेशनों के माध्यम से वर्णित किया जाता है जिनके राज्य पर दुष्प्रभाव हो सकते हैं और जो अधिकतर पूर्व नियम और पोस्टकंडिशन का उपयोग करके अंतर्निहित रूप से निर्दिष्ट होते हैं। डेनिश स्कूल (डाइन्स ब्योर्नर या ब्योर्नर एट अल. 1982) ने अधिक सीमा तक उपयोग किए जाने वाले स्पष्ट परिचालन स्पेसिफिकेशन के साथ रचनात्मक दृष्टिकोण पर जोर दिया है। डेनिश स्कूल में काम करने से पहला यूरोपीय मान्य एडा प्रोग्रामिंग लैंग्वेज  कंपाइलर तैयार हुआ।
[[मेटा-IV]] के बीच कोई संबंध नहीं है,<ref>Bjørner&Jones 1978, p.24.</ref> और शोर्रे की मेटा II लैंग्वेज , या इसकी उत्तराधिकारी [[ वृक्ष मेटा |ट्री मेटा]] ; ये फॉर्मल समस्या विवरण के लिए उपयुक्त होने के अतिरिक्त [[ संकलक-संकलक |कम्पाइलर -कम्पाइलर]] सिस्टम थे।


लैंग्वेज के लिए मानकीकरण मानक के लिए एक अंतर्राष्ट्रीय संगठन 1996 में जारी किया गया था (आईएसओ, 1996)।
इसलिए मेटा-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)।


==वीडीएम सुविधाएँ==
==वीडीएम सुविधाएँ==
वीडीएम-एसएल और VDM++ सिंटैक्स और शब्दार्थ का वर्णन VDMTools लैंग्वेज मैनुअल और उपलब्ध टेक्स्ट में विस्तार से किया गया है। आईएसओ मानक में लैंग्वेज के शब्दार्थ की औपचारिक डिफ्निसन सम्मिलित है। इस आलेख के शेष भाग में, आईएसओ-परिभाषित इंटरचेंज (ASCII) सिंटैक्स का उपयोग किया गया है। कुछ टेक्स्ट अधिक संक्षिप्त [[गणितीय संकेतन]] को प्राथमिकता देते हैं।
वीडीएम-एसएल और वीडीएम++ सिंटैक्स और शब्दार्थ का वर्णन वीडीएमटूल्स लैंग्वेज मैनुअल और उपलब्ध टेक्स्ट में विस्तार से किया गया है। आईएसओ मानक में लैंग्वेज के शब्दार्थ की फॉर्मल डिफ्निसन सम्मिलित है। इस आलेख के शेष भाग में, आईएसओ-परिभाषित इंटरचेंज (एएससीआईआई) सिंटैक्स का उपयोग किया गया है। कुछ टेक्स्ट अधिक संक्षिप्त [[गणितीय संकेतन]] को प्राथमिकता देते हैं।


वीडीएम-एसएल मॉडल डेटा पर निष्पादित कार्यक्षमता के संदर्भ में दिया गया एक सिस्टम विवरण है। इसमें डेटा टाइप और उन पर निष्पादित कार्यों या संचालन की डिफ्निसन ओं की एक श्रृंखला सम्मिलित है।
वीडीएम-एसएल मॉडल डेटा पर निष्पादित कार्यक्षमता के कॉन्टेक्स्ट में दिया गया सिस्टम विवरण है। इसमें डेटा टाइप और उन पर निष्पादित कार्यों या संचालन की डिफ्निसन ओं की श्रृंखला सम्मिलित है।


===मूल प्रकार: संख्यात्मक, वर्ण, टोकन और कोटे प्रकार===
===मूल प्रकार: संख्यात्मक, वर्ण, टोकन और कोटे प्रकार===
Line 54: Line 54:
| {{mono|...}}
| {{mono|...}}
|}
|}
डेटा टाइप को मॉडल किए गए सिस्टम के मुख्य डेटा का प्रतिनिधित्व करने के लिए परिभाषित किया गया है। प्रत्येक टाइप की डिफ्निसन एक नए टाइप के नाम का परिचय देती है और मूल टाइप के संदर्भ में या पहले से प्रस्तुत किए गए टाइप के संदर्भ में एक प्रतिनिधित्व देती है। उदाहरण के लिए, लॉग-इन प्रबंधन प्रणाली के लिए एक टाइप के मॉडलिंग उपयोगकर्ता पहचानकर्ता को निम्नानुसार परिभाषित किया जा सकता है:
डेटा टाइप को मॉडल किए गए सिस्टम के मुख्य डेटा का प्रतिनिधित्व करने के लिए परिभाषित किया गया है। प्रत्येक टाइप की डिफ्निसन नए टाइप के नाम का परिचय देती है और मूल टाइप के कॉन्टेक्स्ट में या पहले से प्रस्तुत किए गए टाइप के कॉन्टेक्स्ट में प्रतिनिधित्व देती है। उदाहरण के लिए, लॉग-इन मैनेजमेंट सिस्टम के लिए टाइप के मॉडलिंग उपयोगकर्ता पहचानकर्ता को निम्नानुसार परिभाषित किया जा सकता है:


  types
  types
  UserId = nat
  UserId = nat


डेटा टाइप से संबंधित मूल्यों में परिवर्तन करने के लिए, ऑपरेटरों को मूल्यों पर परिभाषित किया जाता है। इस प्रकार, प्राकृतिक संख्या जोड़, घटाव आदि प्रदान किए जाते हैं, जैसे कि समानता और असमानता जैसे बूलियन ऑपरेटर होते हैं। लैंग्वेज अधिकतम या न्यूनतम प्रतिनिधित्व योग्य संख्या या वास्तविक संख्याओं के लिए कोई परिशुद्धता तय नहीं करती है। ऐसी बाधाओं को परिभाषित किया जाता है जहां डेटा टाइप के इनवेरिएंट के माध्यम से प्रत्येक मॉडल में उनकी आवश्यकता होती है - बूलियन अभिव्यक्तियां उन स्थितियों को दर्शाती हैं जिनका परिभाषित टाइप के सभी तत्वों द्वारा सम्मान किया जाना चाहिए। उदाहरण के लिए, एक आवश्यकता कि उपयोगकर्ता पहचानकर्ता 9999 से अधिक नहीं होने चाहिए, निम्नानुसार व्यक्त की जाएगी (जहां <code><=</code> प्राकृतिक संख्याओं पर बूलियन ऑपरेटर से कम या उसके समान है):
डेटा टाइप से संबंधित मूल्यों में परिवर्तन करने के लिए, ऑपरेटरों को मूल्यों पर परिभाषित किया जाता है। इस प्रकार, प्राकृतिक संख्या जोड़, घटाव आदि प्रदान किए जाते हैं, जैसे कि समानता और असमानता जैसे बूलियन ऑपरेटर होते हैं। लैंग्वेज अधिकतम या न्यूनतम प्रतिनिधित्व योग्य संख्या या वास्तविक संख्याओं के लिए कोई परिशुद्धता तय नहीं करती है। ऐसी बाधाओं को परिभाषित किया जाता है जहां डेटा टाइप के इनवेरिएंट के माध्यम से प्रत्येक मॉडल में उनकी आवश्यकता होती है - बूलियन अभिव्यक्तियां उन स्थितियों को दर्शाती हैं जिनका परिभाषित टाइप के सभी कॉम्पोनेन्टं द्वारा सम्मान किया जाना चाहिए। उदाहरण के लिए, आवश्यकता कि उपयोगकर्ता पहचानकर्ता 9999 से अधिक नहीं होने चाहिए, निम्नानुसार व्यक्त की जाएगी (जहां <code><=</code> प्राकृतिक संख्याओं पर बूलियन ऑपरेटर से कम या उसके समान है):


  UserId = nat
  UserId = nat
  inv uid == uid <= 9999
  inv uid == uid <= 9999


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


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


उदाहरण के लिए, ट्रैफ़िक सिग्नल नियंत्रक के मॉडलिंग में, ट्रैफ़िक सिग्नल के रंगों को कोटे टाइप के रूप में दर्शाने के लिए मानों को परिभाषित करना सुविधाजनक हो सकता है:
उदाहरण के लिए, ट्रैफ़िक सिग्नल कंट्रोलर के मॉडलिंग में, ट्रैफ़िक सिग्नल के रंगों को कोटे टाइप के रूप में दर्शाने के लिए मानों को परिभाषित करना सुविधाजनक हो सकता है:


  <Red>, <Amber>, <FlashingAmber>, <Green>
  <Red>, <Amber>, <FlashingAmber>, <Green>
Line 83: Line 83:
| <code>T :: f1:T1 ... fn:Tn</code>  ||समग्र (रिकॉर्ड) प्रकार
| <code>T :: f1:T1 ... fn:Tn</code>  ||समग्र (रिकॉर्ड) प्रकार
|}
|}
सबसे बेसिक टाइप का कंस्ट्रक्टर दो पूर्वनिर्धारित टाइप का मिलन बनाता है। प्ररूप <code>(A|B)</code> इसमें A टाइप के सभी तत्व और टाइप के सभी तत्व सम्मिलित हैं <code>B</code>. ट्रैफ़िक सिग्नल नियंत्रक उदाहरण में, ट्रैफ़िक सिग्नल के रंग मॉडलिंग के टाइप को निम्नानुसार परिभाषित किया जा सकता है:
सबसे बेसिक टाइप का कंस्ट्रक्टर दो पूर्वनिर्धारित टाइप का मिलन बनाता है। प्ररूप <code>(A|B)</code> इसमें A टाइप के सभी कॉम्पोनेन्ट और टाइप के सभी कॉम्पोनेन्ट सम्मिलित हैं <code>B</code>. ट्रैफ़िक सिग्नल कंट्रोलर उदाहरण में, ट्रैफ़िक सिग्नल के रंग मॉडलिंग के टाइप को निम्नानुसार परिभाषित किया जा सकता है:


  SignalColour = <Red> | <Amber> | <FlashingAmber> | <Green>
  SignalColour = <Red> | <Amber> | <FlashingAmber> | <Green>


वीडीएम-एसएल में [[प्रगणित प्रकार|प्रगणित]] टाइप को कोटे टाइप पर यूनियनों के रूप में ऊपर दिखाए गए अनुसार परिभाषित किया गया है।
वीडीएम-एसएल में [[प्रगणित प्रकार|प्रगणित]] टाइप को कोटे टाइप पर यूनियनों के रूप में ऊपर दिखाए गए अनुसार परिभाषित किया गया है।


कार्टेशियन प्रोडक्ट टाइप को वीडीएम-एसएल में भी परिभाषित किया जा सकता है। प्ररूप <code>(A1*…*An)</code> मानों के सभी टुपल्स से बना टाइप है, जिसका पहला तत्व टाइप से है <code>A1</code> और दूसरा टाइप से <code>A2</code> और इसी तरह मिश्रित या रिकॉर्ड टाइप एक कार्टेशियन प्रोडक्ट है जिसमें फ़ील्ड के लिए लेबल होते हैं। प्ररूप
कार्टेशियन प्रोडक्ट टाइप को वीडीएम-एसएल में भी परिभाषित किया जा सकता है। प्ररूप <code>(A1*…*An)</code> मानों के सभी टुपल्स से बना टाइप है, जिसका पहला कॉम्पोनेन्ट टाइप से है <code>A1</code> और दूसरा टाइप से <code>A2</code> और इसी तरह मिश्रित या रिकॉर्ड टाइप कार्टेशियन प्रोडक्ट है जिसमें फ़ील्ड के लिए लेबल होते हैं। प्ररूप


  T :: f1:A1
  T :: f1:A1
      f2:A2
  f2:A2
      ...
  ...
      fn:An
  fn:An


<code>f1,…,fn</code> लेबल वाले फ़ील्ड वाला कार्टेशियन प्रोडक्ट है। टाइप <code>T</code> का एक तत्व उसके घटक भागों से एक कंस्ट्रक्टर द्वारा बनाया जा सकता है, जिसे <code>mk_T</code> लिखा जाता है। इसके विपरीत, टाइप <code>T</code>का एक तत्व दिए जाने पर, नामित घटक का चयन करने के लिए फ़ील्ड नामों का उपयोग किया जा सकता है। उदाहरण के लिए, प्रकार
<code>f1,…,fn</code> लेबल वाले फ़ील्ड वाला कार्टेशियन प्रोडक्ट है। टाइप <code>T</code> का कॉम्पोनेन्ट उसके घटक भागों से कंस्ट्रक्टर द्वारा बनाया जा सकता है, जिसे <code>mk_T</code> लिखा जाता है। इसके विपरीत, टाइप <code>T</code>का कॉम्पोनेन्ट दिए जाने पर, नामित घटक का चयन करने के लिए फ़ील्ड नामों का उपयोग किया जा सकता है। उदाहरण के लिए, प्रकार


  Date :: day:nat1
  Date :: day:nat1
        month:nat1
  month:nat1
        year:nat
  year:nat
  inv mk_Date(d,m,y) == d <=31 and m<=12
  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> महीने का प्रतिनिधित्व करने वाली एक प्राकृतिक संख्या है। यदि चाहें तो प्रति माह दिनों और लीप वर्ष पर प्रतिबंध को अपरिवर्तनीय में सम्मिलित किया जा सकता है। इनका संयोजन:
एक साधारण दिनांक टाइप मॉडल करता है। मान <code>mk_Date(1,4,2001)</code> 1 अप्रैल 2001 से मेल खाता है। दिनांक <code>d</code> दी गई है अभिव्यक्ति <code>d.month</code> महीने का प्रतिनिधित्व करने वाली प्राकृतिक संख्या है। यदि चाहें तो प्रति माह दिनों और लीप वर्ष पर प्रतिबंध को अपरिवर्तनीय में सम्मिलित किया जा सकता है। इनका संयोजन:


  mk_Date(1,4,2001).month = 4
  mk_Date(1,4,2001).month = 4


===कलेक्शन्स ===
===कलेक्शन्स ===
संग्रह टाइप मानो के मॉडल समूह सेट परिमित अव्यवस्थित संग्रह हैं जिनमें मानों के बीच दोहराव को दबा दिया जाता है। अनुक्रम परिमित क्रमित संग्रह (सूचियाँ) हैं जिनमें दोहराव हो सकता है और मैपिंग मानों के दो सेटों के बीच परिमित कॉरेस्पोंडेंस का प्रतिनिधित्व करते हैं।
स्टोर टाइप मानो के मॉडल समूह सेट परिमित अव्यवस्थित स्टोर हैं जिनमें मानों के बीच दोहराव को दबा दिया जाता है। अनुक्रम परिमित क्रमित स्टोर (सूचियाँ) हैं जिनमें दोहराव हो सकता है और मैपिंग मानों के दो सेटों के बीच परिमित कॉरेस्पोंडेंस का प्रतिनिधित्व करते हैं।


==== सेट ====
==== सेट ====
सेट टाइप का कंस्ट्रक्टर (<code>T</code> का लिखित <code>set of T</code> एक पूर्वनिर्धारित टाइप है) टाइप <code>T</code> से खींचे गए मानों के सभी परिमित सेटों से बना टाइप का निर्माण करता है। उदाहरण के लिए टाइप की परिभाषा<syntaxhighlight>
सेट टाइप का कंस्ट्रक्टर (<code>T</code> का लिखित <code>set of T</code> पूर्वनिर्धारित टाइप है) टाइप <code>T</code> से खींचे गए मानों के सभी परिमित सेटों से बना टाइप का निर्माण करता है। उदाहरण के लिए टाइप की परिभाषा<syntaxhighlight>
UGroup = set of UserId
UGroup = set of UserId
</syntaxhighlight><code>UserId</code>मानों के सभी परिमित सेटों से बना एक टाइप <code>UGroup</code> को परिभाषित करता है। विभिन्न ऑपरेटरों को उनके संघ, प्रतिच्छेदन, उचित और गैर-सख्त सबसेट संबंधों का निर्धारण आदि के लिए सेट पर परिभाषित किया गया है।
</syntaxhighlight><code>UserId</code>मानों के सभी परिमित सेटों से बना टाइप <code>UGroup</code> को परिभाषित करता है। विभिन्न ऑपरेटरों को उनके संघ, प्रतिच्छेदन, उचित और गैर-सख्त सबसेट संबंधों का निर्धारण आदि के लिए सेट पर परिभाषित किया गया है।
{| class="wikitable" border="1"
{| class="wikitable" border="1"
|+ style="background:#ffdead;" |सेट पर मुख्य ऑपरेटर (s, s1, s2 सेट हैं)
|+ style="background:#ffdead;" |सेट पर मुख्य ऑपरेटर (s, s1, s2 सेट हैं)
|-
|-
| <code>{a, b, c}</code> || Set enumeration: the set of elements <code>a</code>, <code>b</code> and <code>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> || Set comprehension: the set of <code>x</code> from type <code>T</code> such that <code>P(x)</code>
| <code><nowiki>{x | x:T & P(x)}</nowiki></code> || सेट कॉम्प्रिहेंशन: का सेट <code>x</code> का प्रकार <code>T</code> ऐसा है कि <code>P(x)</code>
|-
|-
| <code>{i, ..., j}</code> || The set of integers in the range <code>i</code> to <code>j</code>
| <code>{i, ..., j}</code> || <code>i</code> से <code>j</code> की सीमा में पूर्णांकों का समुच्चय
|-
|-
| <code>e in set s</code> || <code>e</code> is an element of set <code>s</code>
| <code>e in set s</code> || <code>e</code> सेट <code>s</code> का एलिमेंट है
|-
|-
| <code>e not in set s</code> || <code>e</code> is not an element of set <code>s</code>
| <code>e not in set s</code> || <code>e</code> सेट <code>s</code> का एलिमेंट नहीं है
|-
|-
| <code>s1 union s2</code> || Union of sets <code>s1</code> and <code>s2</code>
| <code>s1 union s2</code> || सेट <code>s1</code> और <code>s2</code> का यूनियन
|-
|-
| <code>s1 inter s2</code> || Intersection of sets <code>s1</code> and <code>s2</code>
| <code>s1 inter s2</code> || सेट <code>s1</code> और <code>s2</code> का प्रतिच्छेदन
|-
|-
| <code>s1 \ s2</code> || Set difference of sets <code>s1</code> and <code>s2</code>
| <code>s1 \ s2</code> || सेट s1 और s2 का अंतर निर्धारित करें
|-
|-
| <code>dunion s</code> || Distributed union of set of sets <code>s</code>
| <code>dunion s</code> || सेट के सेट का डिस्ट्रीब्यूटेड यूनियन s
|-
|-
| <code>s1 psubset s2</code> || s1 is a (proper) subset of <code>s2</code>
| <code>s1 psubset s2</code> || s1, <code>s2</code> का एक (प्रोपर) सबसेट है
|-
|-
| <code>s1 subset s2</code>  || s1 is a (weak) subset of <code>s2</code>
| <code>s1 subset s2</code>  || s1 , <code>s2</code> का एक (अशक्त) सबसेट है
|-
|-
| <code>card s</code> || The cardinality of set <code>s</code>
| <code>card s</code> || सेट <code>s</code> की कार्डिनैलिटी
|}
|}




==== अनुक्रम ====
==== अनुक्रम ====
परिमित अनुक्रम टाइप कंस्ट्रक्टर (लिखित) <code>seq of T</code> कहाँ <code>T</code> एक पूर्वनिर्धारित टाइप है) टाइप से निकाले गए मानों की सभी सीमित सूचियों से बना टाइप बनाता है <code>T</code>. उदाहरण के लिए, टाइप की डिफ्निसन  
परिमित अनुक्रम टाइप कंस्ट्रक्टर (लिखित) <code>seq of T</code> जहाँ <code>T</code> पूर्वनिर्धारित टाइप है) टाइप से निकाले गए मानों की सभी सीमित सूचियों से बना टाइप <code>T</code> बनाता है . उदाहरण के लिए, टाइप की डिफ्निसन  


  String = seq of char
  String = seq of char


एक टाइप को परिभाषित करता है <code>String</code> वर्णों की सभी सीमित श्रृंखलाओं से बना है। विभिन्न ऑपरेटरों को संयोजन के निर्माण, तत्वों और उसके बाद के अनुक्रम आदि के चयन के लिए अनुक्रमों पर परिभाषित किया गया है। इनमें से कई ऑपरेटर इस अर्थ में आंशिक हैं कि उन्हें कुछ अनुप्रयोगों के लिए परिभाषित नहीं किया गया है। उदाहरण के लिए, किसी अनुक्रम के 5वें तत्व का चयन करना जिसमें केवल तीन तत्व हैं, अपरिभाषित है।
एक टाइप को परिभाषित करता है <code>String</code> वर्णों की सभी सीमित श्रृंखलाओं से बना है। विभिन्न ऑपरेटरों को संयोजन के निर्माण, कॉम्पोनेन्टं और उसके पश्चात् के अनुक्रम आदि के चयन के लिए अनुक्रमों पर परिभाषित किया गया है। इनमें से कई ऑपरेटर इस अर्थ में आंशिक हैं कि उन्हें कुछ अनुप्रयोगों के लिए परिभाषित नहीं किया गया है। उदाहरण के लिए, किसी अनुक्रम के 5वें कॉम्पोनेन्ट का चयन करना जिसमें केवल तीन कॉम्पोनेन्ट हैं, अपरिभाषित है।


इसलिए, एक क्रम में वस्तुओं का क्रम और पुनरावृत्ति महत्वपूर्ण है <code>[a, b]</code> के समान नहीं है <code>[b, a]</code>, और <code>[a]</code> के समान नहीं है <code>[a, a]</code>.
इसलिए, क्रम में वस्तुओं का क्रम और पुनरावृत्ति महत्वपूर्ण है <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;" |अनुक्रमों पर मुख्य संचालक (s, s1,s2 अनुक्रम हैं)
|+ style="background:#ffdead;" |अनुक्रमों पर मुख्य संचालक (s, s1,s2 अनुक्रम हैं)
|-
|-
| <code>[a, b, c]</code> || अनुक्रम गणना: तत्वों <code>a</code>, <code>b</code> and <code>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> || अनुक्रम बोध: (संख्यात्मक) प्रकार T के प्रत्येक x के लिए अभिव्यक्ति f(x) का अनुक्रम इस प्रकार है कि P(x) बना रहे
| <code><nowiki>[f(x) | x:T & P(x)]</nowiki></code> || अनुक्रम बोध: (संख्यात्मक) प्रकार T के प्रत्येक x के लिए अभिव्यक्ति f(x) का अनुक्रम इस प्रकार है कि P(x) बना रहे
(x मान संख्यात्मक क्रम में लिया गया है)
(x मान संख्यात्मक क्रम में लिया गया है)
|-
|-
| <code>hd s</code> || <code>s</code>का प्रमुख (प्रथम तत्व)
| <code>hd s</code> || <code>s</code>का प्रमुख (प्रथम अवयव)
|-
|-
| <code>tl s</code> ||<code>s</code>की पूँछ (सिर हटाने के बाद शेष क्रम)।
| <code>tl s</code> ||<code>s</code>की पूँछ (सिर हटाने के पश्चात् शेष क्रम)।
|-
|-
| <code>len s</code> ||<code>s</code>की लंबाई
| <code>len s</code> ||<code>s</code>की लंबाई
|-
|-
| <code>elems s</code> ||<code>s</code>के तत्वों का सेट
| <code>elems s</code> ||<code>s</code>के कॉम्पोनेन्टं का सेट
|-
|-
| <code>s(i)</code> || <code>s का i<sup>th</sup> तत्व</code>
| <code>s(i)</code> || <code>s का i<sup>th</sup> अवयव</code>
|-
|-
| <code>inds s</code> ||अनुक्रम के लिए सूचकांकों का सेट <code>s</code>  
| <code>inds s</code> ||अनुक्रम के लिए सूचकांकों का सेट <code>s</code>  
Line 177: Line 177:


==== मानचित्र ====
==== मानचित्र ====
एक परिमित मानचित्रण दो सेटों, डोमेन और रेंज के बीच, रेंज के डोमेन अनुक्रमण तत्वों के साथ एक कॉरेस्पोंडेंस है। इसलिए यह एक परिमित कार्य के समान है। वीडीएम-एसएल में मैपिंग टाइप का कंस्ट्रक्टर (लिखित) <code>map T1 to T2</code> जहाँ <code>T1</code> और <code>T2</code> पूर्वनिर्धारित टाइप हैं) सेट से सभी परिमित मैपिंग से बने टाइप का निर्माण करता है जिसमे<code>T1</code> के सेट के लिए मान <code>T2</code> मूल्य. उदाहरण के लिए, टाइप की डिफ्निसन  
एक परिमित मानचित्रण दो सेटों, डोमेन और रेंज के बीच, रेंज के डोमेन अनुक्रमण कॉम्पोनेन्टं के साथ कॉरेस्पोंडेंस है। इसलिए यह परिमित कार्य के समान है। वीडीएम-एसएल में मैपिंग टाइप का कंस्ट्रक्टर (लिखित) <code>map T1 to T2</code> जहाँ <code>T1</code> और <code>T2</code> पूर्वनिर्धारित टाइप हैं) सेट से सभी परिमित मैपिंग से बने टाइप का निर्माण करता है जिसमे<code>T1</code> के सेट के लिए मान <code>T2</code> मूल्य. उदाहरण के लिए, टाइप की डिफ्निसन  


  Birthdays = map String to Date
  Birthdays = map String to Date
Line 184: Line 184:


{| border="1" class="wikitable"
{| border="1" class="wikitable"
|+ style="background:#ffdead;" |Main operators on mappings
|+ style="background:#ffdead;" |मैपिंग पर मुख्य ऑपरेटर
|-
|-
| <code><nowiki>{a |-> r, b |-> s}</nowiki></code> || Mapping enumeration: <code>a</code> maps to <code>r</code>, <code>b</code> maps to <code>s</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> || Mapping comprehension: <code>x</code> maps to <code>f(x)</code> for all <code>x</code> for type <code>T</code> such that <code>P(x)</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> || The domain of <code>m</code>
| <code>dom m</code> || <code>m</code> का डोमेन
|-
|-
| <code>rng m</code> || The range of <code>m</code>
| <code>rng m</code> || <code>m की रेंज</code>
|-
|-
| <code>m(x)</code> || <code>m</code> applied to <code>x</code>
| <code>m(x)</code> || <code>m</code> <code>x</code> पर प्रयुक्त होता है
|-
|-
| <code>m1 munion m2</code> || Union of mappings <code>m1</code> and <code>m2</code> (<code>m1</code>, <code>m2</code> must be consistent where they overlap)
| <code>m1 munion m2</code> || मैपिंग <code>m1</code> और <code>m2</code> (<code>m1</code>, <code>m2</code> जहां वह ओवरलैप होते हैं वहां सुसंगत होना चाहिए)  
|-
|-
| <code>m1 ++ m2</code> || <code>m1</code> overwritten by <code>m2</code>
| <code>m1 ++ m2</code> || <code>m1</code> को <code>m2</code> द्वारा अधिलेखित किया गया
|}
|}




===संरचना===
===संरचना===
वीडीएम-एसएल और VDM++ नोटेशन के बीच मुख्य अंतर संरचना से निपटने के तरीके में है। वीडीएम-एसएल में एक पारंपरिक मॉड्यूलर एक्सटेंशन है जबकि वीडीएम++ में कक्षाओं और विरासत के साथ एक पारंपरिक ऑब्जेक्ट-ओरिएंटेड संरचना तंत्र है।
वीडीएम-एसएल और वीडीएम++ नोटेशन के बीच मुख्य अंतर संरचना से सामना करने के मेथड में है। वीडीएम-एसएल में पारंपरिक मॉड्यूलर एक्सटेंशन है जबकि वीडीएम++ में क्लास और इनहेरिटेंस के साथ पारंपरिक ऑब्जेक्ट-ओरिएंटेड संरचना तंत्र है।


====वीडीएम-एसएल में संरचना====
====वीडीएम-एसएल में संरचना====
वीडीएम-एसएल के लिए आईएसओ मानक में एक सूचनात्मक अनुबंध है जिसमें विभिन्न संरचना सिद्धांत सम्मिलित हैं। ये सभी मॉड्यूल के साथ पारंपरिक जानकारी छिपाने के सिद्धांतों का पालन करते हैं और इन्हें इस टाइप समझाया जा सकता है:
वीडीएम-एसएल के लिए आईएसओ मानक में सूचनात्मक अनुबंध है जिसमें विभिन्न संरचना सिद्धांत सम्मिलित हैं। ये सभी मॉड्यूल के साथ पारंपरिक जानकारी छिपाने के सिद्धांतों का पालन करते हैं और इन्हें इस टाइप कॉम्प्रिहेंशनाया जा सकता है:
* मॉड्यूल नामकरण: प्रत्येक मॉड्यूल वाक्यात्मक रूप से कीवर्ड से शुरू होता है <code>module</code> इसके बाद मॉड्यूल का नाम आता है। मॉड्यूल के अंत में कीवर्ड <code>end</code> मॉड्यूल के नाम के बाद फिर से लिखा गया है।
* मॉड्यूल नामकरण: प्रत्येक मॉड्यूल वाक्यात्मक रूप से कीवर्ड से प्रारंभ होता है <code>module</code> इसके पश्चात् मॉड्यूल का नाम आता है। मॉड्यूल के अंत में कीवर्ड <code>end</code> मॉड्यूल के नाम के पश्चात् फिर से लिखा गया है।
* आयात करना: अन्य मॉड्यूल से निर्यात की गई डिफ्निसन ओं को आयात करना संभव है। यह ''आयात अनुभाग'' में किया जाता है जिसकी शुरुआत कीवर्ड से होती है <code>imports</code> और उसके बाद विभिन्न मॉड्यूल से आयात का क्रम चलता है। इनमें से प्रत्येक मॉड्यूल आयात कीवर्ड से शुरू होता है <code>from</code> उसके बाद मॉड्यूल का नाम और मॉड्यूल हस्ताक्षर आता है। मॉड्यूल हस्ताक्षर या तो केवल कीवर्ड हो सकता है <code>all</code> उस मॉड्यूल से निर्यात की गई सभी डिफ्निसन ओं के आयात को इंगित करना, या यह आयात हस्ताक्षरों का एक क्रम हो सकता है। आयात हस्ताक्षर प्रकार, मान, फ़ंक्शन और संचालन के लिए विशिष्ट होते हैं और इनमें से प्रत्येक संबंधित कीवर्ड से शुरू होते हैं। इसके अलावा ये आयात हस्ताक्षर उन निर्माणों का नाम देते हैं जिन तक पहुंच प्राप्त करने की इच्छा है। इसके अलावा वैकल्पिक टाइप की जानकारी मौजूद हो सकती है और अंततः आयात पर प्रत्येक निर्माण का नाम बदलना संभव है। टाइप के लिए कीवर्ड का भी उपयोग करना होगा <code>struct</code> यदि कोई किसी विशेष टाइप की आंतरिक संरचना तक पहुंच प्राप्त करना चाहता है।
* आयात करना: अन्य मॉड्यूल से निर्यात की गई डिफ्निसन ओं को आयात करना संभव है। यह ''आयात अनुभाग'' में किया जाता है जिसकी प्रारंभिक कीवर्ड से होती है <code>imports</code> और उसके पश्चात् विभिन्न मॉड्यूल से आयात का क्रम चलता है। इनमें से प्रत्येक मॉड्यूल आयात कीवर्ड से प्रारंभ होता है <code>from</code> उसके पश्चात् मॉड्यूल का नाम और मॉड्यूल हस्ताक्षर आता है। मॉड्यूल हस्ताक्षर या तो केवल कीवर्ड हो सकता है <code>all</code> उस मॉड्यूल से निर्यात की गई सभी डिफ्निसन ओं के आयात को निरुपित करना, या यह आयात हस्ताक्षरों का क्रम हो सकता है। आयात हस्ताक्षर प्रकार, मान, फ़ंक्शन और संचालन के लिए विशिष्ट होते हैं और इनमें से प्रत्येक संबंधित कीवर्ड से प्रारंभ होते हैं। इसके अतिरिक्त ये आयात हस्ताक्षर उन निर्माणों का नाम देते हैं जिन तक पहुंच प्राप्त करने की इच्छा है। इसके अतिरिक्त वैकल्पिक टाइप की जानकारी उपस्थित हो सकती है और अंततः आयात पर प्रत्येक निर्माण का नाम परिवर्तित करना संभव है। टाइप के लिए कीवर्ड का भी उपयोग करना होगा <code>struct</code> यदि कोई किसी विशेष टाइप की आंतरिक संरचना तक पहुंच प्राप्त करना चाहता है।
* 'निर्यात': एक मॉड्यूल की डिफ्निसन एँ, जिन तक कोई अन्य मॉड्यूल की पहुंच चाहता है, कीवर्ड का उपयोग करके निर्यात की जाती हैं <code>exports</code> इसके बाद एक निर्यात मॉड्यूल हस्ताक्षर होगा। निर्यात मॉड्यूल हस्ताक्षर में या तो केवल कीवर्ड सम्मिलित हो सकता है <code>all</code> या निर्यात हस्ताक्षरों के अनुक्रम के रूप में। ऐसे निर्यात हस्ताक्षर प्रकार, मान, फ़ंक्शन और संचालन के लिए विशिष्ट होते हैं और इनमें से प्रत्येक संबंधित कीवर्ड से शुरू होते हैं। यदि कोई किसी टाइप की कीवर्ड की आंतरिक संरचना को निर्यात करना चाहता है <code>struct</code> उपयोग किया जाना चाहिए।
* 'निर्यात': मॉड्यूल की डिफ्निसन, जिन तक कोई अन्य मॉड्यूल की पहुंच चाहता है, कीवर्ड का उपयोग करके निर्यात की जाती हैं <code>exports</code> इसके पश्चात् निर्यात मॉड्यूल हस्ताक्षर होगा। निर्यात मॉड्यूल हस्ताक्षर में या तो केवल कीवर्ड सम्मिलित हो सकता है <code>all</code> या निर्यात हस्ताक्षरों के अनुक्रम के रूप में। ऐसे निर्यात हस्ताक्षर प्रकार, मान, फ़ंक्शन और संचालन के लिए विशिष्ट होते हैं और इनमें से प्रत्येक संबंधित कीवर्ड से प्रारंभ होते हैं। यदि कोई किसी टाइप की कीवर्ड की आंतरिक संरचना को निर्यात करना चाहता है <code>struct</code> उपयोग किया जाना चाहिए।
* अधिक विदेशी विशेषताएं: वीडीएम-एसएल टूल के पुराने संस्करणों में पैरामीटरयुक्त मॉड्यूल और ऐसे मॉड्यूल के इंस्टेंटेशन के लिए भी समर्थन था। हालाँकि, इन सुविधाओं को 2000 के आसपास VDMTools से हटा दिया गया था क्योंकि इनका उपयोग शायद ही कभी औद्योगिक अनुप्रयोगों में किया गया था और इन सुविधाओं के साथ बड़ी संख्या में टूल चुनौतियाँ थीं।
* अधिक विदेशी विशेषताएं: वीडीएम-एसएल टूल के पुराने संस्करणों में पैरामीटरयुक्त मॉड्यूल और ऐसे मॉड्यूल के इंस्टेंटेशन के लिए भी समर्थन था। चूँकि , इन सुविधाओं को 2000 के आसपास वीडीएमटूल्स से हटा दिया गया था क्योंकि इनका उपयोग संभवतः ही कभी औद्योगिक अनुप्रयोगों में किया गया था और इन सुविधाओं के साथ बड़ी संख्या में टूल चुनौतियाँ थीं।


=== VDM++ में संरचना ===
=== वीडीएम++ में संरचना ===
VDM++ में कक्षाओं और एकाधिक वंशानुक्रम का उपयोग करके संरचना की जाती है। प्रमुख अवधारणाएँ हैं:
वीडीएम++ में क्लास और एकाधिक इनहेरिटेंस का उपयोग करके संरचना की जाती है। प्रमुख अवधारणाएँ हैं:
* क्लास: प्रत्येक क्लास वाक्यात्मक रूप से कीवर्ड से शुरू होती है <code>class</code> इसके बाद वर्ग का नाम आता है। कक्षा के अंत में कीवर्ड <code>end</code> इसके बाद फिर से कक्षा का नाम लिखा जाता है।
* क्लास: प्रत्येक क्लास वाक्यात्मक रूप से कीवर्ड से प्रारंभ होती है <code>class</code> इसके पश्चात् वर्ग का नाम आता है। कक्षा के अंत में कीवर्ड <code>end</code> इसके पश्चात् फिर से कक्षा का नाम लिखा जाता है।
* वंशानुक्रम: यदि किसी वर्ग को अन्य वर्गों से संरचनाएं विरासत में मिलती हैं तो वर्ग शीर्षक में वर्ग नाम के बाद कीवर्ड का उपयोग किया जा सकता है <code>is subclass of</code> उसके बाद सुपरक्लास के नामों की अल्पविराम से अलग की गई सूची।
* इनहेरिटेंस: यदि किसी वर्ग को अन्य वर्गों से संरचनाएं इनहेरिटेंस में मिलती हैं तो वर्ग शीर्षक में वर्ग नाम के पश्चात् कीवर्ड का उपयोग किया जा सकता है <code>is subclass of</code> उसके पश्चात् सुपरक्लास के नामों की अल्पविराम से अलग की गई सूची।
* एक्सेस संशोधक: VDM++ में जानकारी छिपाना उसी तरह से किया जाता है जैसे अधिकांश ऑब्जेक्ट ओरिएंटेड लैंग्वेज ओं में एक्सेस संशोधक का उपयोग करके किया जाता है। VDM++ में डिफ्निसन एँ डिफ़ॉल्ट रूप से निजी होती हैं लेकिन सभी डिफ्निसन ओं के सामने एक्सेस संशोधक कीवर्ड में से किसी एक का उपयोग करना संभव है: <code>private</code>, <code>public</code> और <code>protected</code>.
* एक्सेस संशोधक: वीडीएम++ में जानकारी हिडेन करना उसी तरह से किया जाता है जैसे अधिकांश ऑब्जेक्ट ओरिएंटेड लैंग्वेज ओं में एक्सेस संशोधक का उपयोग करके किया जाता है। वीडीएम++ में डिफ्निसन एँ डिफ़ॉल्ट रूप से निजी होती हैं किंतु सभी डिफ्निसन ओं के सामने एक्सेस संशोधक कीवर्ड <code>private</code>, <code>public</code> और <code>protected</code> में से किसी का उपयोग करना संभव है:.


==मॉडलिंग कार्यक्षमता==
==मॉडलिंग कार्यक्षमता==
Line 222: Line 222:
===कार्यात्मक मॉडलिंग===
===कार्यात्मक मॉडलिंग===


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


  SQRT(x:nat)r:real
  SQRT(x:nat)r:real
  post r*r = x
  post r*r = x


यहां पोस्टकंडिशन परिणाम की गणना के लिए एक मेथड को परिभाषित नहीं करता है <code>r</code> लेकिन यह बताता है कि इसके पास कौन से गुण माने जा सकते हैं। ध्यान दें कि यह एक फ़ंक्शन को परिभाषित करता है जो एक वैध वर्गमूल लौटाता है; इसकी कोई आवश्यकता नहीं है कि यह सकारात्मक या नकारात्मक मूल होना चाहिए। उपरोक्त स्पेसिफिकेशन संतुष्ट होंगे, उदाहरण के लिए, एक फ़ंक्शन द्वारा जो 4 का नकारात्मक मूल लेकिन अन्य सभी वैध इनपुट का सकारात्मक मूल लौटाता है। ध्यान दें कि वीडीएम-एसएल में फ़ंक्शंस को नियतात्मक होना आवश्यक है जिससे ऊपर दिए गए उदाहरण स्पेसिफिकेशन को संतुष्ट करने वाला फ़ंक्शन हमेशा समान इनपुट के लिए समान परिणाम लौटाए।
यहां पोस्टकंडिशन परिणाम की गणना के लिए मेथड <code>r</code> परिभाषित नहीं करता है किंतु यह बताता है कि इसके पास कौन से गुण माने जा सकते हैं। ध्यान दें कि यह फ़ंक्शन को परिभाषित करता है जो वैध वर्गमूल लौटाता है; इसकी कोई आवश्यकता नहीं है कि यह धनात्मक या ऋणात्मक मूल होना चाहिए। उपरोक्त स्पेसिफिकेशन संतुष्ट होंगे, उदाहरण के लिए फ़ंक्शन द्वारा जो 4 का ऋणात्मक मूल किंतु अन्य सभी वैध इनपुट का धनात्मक मूल लौटाता है। ध्यान दें कि वीडीएम-एसएल में फ़ंक्शंस को नियतात्मक होना आवश्यक है जिससे ऊपर दिए गए उदाहरण स्पेसिफिकेशन को संतुष्ट करने वाला फ़ंक्शन सदैव समान इनपुट के लिए समान परिणाम लौटाए गए।


पोस्टकंडीशन को मजबूत करके एक अधिक बाधित फ़ंक्शन स्पेसिफिकेशन प्राप्त किया जाता है। उदाहरण के लिए, निम्नलिखित डिफ्निसन फ़ंक्शन को सकारात्मक रूट वापस करने के लिए बाध्य करती है।
पोस्टकंडीशन को प्रबल करके अधिक बाधित फ़ंक्शन स्पेसिफिकेशन प्राप्त किया जाता है। उदाहरण के लिए, निम्नलिखित डिफ्निसन फ़ंक्शन को धनात्मक रूट वापस करने के लिए बाध्य करती है।


  SQRT(x:nat)r:real
  SQRT(x:nat)r:real
  post r*r = x and r>=0
  post r*r = x and r>=0


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


  SQRTP(x:real)r:real
  SQRTP(x:real)r:real
Line 240: Line 240:
  post r*r = x and r>=0
  post r*r = x and r>=0


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


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


  SqList: seq of nat -> seq of nat
  SqList: seq of nat -> seq of nat
  SqList(s) == if s = [] then [] else [(hd s)**2] ^ SqList(tl 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
  post len r = len s and
      forall i in set inds s & r(i) = s(i)**2
  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)
  pre pre-f(p)
  post post-f(p, r)
  post post-f(p, r)


और एक स्पष्ट कार्य:
और स्पष्ट कार्य:
  f:T_p -> T_r
  f:T_p -> T_r


Line 266: Line 266:
  forall p in set T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))
  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>f</code> स्पेसिफिकेशन को पूरा करता है.


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


उदाहरण के लिए, यदि हमारे पास एक एकल चर से युक्त एक राज्य है <code>someStateRegister : nat</code>, हम इसे वीडीएम-एसएल में इस टाइप परिभाषित कर सकते हैं:
उदाहरण के लिए, यदि हमारे पास एकल वेरिएबल से युक्त स्टेट है <code>someStateRegister : nat</code>, हम इसे वीडीएम-एसएल में इस टाइप परिभाषित कर सकते हैं:


  state Register of
  state Register of
  someStateRegister : nat
  someStateRegister : nat
  end
  end


इसके अतिरिक्त VDM++ में इसे इस टाइप परिभाषित किया जाएगा:
इसके अतिरिक्त वीडीएम++ में इसे इस टाइप परिभाषित किया जाएगा:


  instance variables
  instance variables
  someStateRegister : nat
  someStateRegister : nat


इस वेरिएबल में मान लोड करने के लिए एक ऑपरेशन को इस टाइप निर्दिष्ट किया जा सकता है:
इस वेरिएबल में मान लोड करने के लिए ऑपरेशन को इस टाइप निर्दिष्ट किया जा सकता है:


  LOAD(i:nat)
  LOAD(i:nat)
Line 288: Line 288:
  post someStateRegister = i
  post someStateRegister = i


बाहरी खंड (<code>ext</code>) निर्दिष्ट करता है कि ऑपरेशन द्वारा राज्य के किन भागो तक पहुँचा जा सकता है; <code>rd</code> केवल-पठन पहुंच का संकेत और <code>wr</code> पढ़ने/लिखने की पहुंच।
बाहरी खंड (<code>ext</code>) निर्दिष्ट करता है कि ऑपरेशन द्वारा स्टेट के किन भागो तक पहुँचा जा सकता है; <code>rd</code> केवल-पठन पहुंच का संकेत और <code>wr</code> पढ़ने/लिखने की पहुंच।


कभी-कभी किसी राज्य को संशोधित करने से पहले उसके मूल्य का उल्लेख करना महत्वपूर्ण होता है; उदाहरण के लिए, वैरिएबल में मान जोड़ने के लिए एक ऑपरेशन को इस टाइप निर्दिष्ट किया जा सकता है:
कभी-कभी किसी स्टेट को संशोधित करने से पहले उसके मूल्य का उल्लेख करना महत्वपूर्ण होता है; उदाहरण के लिए, वैरिएबल में मान जोड़ने के लिए ऑपरेशन को इस टाइप निर्दिष्ट किया जा सकता है:


  ADD(i:nat)
  ADD(i:nat)
Line 296: Line 296:
  post someStateRegister = someStateRegister~ + i
  post someStateRegister = someStateRegister~ + i


जहां <code>~</code> पोस्टकंडिशन में स्टेट वेरिएबल पर प्रतीक ऑपरेशन के निष्पादन से पहले स्टेट वेरिएबल का मान इंगित करता है।
जहां <code>~</code> पोस्टकंडिशन में स्टेट वेरिएबल पर प्रतीक ऑपरेशन के निष्पादन से पहले स्टेट वेरिएबल का मान निरुपित करता है।


==उदाहरण==
==उदाहरण==
{{Further|Meta-IV (specification language)}}
{{Further|मेटा-IV (विनिर्देश लैंग्वेज) }}


===अधिकतम फ़ंक्शन===
===अधिकतम फ़ंक्शन===
यह एक अंतर्निहित फ़ंक्शन डिफ्निसन का एक उदाहरण है। फ़ंक्शन सकारात्मक पूर्णांकों के सेट से सबसे बड़ा तत्व लौटाता है:
यह अंतर्निहित फ़ंक्शन डिफ्निसन का उदाहरण है। फ़ंक्शन धनात्मक पूर्णांकों के सेट से सबसे बड़ा कॉम्पोनेन्ट लौटाता है:


  max(s:set of nat)r:nat
  max(s:set of nat)r:nat
  pre card s > 0
  pre card s > 0
  post r in set s and
  post r in set s and
      forall r' in set s & r' <= r
  forall r' in set s & r' <= r


पोस्टकंडिशन परिणाम को प्राप्त करने के लिए एल्गोरिदम को परिभाषित करने के अतिरिक्त उसे चित्रित करता है। पूर्व नियम की आवश्यकता है क्योंकि सेट खाली होने पर कोई भी फ़ंक्शन सेट s में r वापस नहीं कर सकता है।
पोस्टकंडिशन परिणाम को प्राप्त करने के लिए एल्गोरिदम को परिभाषित करने के अतिरिक्त उसे चित्रित करता है। पूर्व नियम की आवश्यकता है क्योंकि सेट रिक्त होने पर कोई भी फ़ंक्शन सेट s में r वापस नहीं कर सकता है।


===प्राकृतिक संख्या गुणन===
===प्राकृतिक संख्या गुणन===
Line 316: Line 316:
  post r = i*j
  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>:
प्रमाण दायित्व प्रयुक्त करना <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) ==
  multp(i,j) ==
Line 322: Line 322:
   then 0
   then 0
   else if is-even(i)
   else if is-even(i)
      then 2*multp(i/2,j)
  then 2*multp(i/2,j)
      else j+multp(i-1,j)
  else j+multp(i-1,j)


तब प्रमाण दायित्व बन जाता है:
तब प्रमाण दायित्व बन जाता है:
Line 330: Line 330:


इसे इसके द्वारा सही दिखाया जा सकता है:
इसे इसके द्वारा सही दिखाया जा सकता है:
# यह सिद्ध करना कि पुनरावृत्ति समाप्त हो जाती है (इसके बदले में यह सिद्ध करना आवश्यक है कि संख्याएँ प्रत्येक चरण में छोटी हो जाती हैं)
# यह सिद्ध करना कि पुनरावृत्ति समाप्त हो जाती है (इसके बदले में यह सिद्ध करना आवश्यक है कि संख्याएँ प्रत्येक फेज में छोटी हो जाती हैं)
# [[गणितीय प्रेरण]]
# [[गणितीय प्रेरण]]


===कतार सार डेटा प्रकार===
===पंक्ति सार डेटा टाइप ===
यह एक प्रसिद्ध डेटा संरचना के राज्य-आधारित मॉडल में अंतर्निहित ऑपरेशन स्पेसिफिकेशन के उपयोग को दर्शाने वाला एक शास्त्रीय उदाहरण है। कतार को एक टाइप के तत्वों से बने अनुक्रम के रूप में तैयार किया गया है <code>Qelt</code>. प्रतिनिधित्व है <code>Qelt</code> सारहीन है और इसलिए इसे टोकन टाइप के रूप में परिभाषित किया गया है।
यह प्रसिद्ध डेटा संरचना के स्टेट -बेस्ड मॉडल में अंतर्निहित ऑपरेशन स्पेसिफिकेशन के उपयोग को दर्शाने वाला मौलिक उदाहरण है। पंक्ति को टाइप के कॉम्पोनेन्टं से बने अनुक्रम के रूप में तैयार किया गया है <code>Qelt</code>. प्रतिनिधित्व है <code>Qelt</code> सारहीन है और इसलिए इसे टोकन टाइप के रूप में परिभाषित किया गया है।


  types
  types
Line 342: Line 342:


  state TheQueue of
  state TheQueue of
  q : Queue
  q : Queue
  end
  end


Line 360: Line 360:
  post r <=> (len q = 0)
  post r <=> (len q = 0)


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




Line 370: Line 370:


  AccData :: owner : CustNum
  AccData :: owner : CustNum
            balance : Balance
  balance : Balance


  state Bank of
  state Bank of
  accountMap : map AccNum to AccData
  accountMap : map AccNum to AccData
  overdraftMap : map CustNum to Overdraft
  overdraftMap : map CustNum to Overdraft
  inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and
  inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and
                                        a.balance >= -overdraftMap(a.owner)
  a.balance >= -overdraftMap(a.owner)


संचालन के साथ:
संचालन के साथ:
NEWC एक नया ग्राहक नंबर आवंटित करता है:
 
एनईडब्ल्यूसी नया ग्राहक नंबर आवंटित करता है:


  operations
  operations
Line 386: Line 387:
  post r not in set dom ~overdraftMap and overdraftMap = ~overdraftMap ++ { r |-> od};
  post r not in set dom ~overdraftMap and overdraftMap = ~overdraftMap ++ { r |-> od};


NEWAC एक नया खाता नंबर आवंटित करता है और शेष राशि को शून्य पर सेट करता है:
एनईडब्ल्यूएसी नया खाता नंबर आवंटित करता है और शेष राशि को शून्य पर सेट करता है:


  NEWAC(cu : CustNum)r : AccNum
  NEWAC(cu : CustNum)r : AccNum
  ext wr accountMap : map AccNum to AccData
  ext wr accountMap : map AccNum to AccData
    rd overdraftMap map CustNum to Overdraft
  rd overdraftMap map CustNum to Overdraft
  pre cu in set dom overdraftMap
  pre cu in set dom overdraftMap
  post r not in set dom accountMap~ and accountMap = accountMap~ ++ {r|-> mk_AccData(cu,0)}
  post r not in set dom accountMap~ and accountMap = accountMap~ ++ {r|-> mk_AccData(cu,0)}


ACINF एक ग्राहक के सभी खातों की सभी शेष राशि, शेष राशि के खाता संख्या के मानचित्र के रूप में लौटाता है:
एसीआईएनएफ ग्राहक के सभी खातों की सभी शेष राशि, शेष राशि के खाता संख्या के मानचित्र के रूप में लौटाता है:


  ACINF(cu : CustNum)r : map AccNum to Balance
  ACINF(cu : CustNum)r : map AccNum to Balance
Line 401: Line 402:


==उपकरण समर्थन==
==उपकरण समर्थन==
कई अलग-अलग उपकरण VDM का समर्थन करते हैं:
कई अलग-अलग उपकरण वीडीएम का समर्थन करते हैं:
* [http://www.vdmtools.jp/en VDMTools] VDM और VDM++ के लिए अग्रणी व्यावसायिक उपकरण था, जिसका स्वामित्व, विपणन, रखरखाव और डेवलपमेंट [http://www.csk.com CSK Systems] द्वारा किया गया था, जो डेनिश कंपनी IFAD द्वारा विकसित पुराने संस्करणों पर आधारित था। [http://www.vdmtools.jp/en/modules/tinyd2/index.php?id=2 मैनुअल] और एक व्यावहारिक [http://www.vdmportal.org/twiki/pub/Main/WebHome/tutorial1.pdf ट्यूटोरियल] उपलब्ध हैं। टूल के पूर्ण संस्करण के लिए सभी लाइसेंस निःशुल्क उपलब्ध हैं। पूर्ण संस्करण में जावा और C++ के लिए स्वचालित कोड जनरेशन, डायनेमिक लिंक लाइब्रेरी और CORBA समर्थन सम्मिलित है।
* [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 vdm-mode] वीडीएम-एसएल, VDM++ और VDM-RT का उपयोग करके VDM स्पेसिफिकेशन लिखने के लिए Emacs पैकेजों का एक संग्रह है। यह सिंटैक्स हाइलाइटिंग और संपादन, ऑन-द-फ्लाई सिंटैक्स चेकिंग, टेम्पलेट पूर्णता और दुभाषिया समर्थन का समर्थन करता है।
* [https://github.com/peterwvj/vdm-mode वीडीएम-mode] वीडीएम-एसएल, वीडीएम++ और वीडीएम-आरटी का उपयोग करके वीडीएम स्पेसिफिकेशन लिखने के लिए इमैक्स पैकेजों का स्टोर है। यह सिंटैक्स हाइलाइटिंग और संपादन, ऑन-द-फ्लाई सिंटैक्स चेकिंग, टेम्पलेट पूर्णता और इन्टेरोपेराबल समर्थन का समर्थन करता है।
* [http://www.adelard.com/web/hnav/services/SoftwareTools/SpecBox/index.html SpecBox]: एडेलार्ड से सिंटैक्स जांच, कुछ सरल सिमेंटिक जांच और एक [[LaTeX]] फ़ाइल का निर्माण प्रदान किया जाता है, जो विशिष्टताओं को गणितीय नोटेशन में मुद्रित करने में सक्षम बनाता है। यह उपकरण निःशुल्क उपलब्ध है लेकिन इसका रखरखाव नहीं किया जा रहा है।
* [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/ मैक्रोज़] ऑनलाइन उपलब्ध हैं।
* आईएसओ मानक लैंग्वेज के गणितीय वाक्यविन्यास में वीडीएम मॉडल की प्रस्तुति का समर्थन करने के लिए LaTeX और LaTeX2e मैक्रोज़ उपलब्ध हैं। इन्हें यूके में राष्ट्रीय भौतिक प्रयोगशाला द्वारा विकसित और रखरखाव किया गया है। [http://ftp.npl.co.uk/pub/latex/macros/vdm-sl/README डॉक्यूमेंटीकरण] और [http://ftp.npl.co.uk/pub/latex/macros/vdm-sl/ मैक्रोज़] ऑनलाइन उपलब्ध हैं।


==औद्योगिक अनुभव==
==औद्योगिक अनुभव==
वीडीएम को विभिन्न एप्लिकेशन डोमेन में व्यापक रूप से लागू किया गया है। इनमें से सबसे प्रसिद्ध अनुप्रयोग हैं:
वीडीएम को विभिन्न एप्लिकेशन डोमेन में व्यापक रूप से प्रयुक्त किया गया है। इनमें से सबसे प्रसिद्ध अनुप्रयोग हैं:
* Ada (प्रोग्रामिंग लैंग्वेज ) और [[CHILL]] [[ संकलक ]]: पहला यूरोपीय मान्य Ada कंपाइलर VDM का उपयोग करके 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> इसी टाइप CHILL और [[Modula-2]] के शब्दार्थ को VDM का उपयोग करके उनके मानकों में वर्णित किया गया था।
* 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]] के शब्दार्थ को वीडीएम का उपयोग करके उनके मानकों में वर्णित किया गया था।
* कॉनफॉर्म: ब्रिटिश एयरोस्पेस में एक प्रयोग जिसमें एक विश्वसनीय गेटवे के पारंपरिक डेवलपमेंट की तुलना वीडीएम का उपयोग करके किए गए डेवलपमेंट से की गई है।
* कॉनफॉर्म: ब्रिटिश एयरोस्पेस में प्रयोग जिसमें विश्वसनीय गेटवे के पारंपरिक डेवलपमेंट की तुलना वीडीएम का उपयोग करके किए गए डेवलपमेंट से की गई है।
* धूल-विशेषज्ञ: सुरक्षा संबंधी अनुप्रयोग के लिए [[यूके]] में एडेलार्ड द्वारा चलाया गया एक प्रोजेक्ट जो यह निर्धारित करता है कि औद्योगिक संयंत्रों के लेआउट में सुरक्षा उपयुक्त है।
* धूल-विशेषज्ञ: सुरक्षा संबंधी अनुप्रयोग के लिए [[यूके]] में एडेलार्ड द्वारा चलाया गया प्रोजेक्ट जो यह निर्धारित करता है कि औद्योगिक संयंत्रों के लेआउट में सुरक्षा उपयुक्त है।
* VDMTools का विकास: VDMTools टूल सूट के अधिकांश घटक स्वयं VDM का उपयोग करके विकसित किए गए हैं। यह डेवलपमेंट [[डेनमार्क]] में [http://www.ifad.dk/ IFAD] और [[जापान]] में [[सीएसके होल्डिंग्स कॉर्पोरेशन]] में किया गया है।<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>
* वीडीएमटूल्स का विकास: वीडीएमटूल्स टूल सूट के अधिकांश घटक स्वयं वीडीएम का उपयोग करके विकसित किए गए हैं। यह डेवलपमेंट [[डेनमार्क]] में [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 439: 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>. डेटा संशोधन की शुद्धता पर्याप्तता सिद्ध करने पर निर्भर करती है, यानी।
डेटा पुनरीक्षण (चरणबद्ध शोधन) में स्पेसिफिकेशन में उपयोग किए गए एब्सट्रेक्ट डेटा टाइप का अधिक ठोस प्रतिनिधित्व खोजना सम्मिलित है। कार्यान्वयन तक पहुँचने से पहले कई फेज हो सकते हैं। एब्सट्रेक्ट डेटा प्रतिनिधित्व के लिए प्रत्येक पुनरीक्षण फेज <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)
  forall a:ABS_REP & exists r:NEW_REP & a = retr(r)


चूँकि डेटा प्रतिनिधित्व बदल गया है, संचालन और कार्यों को अद्यतन करना आवश्यक है जिससे वे काम करते रहें <code>NEW_REP</code>. नए प्रतिनिधित्व पर किसी भी डेटा टाइप के इनवेरिएंट (कंप्यूटर विज्ञान) को संरक्षित करने के लिए नए संचालन और कार्यों को दिखाया जाना चाहिए। यह सिद्ध करने के लिए कि नए संचालन और फ़ंक्शन मॉडल मूल स्पेसिफिकेशन में पाए गए हैं, दो प्रमाण दायित्वों का निर्वहन करना आवश्यक है:
चूँकि डेटा प्रतिनिधित्व बदल गया है, संचालन और कार्यों को अद्यतन करना आवश्यक है जिससे वे कार्य करते रहें जिससे <code>NEW_REP</code>. नए प्रतिनिधित्व पर किसी भी डेटा टाइप के इनवेरिएंट (कंप्यूटर विज्ञान) को संरक्षित करने के लिए नए संचालन और कार्यों को दिखाया जाना चाहिए। यह सिद्ध करने के लिए कि नए संचालन और फ़ंक्शन मॉडल मूल स्पेसिफिकेशन में पाए गए हैं, दो प्रमाण दायित्वों का निर्वहन करना आवश्यक है:


*डोमेन नियम:
*डोमेन नियम:
Line 452: Line 453:
  forall ~r,r:NEW_REP & pre-OPA(retr(~r)) and post-OPR(~r,r) => post-OPA(retr(~r,), retr(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
  types
Line 468: Line 468:


  state AWCCS of
  state AWCCS of
  pres: Workers
  pres: Workers
  end
  end


Line 490: Line 490:
  ext rd pres : Workers
  ext rd pres : Workers
  post r <=> p in set pres~
  post r <=> p in set pres~
चूँकि अधिकांश प्रोग्रामिंग लैंग्वेज ओं में एक सेट (अक्सर एक सरणी के रूप में) की तुलना में एक अवधारणा होती है, स्पेसिफिकेशन से पहला कदम अनुक्रम के संदर्भ में डेटा का प्रतिनिधित्व करना है। इन अनुक्रमों को पुनरावृत्ति की अनुमति नहीं देनी चाहिए, क्योंकि हम नहीं चाहते कि एक ही कार्यकर्ता दो बार दिखाई दे, इसलिए हमें नए डेटा टाइप में एक इनवेरिएंट (कंप्यूटर विज्ञान) जोड़ना होगा। इस मामले में, ऑर्डर देना महत्वपूर्ण नहीं है, इसलिए <code>[a,b]</code> वैसा ही है जैसा कि <code>[b,a]</code>.
चूँकि अधिकांश प्रोग्रामिंग लैंग्वेज ओं में सेट ( अधिकांशतः सरणी के रूप में) की तुलना में अवधारणा होती है, स्पेसिफिकेशन से पहला कदम अनुक्रम के कॉन्टेक्स्ट में डेटा का प्रतिनिधित्व करना है। इन अनुक्रमों को पुनरावृत्ति की अनुमति नहीं देनी चाहिए, क्योंकि हम नहीं चाहते कि ही कार्यकर्ता दो बार दिखाई दे, इसलिए हमें नए डेटा टाइप में इनवेरिएंट (कंप्यूटर विज्ञान) जोड़ना होगा। इस स्थिति में, ऑर्डर देना महत्वपूर्ण नहीं है, इसलिए <code>[a,b]</code> वैसा ही है जैसा कि <code>[b,a]</code>.के समान है।


वियना डेवलपमेंट पद्धति मॉडल-आधारित प्रणालियों के लिए मूल्यवान है। यदि व्यवस्था समय आधारित है तो यह उचित नहीं है। ऐसे स्थितियों के लिए, [[संचार प्रणालियों की गणना]] (सीसीएस) अधिक उपयोगी है।
वियना डेवलपमेंट पद्धति मॉडल-बेस्ड सिस्टम्स के लिए मूल्यवान है। यदि व्यवस्था समय बेस्ड है तो यह उचित नहीं है। ऐसे स्थितियों के लिए, [[संचार प्रणालियों की गणना|कम्युनिकेटिंग सिस्टम्स की गणना]] (सीसीएस) अधिक उपयोगी है।


==यह भी देखें==
==यह भी देखें==
* औपचारिक तरीके
* फॉर्मल मेथड्स
* [[औपचारिक विशिष्टता]]
* [[औपचारिक विशिष्टता|फॉर्मल]] [[Z विशिष्टता भाषा|स्पेसिफिकेशन]]
* [[पिजिन कोड]]
* [[पिजिन कोड]]
* [[विधेय तर्क|विधेय लॉजिक]]  
* [[विधेय तर्क|विधेय लॉजिक]]  
* [[प्रस्तावात्मक कलन]]
* [[प्रस्तावात्मक कलन|प्रस्तावात्मक एल्गोरिथ्म]]  
* [[Z विशिष्टता भाषा|Z विशिष्टता लैंग्वेज]] , वीडीएम-एसएल का मुख्य विकल्प (तुलना करें)
* [[Z विशिष्टता भाषा|जेड स्पेसिफिकेशन लैंग्वेज]] , वीडीएम-एसएल का मुख्य विकल्प (तुलना करें)
* [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 }} (सीएमएल), [[प्रोग्रामिंग के एकीकृत सिद्धांत]]ों पर आधारित संचार अनुक्रमिक प्रक्रियाओं के साथ वीडीएम-एसएल का एक संयोजन, सिस्टम ऑफ मॉडलिंग (एसओएस) के लिए विकसित किया गया है।
* [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 509: 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 VDM'', [[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
* [[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 वीडीएम-एसएल Reference Guide'', [[Pitman (publisher)|Pitman]] 1991. {{ISBN|0-273-03151-1}}
* J. Dawes, ''The वीडीएम-एसएल Reference Guide'', [[Pitman (publisher)|Pitman]] 1991. {{ISBN|0-273-03151-1}}
Line 515: Line 515:
* [[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 VDM: a Practitioner's Guide''. [[Springer Verlag]] Formal Approaches to Computing and Information Technology (FACIT), 1994. {{ISBN|3-540-19813-X}} .
* 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 VDM and VDM++ (archived copy at archive.org)]
* [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)]
{{Use dmy dates|date=September 2019}}
[[Category: औपचारिक तरीके]] [[Category: औपचारिक विशिष्टता भाषाएँ]]


[[Category: Machine Translated Page]]
[[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 UserId

UserIdमानों के सभी परिमित सेटों से बना टाइप UGroup को परिभाषित करता है। विभिन्न ऑपरेटरों को उनके संघ, प्रतिच्छेदन, उचित और गैर-सख्त सबसेट संबंधों का निर्धारण आदि के लिए सेट पर परिभाषित किया गया है।

सेट पर मुख्य ऑपरेटर (s, s1, s2 सेट हैं)
{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].

अनुक्रमों पर मुख्य संचालक (s, s1,s2 अनुक्रम हैं)
[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

इसे इसके द्वारा सही दिखाया जा सकता है:

  1. यह सिद्ध करना कि पुनरावृत्ति समाप्त हो जाती है (इसके बदले में यह सिद्ध करना आवश्यक है कि संख्याएँ प्रत्येक फेज में छोटी हो जाती हैं)
  2. गणितीय प्रेरण

पंक्ति सार डेटा टाइप

यह प्रसिद्ध डेटा संरचना के स्टेट -बेस्ड मॉडल में अंतर्निहित ऑपरेशन स्पेसिफिकेशन के उपयोग को दर्शाने वाला मौलिक उदाहरण है। पंक्ति को टाइप के कॉम्पोनेन्टं से बने अनुक्रम के रूप में तैयार किया गया है 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].के समान है।

वियना डेवलपमेंट पद्धति मॉडल-बेस्ड सिस्टम्स के लिए मूल्यवान है। यदि व्यवस्था समय बेस्ड है तो यह उचित नहीं है। ऐसे स्थितियों के लिए, कम्युनिकेटिंग सिस्टम्स की गणना (सीसीएस) अधिक उपयोगी है।

यह भी देखें

अग्रिम पठन

  • 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 .


कॉन्टेक्स्ट

  1. 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.
  2. The double plus is adopted from the C++ objected oriented programming language based on C.
  3. Bjørner&Jones 1978, Introduction, p.ix
  4. Introductory remarks by Cliff B. Jones (editor) in Bekič 1984, p.vii
  5. Bjørner&Jones 1978, Introduction, p.xi
  6. Bjørner&Jones 1978, p.24.
  7. See the article on persistence for its use within computer science.
  8. 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.
  9. 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
  10. Modelling Systems: Practical Tools and Techniques in Software Engineering
  11. Validated Designs for Object-oriented Systems


बाहरी संबंध