वियना विकास विधि

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

फिलोसॉफी

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

इतिहास

वीडीएम-एसएल की उत्पत्ति वियना में आईबीएम प्रयोगशाला में हुई जहां लैंग्वेज के पहले संस्करण को वियना डेफिनिशन लैंग्वेज (वीडीएल) कहा जाता था। वीडीएल का उपयोग अनिवार्य रूप से वीडीएम - मेटा-IV के विपरीत ऑपरेशनल सेमांटिक्स डिस्क्रिप्शन देने के लिए किया गया था, जो डिनोटैस्नल सेमांटिक्स प्रदान करता था।

<ब्लॉककोट>

«1972 के अंत में वियना समूह ने फिर से एक लैंग्वेज डिफ्निसन से एक कम्पाइलर को व्यवस्थित रूप से विकसित करने की समस्या पर अपना ध्यान केंद्रित किया। अपनाए गए समग्र दृष्टिकोण को वियना डेवलपमेंट मेथड कहा गया है ... वास्तव में अपनाई गई मेटा-लैंग्वेज (मेटा-IV) का उपयोग पीएल/1 के प्रमुख भागो को परिभाषित करने के लिए किया जाता है (जैसा कि ईसीएमए 74 में दिया गया है - रौचक बात यह है कि एक एब्सट्रेक्ट इंटरप्रेटर के रूप में लिखा गया एक औपचारिक मानक डॉक्यूमेंट ) BEKIČ 74 में।

</ब्लॉककोट>

मेटा-IV के बीच कोई संबंध नहीं है, और शोर्रे की मेटा II लैंग्वेज , या इसकी उत्तराधिकारी ट्री मेटा ; ये औपचारिक समस्या विवरण के लिए उपयुक्त होने के अतिरिक्त कम्पाइलर -कम्पाइलर सिस्टम थे।

इसलिए मेटा-IV का उपयोग पीएल/आई प्रोग्रामिंग लैंग्वेज के प्रमुख भागों को परिभाषित करने के लिए किया गया था। मेटा-IV और वीडीएम-एसएल का उपयोग करके पूर्वव्यापी रूप से वर्णित या आंशिक रूप से वर्णित अन्य प्रोग्रामिंग लैंग्वेज ओं में बेसिक प्रोग्रामिंग लैंग्वेज , फोरट्रान, एपीएल प्रोग्रामिंग लैंग्वेज , ALGOL 60, एडा प्रोग्रामिंग लैंग्वेज और पास्कल प्रोग्रामिंग लैंग्वेज सम्मिलित हैं। मेटा-IV कई टाइप में विकसित हुआ, जिन्हें समान्यत: डेनिश, अंग्रेजी और आयरिश स्कूलों के रूप में वर्णित किया गया है।

इंग्लिश स्कूल वीडीएम के उन विधियों पर क्लिफ जोन्स (कंप्यूटर वैज्ञानिक) के काम से प्राप्त हुआ है जो विशेष रूप से लैंग्वेज डिफ्निसन और कंपाइलर डिजाइन से संबंधित नहीं हैं (जोन्स 1980, 1990)। यह निरंतर मॉडलिंग पर जोर देता है आधार टाइप के समृद्ध संग्रह से निर्मित डेटा टाइप के उपयोग के माध्यम से बताएं। कार्यक्षमता को समान्यत: उन ऑपरेशनों के माध्यम से वर्णित किया जाता है जिनके स्टेट पर दुष्प्रभाव हो सकते हैं और जो अधिकतर पूर्व नियम और पोस्टकंडिशन का उपयोग करके अंतर्निहित रूप से निर्दिष्ट होते हैं। डेनिश स्कूल (डाइन्स ब्योर्नर या ब्योर्नर एट अल. 1982) ने अधिक सीमा तक उपयोग किए जाने वाले स्पष्ट परिचालन स्पेसिफिकेशन के साथ रचनात्मक दृष्टिकोण पर जोर दिया है। डेनिश स्कूल में काम करने से पहला यूरोपीय मान्य एडा प्रोग्रामिंग लैंग्वेज कंपाइलर तैयार हुआ।

लैंग्वेज के लिए मानकीकरण मानक के लिए एक अंतर्राष्ट्रीय संगठन 1996 में जारी किया गया था (आईएसओ, 1996)।

वीडीएम सुविधाएँ

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

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

मूल प्रकार: संख्यात्मक, वर्ण, टोकन और कोटे प्रकार

वीडीएम-एसएल में बेसिक टाइप के मॉडलिंग नंबर और अक्षर इस टाइप सम्मिलित हैं:

बेसिक टाइप

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}	Set enumeration: the set of elements a, b and c
{x | x:T & P(x)}	Set comprehension: the set of x from type T such that P(x)
{i, ..., j}	The set of integers in the range i to j
e in set s	e is an element of set s
e not in set s	e is not an element of set s
s1 union s2	Union of sets s1 and s2
s1 inter s2	Intersection of sets s1 and s2
s1 \ s2	Set difference of sets s1 and s2
dunion s	Distributed union of set of sets s
s1 psubset s2	s1 is a (proper) subset of s2
s1 subset s2	s1 is a (weak) subset of s2
card s	The cardinality of set 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. फिर से, मैपिंग में अनुक्रमण, मैपिंग को मर्ज करने, उप-मैपिंग को निकालने के लिए ओवरराइटिंग के लिए ऑपरेटरों को मैपिंग पर परिभाषित किया जाता है।

Main operators on mappings

{a |-> r, b |-> s}	Mapping enumeration: a maps to r, b maps to s
{x |-> f(x) | x:T & P(x)}	Mapping comprehension: x maps to f(x) for all x for type T such that P(x)
dom m	The domain of m
rng m	The range of m
m(x)	m applied to x
m1 munion m2	Union of mappings m1 and m2 (m1, m2 must be consistent where they overlap)
m1 ++ m2	m1 overwritten by m2

संरचना

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

वीडीएम-एसएल में संरचना

वीडीएम-एसएल के लिए आईएसओ मानक में एक सूचनात्मक अनुबंध है जिसमें विभिन्न संरचना सिद्धांत सम्मिलित हैं। ये सभी मॉड्यूल के साथ पारंपरिक जानकारी छिपाने के सिद्धांतों का पालन करते हैं और इन्हें इस टाइप समझाया जा सकता है:

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

VDM++ में संरचना

VDM++ में कक्षाओं और एकाधिक वंशानुक्रम का उपयोग करके संरचना की जाती है। प्रमुख अवधारणाएँ हैं:

• क्लास: प्रत्येक क्लास वाक्यात्मक रूप से कीवर्ड से प्रारंभ होती है class इसके बाद वर्ग का नाम आता है। कक्षा के अंत में कीवर्ड end इसके बाद फिर से कक्षा का नाम लिखा जाता है।
• वंशानुक्रम: यदि किसी वर्ग को अन्य वर्गों से संरचनाएं विरासत में मिलती हैं तो वर्ग शीर्षक में वर्ग नाम के बाद कीवर्ड का उपयोग किया जा सकता है is subclass of उसके बाद सुपरक्लास के नामों की अल्पविराम से अलग की गई सूची।
• एक्सेस संशोधक: VDM++ में जानकारी छिपाना उसी तरह से किया जाता है जैसे अधिकांश ऑब्जेक्ट ओरिएंटेड लैंग्वेज ओं में एक्सेस संशोधक का उपयोग करके किया जाता है। VDM++ में डिफ्निसन एँ डिफ़ॉल्ट रूप से निजी होती हैं किंतु सभी डिफ्निसन ओं के सामने एक्सेस संशोधक कीवर्ड 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

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

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

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

उदाहरण

Further information: मेटा-IV (विनिर्देश लैंग्वेज)

अधिकतम फ़ंक्शन

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

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

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

प्राकृतिक संख्या गुणन

multp(i,j:nat)r:nat
pre true
post r = i*j

प्रमाण दायित्व प्रयुक्त करना 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}

उपकरण समर्थन

कई अलग-अलग उपकरण VDM का समर्थन करते हैं:

• VDMTools VDM और VDM++ के लिए अग्रणी व्यावसायिक उपकरण था, जिसका स्वामित्व, विपणन, रखरखाव और डेवलपमेंट CSK Systems द्वारा किया गया था, जो डेनिश कंपनी IFAD द्वारा विकसित पुराने संस्करणों पर आधारित था। मैनुअल और एक व्यावहारिक ट्यूटोरियल उपलब्ध हैं। टूल के पूर्ण संस्करण के लिए सभी लाइसेंस निःशुल्क उपलब्ध हैं। पूर्ण संस्करण में जावा और C++ के लिए स्वचालित कोड जनरेशन, डायनेमिक लिंक लाइब्रेरी और CORBA समर्थन सम्मिलित है।
• ओवरवेरिएबल एक समुदाय-आधारित ओपन सोर्स पहल है जिसका उद्देश्य सभी वीडीएम बोलियों (वीडीएम-एसएल, वीडीएम++ और वीडीएम-आरटी) के लिए मूल रूप से एक्लिप्स प्लेटफॉर्म के शीर्ष पर किंतु बाद में विजुअल स्टूडियो कोड प्लेटफॉर्म के शीर्ष पर स्वतंत्र रूप से उपलब्ध टूल समर्थन प्रदान करना है। इसका उद्देश्य इंटरऑपरेबल टूल के लिए एक ढांचा विकसित करना है जो औद्योगिक अनुप्रयोग, अनुसंधान और शिक्षा के लिए उपयोगी होगा।
• vdm-mode वीडीएम-एसएल, VDM++ और VDM-RT का उपयोग करके VDM स्पेसिफिकेशन लिखने के लिए Emacs पैकेजों का एक संग्रह है। यह सिंटैक्स हाइलाइटिंग और संपादन, ऑन-द-फ्लाई सिंटैक्स चेकिंग, टेम्पलेट पूर्णता और इन्टेरोपेराबल समर्थन का समर्थन करता है।
• SpecBox: एडेलार्ड से सिंटैक्स जांच, कुछ सरल सिमेंटिक जांच और एक LaTeX फ़ाइल का निर्माण प्रदान किया जाता है, जो विशिष्टताओं को गणितीय नोटेशन में मुद्रित करने में सक्षम बनाता है। यह उपकरण निःशुल्क उपलब्ध है किंतु इसका रखरखाव नहीं किया जा रहा है।
• आईएसओ मानक लैंग्वेज के गणितीय वाक्यविन्यास में वीडीएम मॉडल की प्रस्तुति का समर्थन करने के लिए LaTeX और LaTeX2e मैक्रोज़ उपलब्ध हैं। इन्हें यूके में राष्ट्रीय भौतिक प्रयोगशाला द्वारा विकसित और रखरखाव किया गया है। डॉक्यूमेंट ीकरण और मैक्रोज़ ऑनलाइन उपलब्ध हैं।

औद्योगिक अनुभव

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

• Ada (प्रोग्रामिंग लैंग्वेज ) और CHILL कम्पाइलर: पहला यूरोपीय मान्य Ada कंपाइलर VDM का उपयोग करके Dansk डेटामैटिक सेंटर द्वारा विकसित किया गया था। इसी टाइप CHILL और Modula-2 के शब्दार्थ को VDM का उपयोग करके उनके मानकों में वर्णित किया गया था।
• कॉनफॉर्म: ब्रिटिश एयरोस्पेस में एक प्रयोग जिसमें एक विश्वसनीय गेटवे के पारंपरिक डेवलपमेंट की तुलना वीडीएम का उपयोग करके किए गए डेवलपमेंट से की गई है।
• धूल-विशेषज्ञ: सुरक्षा संबंधी अनुप्रयोग के लिए यूके में एडेलार्ड द्वारा चलाया गया एक प्रोजेक्ट जो यह निर्धारित करता है कि औद्योगिक संयंत्रों के लेआउट में सुरक्षा उपयुक्त है।
• VDMTools का विकास: VDMTools टूल सूट के अधिकांश घटक स्वयं VDM का उपयोग करके विकसित किए गए हैं। यह डेवलपमेंट डेनमार्क में IFAD और जापान में सीएसके होल्डिंग्स कॉर्पोरेशन में किया गया है।
• ट्रेडवन: जापानी स्टॉक एक्सचेंज के लिए सीएसके सिस्टम द्वारा विकसित ट्रेडवन बैक-ऑफिस सिस्टम के कुछ प्रमुख घटक वीडीएम का उपयोग करके विकसित किए गए थे। पारंपरिक रूप से विकसित कोड बनाम वीडीएम-विकसित घटकों की डेवलपर उत्पादकता और दोष घनत्व के लिए तुलनात्मक माप उपस्थित हैं।
• फेलिका नेटवर्क्स ने सेलुलर टेलीफोन अनुप्रयोगों के लिए एक एकीकृत सर्किट के लिए एक ऑपरेटिंग सिस्टम के डेवलपमेंट की सूचना दी है।

रेफिनमेन्ट

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

डेटा रीफिकेशन एब्सट्रेक्ट डेटा टाइप को अधिक ठोस डेटा संरचनाओं में विकसित करता है, जबकि ऑपरेशन अपघटन संचालन और कार्यों के (अमूर्त) अंतर्निहित विनिर्देशों को एल्गोरिथ्म मेथड में विकसित करता है जिन्हें सीधे पसंद की कंप्यूटर लैंग्वेज में प्रयुक्त किया जा सकता है।

${\begin{array}{|rcl|}{\textbf {Specification}}&&{\textbf {Implementation}}\\\hline {\text{Abstract data type}}&\xrightarrow {\text{Data reification}} &{\text{Data structure}}\\{\text{Operations}}&{\xrightarrow[{\text{Operation decomposition}}]{}}&{\text{Algorithms}}\end{array}}$

डेटा रीफिकेशन

डेटा पुनरीक्षण (चरणबद्ध शोधन) में एक स्पेसिफिकेशन में उपयोग किए गए एब्सट्रेक्ट डेटा टाइप का अधिक ठोस प्रतिनिधित्व खोजना सम्मिलित है। कार्यान्वयन तक पहुँचने से पहले कई चरण हो सकते हैं। एक एब्सट्रेक्ट डेटा प्रतिनिधित्व के लिए प्रत्येक पुनरीक्षण चरण 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].के समान है।

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

यह भी देखें

• औपचारिक विधि
• औपचारिक विशिष्टता
• पिजिन कोड
• विधेय लॉजिक
• प्रस्तावात्मक एल्गोरिथ्म
• Z विशिष्टता लैंग्वेज , वीडीएम-एसएल का मुख्य विकल्प (तुलना करें)
• कम्पास मॉडलिंग लैंग्वेज Archived 19 February 2020 at the Wayback Machine (सीएमएल), प्रोग्रामिंग के एकीकृत सिद्धांत पर आधारित संचार अनुक्रमिक प्रक्रियाओं के साथ वीडीएम-एसएल का एक संयोजन, सिस्टम ऑफ मॉडलिंग (एसओएस) के लिए विकसित किया गया है।

अग्रिम पठन

• Bjørner, Dines; Cliff B. Jones (1978). The Vienna Development Method: The Meta-Language, Lecture Notes in Computer Science 61. Berlin, Heidelberg, New York: Springer. ISBN 978-0-387-08766-5.
• O'Regan, Gerard (2006). Mathematical Approaches to Software Quality. London: Springer. ISBN 978-1-84628-242-3.
• Cliff B. Jones, ed. (1984). Programming Languages and Their Definition — H. Bekič (1936-1982). Lecture Notes in Computer Science. Vol. 177. Berlin, Heidelberg, New York, Tokyo: Springer-Verlag. doi:10.1007/BFb0048933. ISBN 978-3-540-13378-0. S2CID 7488558.
• Fitzgerald, J.S. and Larsen, P.G., Modelling Systems: Practical Tools and Techniques in Software Engineering. Cambridge University Press, 1998 ISBN 0-521-62348-0 (Japanese Edition pub. Iwanami Shoten 2003 ISBN 4-00-005609-3).
• 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.
• 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
• 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 VDM: a Practitioner's Guide. Springer Verlag Formal Approaches to Computing and Information Technology (FACIT), 1994. ISBN 3-540-19813-X .

बाहरी संबंध

• Information on VDM and VDM++ (archived copy at archive.org)
• Vienna Definition Language (VDL)