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

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

दर्शन

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

इतिहास

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

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

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

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

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

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

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

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

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

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

Basic Types

bool	Boolean datatype	false, true
nat	natural numbers (including zero)	0, 1, 2, 3, 4, 5 ...
nat1	natural numbers (excluding zero)	1, 2, 3, 4, 5, ...
int	integers	..., −3, −2, −1, 0, 1, 2, 3, ...
rat	rational numbers	a/b, where a and b are integers, b is not 0
real	real numbers	...
char	characters	A, B, C, ...
token	structureless tokens	...
<A>	the quote type containing the value <A>	...

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

प्रकार
उपयोगकर्ता आईडी = नेट

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

उपयोगकर्ता आईडी = नेट
यूआईडी आमंत्रित करें == यूआईडी <= 9999

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

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

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

<लाल>, <एम्बर>, <फ्लैशिंगएम्बर>, <हरा>

निर्माता प्रकार: संघ, उत्पाद और मिश्रित प्रकार

केवल मूल प्रकार ही सीमित मूल्य के हैं। नए, अधिक संरचित डेटा प्रकार टाइप कंस्ट्रक्टर का उपयोग करके बनाए जाते हैं।

Basic Type Constructors

T1 | T2 | ... | Tn	Union of types T1,...,Tn
T1*T2*...*Tn	Cartesian product of types T1,...,Tn
T :: f1:T1 ... fn:Tn	Composite (Record) type

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

सिग्नल कलर = <लाल> | <एम्बर> | <चमकतीअम्बर> | <हरा>

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

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

टी :: एफ1:ए1
     f2:A2
     ...
     एफएन:एन

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

दिनांक :: दिन: nat1
        माह:नेट1
        वर्ष: नेट
आमंत्रण mk_Date(d,m,y) == डी <=31 और एम<=12

एक साधारण दिनांक प्रकार मॉडल करता है। मूल्य mk_Date(1,4,2001) 1 अप्रैल 2001 से मेल खाता है। एक तारीख दी गई है d, इजहार d.month महीने का प्रतिनिधित्व करने वाली एक प्राकृतिक संख्या है। यदि चाहें तो प्रति माह दिनों और लीप वर्ष पर प्रतिबंध को अपरिवर्तनीय में शामिल किया जा सकता है। इनका संयोजन:

mk_Date(1,4,2001).माह = 4

संग्रह

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

सेट

सेट प्रकार कंस्ट्रक्टर (लिखित) set of T कहाँ T एक पूर्वनिर्धारित प्रकार है) प्रकार से निकाले गए मानों के सभी परिमित सेटों से बना प्रकार बनाता है T. उदाहरण के लिए, प्रकार परिभाषा समूह = उपयोगकर्ता का सेट एक प्रकार को परिभाषित करता है UGroup के सभी परिमित सेटों से बना है UserId मूल्य. विभिन्न ऑपरेटरों को उनके संघ, प्रतिच्छेदन, उचित और गैर-सख्त उपसमुच्चय संबंधों का निर्धारण आदि के लिए सेट पर परिभाषित किया गया है।

Main operators on sets (s, s1, s2 are sets)

{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. उदाहरण के लिए, प्रकार की परिभाषा

स्ट्रिंग = चार का seq

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

इसलिए, एक क्रम में वस्तुओं का क्रम और पुनरावृत्ति महत्वपूर्ण है [a, b] के बराबर नहीं है [b, a], और [a] के बराबर नहीं है [a, a].

Main operators on sequences (s, s1,s2 are sequences)

[a, b, c]	Sequence enumeration: the sequence of elements a, b and c
[f(x) | x:T & P(x)]	Sequence comprehension: sequence of expressions f(x) for each x of (numeric) type T such that P(x) holds (x values taken in numeric order)
hd s	The head (first element) of s
tl s	The tail (remaining sequence after head is removed) of s
len s	The length of s
elems s	The set of elements of s
s(i)	The ith element of s
inds s	the set of indices for the sequence s
s1^s2	the sequence formed by concatenating sequences s1 and s2

मानचित्र

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

जन्मदिन = मानचित्र स्ट्रिंग टू डेट

एक प्रकार को परिभाषित करता है 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-SL और 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:वास्तविक
पोस्ट आर*आर = एक्स

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

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

SQRT(x:nat)r:वास्तविक
पोस्ट r*r = x और r>=0

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

SQRTP(x:वास्तविक)r:वास्तविक
पूर्व x >=0
पोस्ट r*r = x और r>=0

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

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

SqList: nat का seq -> nat का seq
SqList(s) == यदि s = [] तो [] अन्यथा [(hd s)**2] ^ SqList(tl s)

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

SqListImp(s:seq of nat)r:seq of nat
पोस्ट लेन आर = लेन एस और
     कुल मिलाकर i सेट इंडस्ट्रीज़ s & r(i) = s(i)**2 में

स्पष्ट परिभाषा सरल अर्थ में अंतर्निहित रूप से निर्दिष्ट फ़ंक्शन का कार्यान्वयन है। एक अंतर्निहित विनिर्देश के संबंध में एक स्पष्ट फ़ंक्शन परिभाषा की शुद्धता को निम्नानुसार परिभाषित किया जा सकता है।

एक अंतर्निहित विशिष्टता दी गई:

f(p:T_p)r:T_r
प्री प्री-एफ(पी)
पोस्ट पोस्ट-एफ(पी, आर)

और एक स्पष्ट कार्य:

f:T_p -> T_r

हम कहते हैं कि यह विनिर्देश को पूरा करता है यदि:

सेट T_p और प्री-f(p) => f(p):T_r और पोस्ट-f(p, f(p)) में सभी के लिए p

इसलिए,f एक सही कार्यान्वयन है के रूप में व्याख्या की जानी चाहिएf विशिष्टता को पूरा करता है.

राज्य-आधारित मॉडलिंग

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

उदाहरण के लिए, यदि हमारे पास एक एकल चर से युक्त एक राज्य है someStateRegister : nat, हम इसे VDM-SL में इस प्रकार परिभाषित कर सकते हैं:

का राज्य रजिस्टर
  someStateRegister : nat
अंत

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

आवृत्ति के चर
  someStateRegister : nat

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

लोड(i:nat)
ext wr someStateRegister:nat
कुछस्टेटरजिस्टर पोस्ट करें = i

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

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

जोड़ें(i:nat)
ext wr someStateRegister : nat
someStateRegister = someStateRegister~ + i पोस्ट करें

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

उदाहरण

Further information: Meta-IV (specification language)

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

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

अधिकतम(s:nat का सेट)r:nat
प्री कार्ड एस > 0
सेट एस और में पोस्ट आर
     कुल मिलाकर r' सेट s और r' <= r में

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

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

मल्टीपी(i,j:nat)r:nat
पूर्व सत्य
पोस्ट आर = आई*जे

प्रमाण दायित्व लागू करना forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p)) की एक स्पष्ट परिभाषा के लिए multp:

मल्टीपी(आई,जे) ==
 यदि मैं=0
 फिर 0
 अन्यथा यदि है-सम(i)
      फिर 2*multp(i/2,j)
      अन्यथा j+multp(i-1,j)

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

कुल मिलाकर i, j : nat और multp(i,j):nat और multp(i, j) = i*j

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

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

कतार सार डेटा प्रकार

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

प्रकार

क़ेल्ट = टोकन;
क्यू = क्यूल्ट का सीक;

राज्य की कतार
  प्रश्न: कतार
अंत

परिचालन

पूछताछ(ई:केल्ट)
ext wr q:कतार
पोस्ट क्यू = क्यू~ ^ [ई];

DEQUEUE()e:Qelt
ext wr q:कतार
पूर्व क्यू <> []
पोस्ट q~ = [e]^q;

IS-खाली()r:बूल
एक्सटेंशन तीसरा प्रश्न: कतार
पोस्ट आर <=> (लेन क्यू = 0)

बैंक प्रणाली उदाहरण

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

AccNum = टोकन;
कस्टमनम = टोकन;
संतुलन = पूर्णांक;
ओवरड्राफ्ट = नेट;

AccData :: स्वामी : CustNum
           संतुलन: संतुलन

स्टेट बैंक ऑफ
  अकाउंटमैप: AccNum को AccData में मैप करें
  ओवरड्राफ्ट मैप: कस्टमनम को ओवरड्राफ्ट में मैप करें
inv mk_Bank(अकाउंटमैप,ओवरड्राफ्टमैप) == सेट डोम ओवरड्राफ्ट मैप में सभी ए इन सेट आरएनजी अकाउंट मैप और ए ओनर के लिए
                                        ए.बैलेंस >= -ओवरड्राफ्टमैप(ए.मालिक)

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

परिचालन
NEWC(od : Overdraft)r : CustNum
ext wr ओवरड्राफ्टमैप: कस्टमनम को ओवरड्राफ्ट में मैप करें
पोस्ट r सेट डोम में नहीं है ~overdraftMap और OverdraftMap = ~overdraftMap++ { r |-> od};

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

NEWAC(cu : CustNum)r : AccNum
ext wr अकाउंटमैप: AccNum को AccData में मैप करें
    ओवरड्राफ्ट के लिए तीसरा ओवरड्राफ्टमैप मैप कस्टमनम
प्री सीयू इन सेट डोम ओवरड्राफ्टमैप
पोस्ट आर सेट डोम अकाउंटमैप~ और अकाउंटमैप = अकाउंटमैप~++ {r|-> mk_AccData(cu,0)} में नहीं है

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

ACINF(cu : CustNum)r : AccNum को बैलेंस में मैप करें
एक्सटेंशन तीसरा अकाउंटमैप: AccNum को AccData में मैप करें
पोस्ट r = {an |-> अकाउंटमैप(an).बैलेंस | एक इन सेट डोम अकाउंटमैप और अकाउंटमैप(ए).ओनर = सीयू}

उपकरण समर्थन

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

• VDMTools VDM और VDM++ के लिए अग्रणी व्यावसायिक उपकरण था, जिसका स्वामित्व, विपणन, रखरखाव और विकास CSK Systems द्वारा किया गया था, जो डेनिश कंपनी IFAD द्वारा विकसित पुराने संस्करणों पर आधारित था। मैनुअल और एक व्यावहारिक ट्यूटोरियल उपलब्ध हैं। टूल के पूर्ण संस्करण के लिए सभी लाइसेंस निःशुल्क उपलब्ध हैं। पूर्ण संस्करण में जावा और C++ के लिए स्वचालित कोड जनरेशन, डायनेमिक लिंक लाइब्रेरी और CORBA समर्थन शामिल है।
• ओवरचर एक समुदाय-आधारित ओपन सोर्स पहल है जिसका उद्देश्य सभी वीडीएम बोलियों (वीडीएम-एसएल, वीडीएम++ और वीडीएम-आरटी) के लिए मूल रूप से एक्लिप्स प्लेटफॉर्म के शीर्ष पर लेकिन बाद में विजुअल स्टूडियो कोड प्लेटफॉर्म के शीर्ष पर स्वतंत्र रूप से उपलब्ध टूल समर्थन प्रदान करना है। इसका उद्देश्य इंटरऑपरेबल टूल के लिए एक ढांचा विकसित करना है जो औद्योगिक अनुप्रयोग, अनुसंधान और शिक्षा के लिए उपयोगी होगा।
• vdm-mode VDM-SL, 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. डेटा संशोधन की शुद्धता पर्याप्तता साबित करने पर निर्भर करती है, यानी।

कुल मिलाकर a:ABS_REP और मौजूद r:NEW_REP और a = retr(r)

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

• डोमेन नियम:

फोरऑल आर: NEW_REP और प्री-ओपीए(retr(r)) => प्री-ओपीआर(r)

• मॉडलिंग नियम:

कुल मिलाकर ~r,r:NEW_REP और प्री-ओपीए(retr(~r)) और पोस्ट-ओपीआर(~r,r) => पोस्ट-OPA(retr(~r,), retr(r))

उदाहरण डेटा संशोधन

व्यवसाय सुरक्षा प्रणाली में, श्रमिकों को आईडी कार्ड दिए जाते हैं; इन्हें फ़ैक्टरी में प्रवेश करने और बाहर निकलने पर कार्ड रीडर में फीड किया जाता है। संचालन आवश्यक:

• INIT() सिस्टम को इनिशियलाइज़ करता है, मानता है कि फ़ैक्टरी खाली है
• ENTER(p : Person) रिकॉर्ड करता है कि एक कर्मचारी कारखाने में प्रवेश कर रहा है; श्रमिकों का विवरण आईडी कार्ड से पढ़ा जाता है)
• EXIT(p : Person) रिकॉर्ड करता है कि एक कर्मचारी कारखाने से बाहर निकल रहा है
• IS-PRESENT(p : Person) r : bool यह देखने के लिए जाँच करता है कि कोई निर्दिष्ट कर्मचारी कारखाने में है या नहीं

औपचारिक रूप से, यह होगा:

प्रकार

व्यक्ति = टोकन;
श्रमिक = व्यक्ति का समूह;

के राज्य AWCCS
  अध्यक्ष: श्रमिक
अंत

परिचालन

इस में()
अतिरिक्त लेखक अध्यक्ष: श्रमिक
पोस्ट प्रेस = {};

दर्ज करें(पी: व्यक्ति)
अतिरिक्त लेखक अध्यक्ष: श्रमिक
प्री पी सेट प्रेस में नहीं है
पोस्ट प्रेस = प्रेस ~ यूनियन {पी};

बाहर निकलें(पी: व्यक्ति)
एक्सटेंशन राइटर प्रेसिडेंट: श्रमिक
सेट प्रेस में प्री पी
पोस्ट प्रेस = प्रेस~\{p};

आईएस-वर्तमान (पी: व्यक्ति) आर: बूल
अतिरिक्त तृतीय अध्यक्ष: कार्यकर्ता
सेट प्रेस में पोस्ट आर <=> पी~

चूँकि अधिकांश प्रोग्रामिंग भाषाओं में एक सेट (अक्सर एक सरणी के रूप में) की तुलना में एक अवधारणा होती है, विनिर्देश से पहला कदम अनुक्रम के संदर्भ में डेटा का प्रतिनिधित्व करना है। इन अनुक्रमों को पुनरावृत्ति की अनुमति नहीं देनी चाहिए, क्योंकि हम नहीं चाहते कि एक ही कार्यकर्ता दो बार दिखाई दे, इसलिए हमें नए डेटा प्रकार में एक इनवेरिएंट (कंप्यूटर विज्ञान) जोड़ना होगा। इस मामले में, ऑर्डर देना महत्वपूर्ण नहीं है, इसलिए [a,b] वैसा ही है जैसा कि [b,a].

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

यह भी देखें

• औपचारिक तरीके
• औपचारिक विशिष्टता
• पिजिन कोड
• विधेय तर्क
• प्रस्तावात्मक कलन
• Z विशिष्टता भाषा, VDM-SL का मुख्य विकल्प (तुलना करें)
• कम्पास मॉडलिंग भाषा 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 VDM-SL 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 ISO/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)