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

From Vigyanwiki
No edit summary
No edit summary
Line 96: Line 96:
       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
Line 103: Line 103:
  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).माह = 4
  mk_Date(1,4,2001).month = 4


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


==== सेट ====
==== सेट ====
सेट टाइप कंस्ट्रक्टर (लिखित) <code>set of T</code> कहाँ <code>T</code> एक पूर्वनिर्धारित टाइप है) टाइप से निकाले गए मानों के सभी परिमित सेटों से बना टाइप बनाता है <code>T</code>. उदाहरण के लिए, टाइप डिफ्निसन  समूह = उपयोगकर्ता का सेट
सेट टाइप का कंस्ट्रक्टर (<code>T</code> का लिखित <code>set of T</code> एक पूर्वनिर्धारित टाइप है) टाइप <code>T</code> से खींचे गए मानों के सभी परिमित सेटों से बना टाइप का निर्माण करता है। उदाहरण के लिए टाइप की परिभाषा<syntaxhighlight>
एक टाइप को परिभाषित करता है <code>UGroup</code> के सभी परिमित सेटों से बना है <code>UserId</code> मूल्य. विभिन्न ऑपरेटरों को उनके संघ, प्रतिच्छेदन, उचित और गैर-सख्त उपसमुच्चय संबंधों का निर्धारण आदि के लिए सेट पर परिभाषित किया गया है।
UGroup = set of UserId
 
</syntaxhighlight><code>UserId</code>मानों के सभी परिमित सेटों से बना एक टाइप <code>UGroup</code> को परिभाषित करता है। विभिन्न ऑपरेटरों को उनके संघ, प्रतिच्छेदन, उचित और गैर-सख्त सबसेट संबंधों का निर्धारण आदि के लिए सेट पर परिभाषित किया गया है।
{| border="1" class="wikitable"
{| class="wikitable" border="1"
|+ style="background:#ffdead;" |Main operators on sets (s, s1, s2 are sets)
|+ 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> || Set enumeration: the set of elements <code>a</code>, <code>b</code> and <code>c</code>
Line 146: Line 146:
परिमित अनुक्रम टाइप कंस्ट्रक्टर (लिखित) <code>seq of T</code> कहाँ <code>T</code> एक पूर्वनिर्धारित टाइप है) टाइप से निकाले गए मानों की सभी सीमित सूचियों से बना टाइप बनाता है <code>T</code>. उदाहरण के लिए, टाइप की डिफ्निसन  
परिमित अनुक्रम टाइप कंस्ट्रक्टर (लिखित) <code>seq of T</code> कहाँ <code>T</code> एक पूर्वनिर्धारित टाइप है) टाइप से निकाले गए मानों की सभी सीमित सूचियों से बना टाइप बनाता है <code>T</code>. उदाहरण के लिए, टाइप की डिफ्निसन  


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


एक टाइप को परिभाषित करता है <code>String</code> वर्णों की सभी सीमित श्रृंखलाओं से बना है। विभिन्न ऑपरेटरों को संयोजन के निर्माण, तत्वों और उसके बाद के अनुक्रम आदि के चयन के लिए अनुक्रमों पर परिभाषित किया गया है। इनमें से कई ऑपरेटर इस अर्थ में आंशिक हैं कि उन्हें कुछ अनुप्रयोगों के लिए परिभाषित नहीं किया गया है। उदाहरण के लिए, किसी अनुक्रम के 5वें तत्व का चयन करना जिसमें केवल तीन तत्व हैं, अपरिभाषित है।
एक टाइप को परिभाषित करता है <code>String</code> वर्णों की सभी सीमित श्रृंखलाओं से बना है। विभिन्न ऑपरेटरों को संयोजन के निर्माण, तत्वों और उसके बाद के अनुक्रम आदि के चयन के लिए अनुक्रमों पर परिभाषित किया गया है। इनमें से कई ऑपरेटर इस अर्थ में आंशिक हैं कि उन्हें कुछ अनुप्रयोगों के लिए परिभाषित नहीं किया गया है। उदाहरण के लिए, किसी अनुक्रम के 5वें तत्व का चयन करना जिसमें केवल तीन तत्व हैं, अपरिभाषित है।
Line 178: Line 178:
एक परिमित मानचित्रण दो सेटों, डोमेन और रेंज के बीच, रेंज के डोमेन अनुक्रमण तत्वों के साथ एक पत्राचार है। इसलिए यह एक परिमित कार्य के समान है। वीडीएम-एसएल में मैपिंग टाइप का कंस्ट्रक्टर (लिखित) <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


एक टाइप को परिभाषित करता है <code>Birthdays</code> जो कैरेक्टर स्ट्रिंग्स को मैप करता है <code>Date</code>. फिर से, मैपिंग में अनुक्रमण, मैपिंग को मर्ज करने, उप-मैपिंग को निकालने के लिए ओवरराइटिंग के लिए ऑपरेटरों को मैपिंग पर परिभाषित किया जाता है।
एक टाइप को परिभाषित करता है <code>Birthdays</code> जो कैरेक्टर स्ट्रिंग्स को मैप करता है <code>Date</code>. फिर से, मैपिंग में अनुक्रमण, मैपिंग को मर्ज करने, उप-मैपिंग को निकालने के लिए ओवरराइटिंग के लिए ऑपरेटरों को मैपिंग पर परिभाषित किया जाता है।
Line 211: Line 211:
* अधिक विदेशी विशेषताएं: वीडीएम-एसएल टूल के पुराने संस्करणों में पैरामीटरयुक्त मॉड्यूल और ऐसे मॉड्यूल के इंस्टेंटेशन के लिए भी समर्थन था। हालाँकि, इन सुविधाओं को 2000 के आसपास VDMTools से हटा दिया गया था क्योंकि इनका उपयोग शायद ही कभी औद्योगिक अनुप्रयोगों में किया गया था और इन सुविधाओं के साथ बड़ी संख्या में टूल चुनौतियाँ थीं।
* अधिक विदेशी विशेषताएं: वीडीएम-एसएल टूल के पुराने संस्करणों में पैरामीटरयुक्त मॉड्यूल और ऐसे मॉड्यूल के इंस्टेंटेशन के लिए भी समर्थन था। हालाँकि, इन सुविधाओं को 2000 के आसपास VDMTools से हटा दिया गया था क्योंकि इनका उपयोग शायद ही कभी औद्योगिक अनुप्रयोगों में किया गया था और इन सुविधाओं के साथ बड़ी संख्या में टूल चुनौतियाँ थीं।


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


  SQRT(x:nat)r:वास्तविक
  SQRT(x:nat)r:real
  पोस्ट आर*आर = एक्स
  post r*r = x


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


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


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


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


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


  SqList: nat का seq -> nat का seq
  SqList: seq of nat -> seq of nat
  SqList(s) == यदि s = [] तो [] अन्यथा [(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
       कुल मिलाकर i सेट इंडस्ट्रीज़ s & r(i) = s(i)**2 में
       forall i in set inds s & r(i) = s(i)**2


स्पष्ट डिफ्निसन  सरल अर्थ में अंतर्निहित रूप से निर्दिष्ट फ़ंक्शन का कार्यान्वयन है। एक अंतर्निहित स्पेसिफिकेशन के संबंध में एक स्पष्ट फ़ंक्शन डिफ्निसन  की शुद्धता को निम्नानुसार परिभाषित किया जा सकता है।
स्पष्ट डिफ्निसन  सरल अर्थ में अंतर्निहित रूप से निर्दिष्ट फ़ंक्शन का कार्यान्वयन है। एक अंतर्निहित स्पेसिफिकेशन के संबंध में एक स्पष्ट फ़ंक्शन डिफ्निसन  की शुद्धता को निम्नानुसार परिभाषित किया जा सकता है।
Line 256: Line 256:
एक अंतर्निहित विशिष्टता दी गई:
एक अंतर्निहित विशिष्टता दी गई:
  f(p:T_p)r:T_r
  f(p:T_p)r:T_r
  प्री प्री-एफ(पी)
  pre pre-f(p)
  पोस्ट पोस्ट-एफ(पी, आर)
  post post-f(p, r)


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


हम कहते हैं कि यह स्पेसिफिकेशन को पूरा करता है यदि:
हम कहते हैं कि यह स्पेसिफिकेशन को पूरा करता है यदि:
  सेट T_p और प्री-f(p) => f(p):T_r और पोस्ट-f(p, f(p)) में सभी के लिए 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> विशिष्टता को पूरा करता है.


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


  का राज्य रजिस्टर
  state Register of
   someStateRegister : nat
   someStateRegister : nat
  अंत
  end


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


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


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


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


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


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


जहां <code>~</code> पोस्टकंडिशन में स्टेट वेरिएबल पर प्रतीक ऑपरेशन के निष्पादन से पहले स्टेट वेरिएबल का मान इंगित करता है।
जहां <code>~</code> पोस्टकंडिशन में स्टेट वेरिएबल पर प्रतीक ऑपरेशन के निष्पादन से पहले स्टेट वेरिएबल का मान इंगित करता है।
Line 302: Line 303:
यह एक अंतर्निहित फ़ंक्शन डिफ्निसन  का एक उदाहरण है। फ़ंक्शन सकारात्मक पूर्णांकों के सेट से सबसे बड़ा तत्व लौटाता है:
यह एक अंतर्निहित फ़ंक्शन डिफ्निसन  का एक उदाहरण है। फ़ंक्शन सकारात्मक पूर्णांकों के सेट से सबसे बड़ा तत्व लौटाता है:


  अधिकतम(s:nat का सेट)r:nat
  max(s:set of nat)r:nat
  प्री कार्ड एस > 0
  pre card s > 0
  सेट एस और में पोस्ट आर
  post r in set s and
       कुल मिलाकर r' सेट s और r' <= r में
       forall r' in set s & r' <= r


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


===प्राकृतिक संख्या गुणन===
===प्राकृतिक संख्या गुणन===
  मल्टीपी(i,j:nat)r:nat
  multp(i,j:nat)r:nat
  पूर्व सत्य
  pre true
  पोस्ट आर = आई*जे
  post r = i*j


प्रमाण दायित्व लागू करना <code>forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))</code> की एक स्पष्ट डिफ्निसन  के लिए <code>multp</code>:
प्रमाण दायित्व लागू करना <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) ==
   यदि मैं=0
   if i=0
   फिर 0
   then 0
   अन्यथा यदि है-सम(i)
   else if is-even(i)
       फिर 2*multp(i/2,j)
       then 2*multp(i/2,j)
       अन्यथा j+multp(i-1,j)
       else j+multp(i-1,j)


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


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


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


  प्रकार
  types


  क़ेल्ट = टोकन;
  Qelt = token;
  क्यू = क्यूल्ट का सीक;
  Queue = seq of Qelt;


  राज्य की कतार
  state TheQueue of
   प्रश्न: कतार
   q : Queue
  अंत
  end


  परिचालन
  operations


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


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


  IS-खाली()r:बूल
  IS-EMPTY()r:bool
  एक्सटेंशन तीसरा प्रश्न: कतार
  ext rd q:Queue
  पोस्ट आर <=> (लेन क्यू = 0)
  post r <=> (len q = 0)


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


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


  AccData :: स्वामी : CustNum
  AccNum = token;
             संतुलन: संतुलन
CustNum = token;
Balance = int;
Overdraft = nat;
 
AccData :: owner : CustNum
             balance : Balance


  स्टेट बैंक ऑफ
  state Bank of
   अकाउंटमैप: AccNum को AccData में मैप करें
   accountMap : map AccNum to AccData
   ओवरड्राफ्ट मैप: कस्टमनम को ओवरड्राफ्ट में मैप करें
   overdraftMap : map CustNum to Overdraft
  inv mk_Bank(अकाउंटमैप,ओवरड्राफ्टमैप) {{=}}{{=}} सेट डोम ओवरड्राफ्ट मैप में सभी ए इन सेट आरएनजी अकाउंट मैप और ए ओनर के लिए
  inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and
                                         ए.बैलेंस >= -ओवरड्राफ्टमैप(ए.मालिक)
                                         a.balance >= -overdraftMap(a.owner)


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


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


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


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


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


  ACINF(cu : CustNum)r : AccNum को बैलेंस में मैप करें
  ACINF(cu : CustNum)r : map AccNum to Balance
  एक्सटेंशन तीसरा अकाउंटमैप: AccNum को AccData में मैप करें
  ext rd accountMap : map AccNum to AccData
  पोस्ट r = {an |-> अकाउंटमैप(an).बैलेंस | एक इन सेट डोम अकाउंटमैप और अकाउंटमैप(ए).ओनर = सीयू}
  post r = {an |-> accountMap(an).balance | an in set dom accountMap & accountMap(an).owner = cu}


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


  कुल मिलाकर a:ABS_REP और मौजूद 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>. नए प्रतिनिधित्व पर किसी भी डेटा टाइप के इनवेरिएंट (कंप्यूटर विज्ञान) को संरक्षित करने के लिए नए संचालन और कार्यों को दिखाया जाना चाहिए। यह सिद्ध करने के लिए कि नए संचालन और फ़ंक्शन मॉडल मूल स्पेसिफिकेशन में पाए गए हैं, दो प्रमाण दायित्वों का निर्वहन करना आवश्यक है:
*डोमेन नियम:
*डोमेन नियम:
  फोरऑल आर: NEW_REP और प्री-ओपीए(retr(r)) => प्री-ओपीआर(r)
  forall r: NEW_REP & pre-OPA(retr(r)) => pre-OPR(r)
* मॉडलिंग नियम:
* मॉडलिंग नियम:
  कुल मिलाकर ~r,r:NEW_REP और प्री-ओपीए(retr(~r)) और पोस्ट-ओपीआर(~r,r) => पोस्ट-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))


====उदाहरण डेटा संशोधन====
====उदाहरण डेटा संशोधन====
Line 457: Line 461:
औपचारिक रूप से, यह होगा:
औपचारिक रूप से, यह होगा:


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


  के राज्य AWCCS
  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
  पोस्ट प्रेस = प्रेस~\{p};
  post pres = pres~ union {p};


  आईएस-वर्तमान (पी: व्यक्ति) आर: बूल
  EXIT(p : Person)
  अतिरिक्त तृतीय अध्यक्ष: कार्यकर्ता
ext wr pres : Workers
  सेट प्रेस में पोस्ट आर <=> पी~
  pre p in set pres
  post pres = pres~\{p};


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


Revision as of 13:03, 3 August 2023

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

फिलोसॉफी

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

इतिहास

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

<ब्लॉककोट>

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

</ब्लॉककोट>

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

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

इंग्लिश स्कूल वीडीएम के उन विधियों पर क्लिफ जोन्स (कंप्यूटर वैज्ञानिक) के काम से प्राप्त हुआ है जो विशेष रूप से लैंग्वेज डिफ्निसन और कंपाइलर डिजाइन से संबंधित नहीं हैं (जोन्स 1980, 1990)। यह निरंतर मॉडलिंग पर जोर देता है[7] आधार टाइप के समृद्ध संग्रह से निर्मित डेटा टाइप के उपयोग के माध्यम से बताएं। कार्यक्षमता को समान्यत: उन ऑपरेशनों के माध्यम से वर्णित किया जाता है जिनके राज्य पर दुष्प्रभाव हो सकते हैं और जो अधिकतर पूर्व नियम और पोस्टकंडिशन का उपयोग करके अंतर्निहित रूप से निर्दिष्ट होते हैं। डेनिश स्कूल (डाइन्स ब्योर्नर या ब्योर्नर एट अल. 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].

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


मानचित्र

एक परिमित मानचित्रण दो सेटों, डोमेन और रेंज के बीच, रेंज के डोमेन अनुक्रमण तत्वों के साथ एक पत्राचार है। इसलिए यह एक परिमित कार्य के समान है। वीडीएम-एसएल में मैपिंग टाइप का कंस्ट्रक्टर (लिखित) 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: Meta-IV (specification language)

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

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

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)

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

operations
NEWC(od : Overdraft)r : CustNum
ext wr overdraftMap : map CustNum to Overdraft
post r not in set dom ~overdraftMap and overdraftMap = ~overdraftMap ++ { r |-> od};

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

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

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

ACINF(cu : CustNum)r : map AccNum to Balance
ext rd accountMap : map AccNum to AccData
post r = {an |-> accountMap(an).balance | an in set dom accountMap & accountMap(an).owner = cu}

उपकरण समर्थन

कई अलग-अलग उपकरण 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 डेटामैटिक सेंटर द्वारा विकसित किया गया था।[8] इसी टाइप CHILL और Modula-2 के शब्दार्थ को VDM का उपयोग करके उनके मानकों में वर्णित किया गया था।
  • कॉनफॉर्म: ब्रिटिश एयरोस्पेस में एक प्रयोग जिसमें एक विश्वसनीय गेटवे के पारंपरिक डेवलपमेंट की तुलना वीडीएम का उपयोग करके किए गए डेवलपमेंट से की गई है।
  • धूल-विशेषज्ञ: सुरक्षा संबंधी अनुप्रयोग के लिए यूके में एडेलार्ड द्वारा चलाया गया एक प्रोजेक्ट जो यह निर्धारित करता है कि औद्योगिक संयंत्रों के लेआउट में सुरक्षा उपयुक्त है।
  • VDMTools का विकास: VDMTools टूल सूट के अधिकांश घटक स्वयं VDM का उपयोग करके विकसित किए गए हैं। यह डेवलपमेंट डेनमार्क में IFAD और जापान में सीएसके होल्डिंग्स कॉर्पोरेशन में किया गया है।[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 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 .


संदर्भ

  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


बाहरी संबंध

Retrieved from ‘https://www.vigyanwiki.in/index.php?title=वियना_विकास_विधि&oldid=239453’