गार्डेड कमांड लैंग्वेज

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

'GCL' की एक महत्वपूर्ण प्रापर्टी नान-टर्मिनिज्म प्रोग्रामिंग है। उदाहरण के लिए, यदि-विवरण में, कई विकल्प सच हो सकते हैं, और जो चुनने का विकल्प रनटाइम पर किया जाता है, जब if-विवरण निष्पादित किया जाता है। यह प्रोग्रामर को अनावश्यक विकल्प चुनने से मुक्त करता है और कार्यक्रमों के औपचारिक विकास में सहायता करता है।

'GCL' में मल्टीपल असाइनमेंट स्टेटमेंट सम्मिलित है। उदाहरण के लिए, स्टेट्मन्ट का निष्पादन x, y:= y, x पहले दाईं ओर के मानों का मूल्यांकन करके और फिर उन्हें बाईं ओर के चर में संग्रहीत करके किया जाता है। इस प्रकार, यह स्टेट्मन्ट x और y के मानों को बदल देता है।

निम्नलिखित पुस्तकें GCL का उपयोग करके कार्यक्रमों के विकास पर चर्चा करती हैं:

• Dijkstra, Edsger W. (1976). अ डिसप्लिन ऑफ प्रोग्रामिंग. Prentice Hall. ISBN 978-0132158718.
• Gries, D. (1981). प्रोग्रामिंग का विज्ञान. Monographs in Computer Science (in English, Spanish, Japanese, Chinese, Italian, and Russian). New York: Springer Verlag. doi:10.1007/978-1-4612-5983-1. ISBN 978-0-387-96480-5. S2CID 37034126.{{cite book}}: CS1 maint: unrecognized language (link)
• Dijkstra, Edsger W.; Feijen, Wim H.J. (1988). प्रोग्रामिंग की एक विधि. Boston, MA: Addison-Wesley Longman Publishing Co., Inc. p. 200. ISBN 978-0-201-17536-3.
• Kaldewaij, Anne (1990). प्रोग्रामिंग: एल्गोरिदम की व्युत्पत्ति. Prentice-Hall, Inc. ISBN 0132041081.
• Cohen, Edward (1990). David Gries (ed.). 1990 के दशक में प्रोग्रामिंग: कार्यक्रमों की गणना का एक परिचय. Texts and Monographs in Computer Science. Springer Verlag. doi:10.1007/978-1-4613-9706-9. ISBN 978-1-4613-9706-9. S2CID 1509875.

गार्डेड कमांड

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

सिंटेक्स (प्रोग्रामिंग लैंग्वेजएँ)

एक गार्डेड कमांड G → S के रूप का एक स्टेट्मन्ट (प्रोग्रामिंग) है, जहां

• G एक प्रापज़िशन है, जिसे गार्ड कहा जाता है।
• S एक स्टेट्मन्ट है।

शब्दार्थ

जिस समय किसी गणना में G का सामना होता है, उसका मूल्यांकन किया जाता है।

• यदि G सत्य है, तो S निष्पादित करें।
• यदि G गलत है, तो क्या करना है यह तय करने के लिए संदर्भ को देखें (किसी भी स्थिति में, S निष्पादित न करें)।

स्किप और एबॉर्ट

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

सिंटेक्स

स्किप

एबॉर्ट

शब्दार्थ

• स्किप: कुछ न करें
• एबॉर्ट: कुछ भी करो

असाइनमेंट (कंप्यूटर प्रोग्रामिंग)

चर (प्रोग्रामिंग) को मान निर्दिष्ट करता है।

सिंटेक्स

v := E

या

 v0, v1, ..., vn := E0, E1, ..., En

जहाँ

• v प्रोग्राम वेरिएबल हैं।
• E उनके संबंधित चर के समान डेटा प्रकार की अभिव्यक्ति हैं।

श्रृंखलन

स्टेट्मन्टों को एक अर्धविराम (;) से अलग किया जाता है।

संकलन (प्रोग्रामिंग): if

संकलन (प्रायः "सशर्त स्टेट्मन्ट" या "if स्टेट्मन्ट" कहा जाता है) गार्डेड कमांड की एक सूची है, जिनमें से एक को निष्पादित करने के लिए चुना जाता है। यदि एक से अधिक गार्ड सत्य हैं, तो एक स्टेट्मन्ट जिसका गार्ड सत्य है, को नान-टर्मिनिज्म रूप से निष्पादित करने के लिए चुना जाता है। यदि कोई गार्ड सत्य नहीं है, तो परिणाम अपरिभाषित है। क्योंकि कम से कम एक गार्ड सत्य होना चाहिए, खाली स्टेटमेंट स्किप की प्रायः आवश्यकता होती है। स्टेट्मन्ट if fi के पास कोई गार्डेड कमांड नहीं है, तो कोई सच्चा गार्ड कभी नहीं होता है। इसलिए, if fi एबॉर्ट के बराबर है।

सिंटेक्स

 if G0 → S0

 □ G1 → S1
...
 □ Gn → Sn
fi

शब्दार्थ

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

उदाहरण

सरल

छद्मकोड में:

if a < b then set c to True

else set c to False

गार्डेड कमांड लैंग्वेज में:

 if a < b → c := true

 □ a ≥ b → c := false
fi

स्किप का प्रयोग

छद्मकोड में:

if error is True then set x to 0

गार्डेड कमांड लैंग्वेज में:

if error → x := 0

 □ error → skip
fi

यदि दूसरा गार्ड हटा दिया गया है और त्रुटि गलत है, तो परिणाम एबॉर्ट हो जाएगा।

अधिक गार्ड सत्य

if a ≥ b → max := a

 □ b ≥ a → max := b
fi

यदि a = b है, तो समान परिणामों के साथ अधिकतम के लिए नए मान के रूप में a या b को चुना जाता है। यद्यपि, कार्यान्वयन से पता चल सकता है कि एक दूसरे की तुलना में आसान या तेज़ है। चूँकि प्रोग्रामर के लिए कोई अंतर नहीं है, कोई भी कार्यान्वयन करेगा।

रेपटिशन: do

इस दोहराव या लूप का निष्पादन नीचे दिखाया गया है।

सिंटेक्स

G0 → S0 करें
 □ G1 → S1
...

 □ Gn → Sn
od

शब्दार्थ

रेपटिशन के निष्पादन में 0 या अधिक रेपटिशनयों को निष्पादित करना सम्मिलित है, जहां एक रेपटिशन में (गैर-निर्धारिती रूप से) एक गार्डेड कमांड चुनना सम्मिलित है Gi → Si किसका रक्षक Gi सत्य का मूल्यांकन करता है और कमांड निष्पादित करता है Si. इस प्रकार, यदि सभी गार्ड प्रारंभ में झूठे हैं, तो रेपटिशन निष्पादित किए बिना, रेपटिशन तुरंत समाप्त हो जाती है। दोहराव do od का निष्पादन, जिसमें कोई गार्डेड कमांड नहीं है, 0 रेपटिशनयों को निष्पादित करता है, इसलिए do od स्किप के बराबर है।

उदाहरण

मूल यूक्लिडियन एल्गोरिथ्म

a, b := A, B;

do a < b → b := b - a
 □ b < a → a := a - b
od

यह रेपटिशन तब समाप्त होती है जब a = b, इस स्थिति में a और b, A और B का सबसे बड़ा सामान्य भाजक रखते हैं।

डिज्क्स्ट्रा इस एल्गोरिदम में दो अनंत चक्रों को सिंक्रनाइज़ करने का एक तरीका देखता है a:= a - b और b:= b - a इस तरह से कि a≥0 और b≥0 सत्य रहता है।

विस्तारित यूक्लिडियन एल्गोरिथ्म

a, b, x, y, u, v := A, B, 1, 0, 0, 1;

do b ≠ 0 →
   q, r := a div b, a mod b;
   a, b, x, y, u, v := b, r, u, v, x - q*u, y - q*v

यह रेपटिशन तब समाप्त होती है जब b = 0, इस स्थिति में चर बेज़आउट की पहचान का समाधान रखते हैं: xA + yB = gcd(A,B) ।

नान-टर्मिनिज्म सॉर्ट

do a>b → a, b := b, a

 □ b>c → b, c := c, b
 □ c>d → c, d := d, c
od

प्रोग्राम तत्वों को क्रमपरिवर्तित करता रहता है जबकि उनमें से एक उसके आनुक्रमिक से बड़ा होता है। यह नान-टर्मिनिज्म बबल सॉर्ट अपने नियतात्मक संस्करण की तुलना में अधिक कुशल नहीं है, लेकिन यह साबित करना आसान है: यह तब तक नहीं रुकेगा जब तक कि तत्वों को सॉर्ट नहीं किया जाता है और प्रत्येक चरण में यह कम से कम 2 तत्वों को सॉर्ट करता है।

Arg मैक्स

x, y = 1, 1;

do x≠n →
   if f(x) ≤ f(y) → x := x+1
    □ f(x) ≥ f(y) → y := x; x := x+1
   fi
od

यह एल्गोरिदम मान 1 ≤ y ≤ n पाता है जिसके लिए दिया गया पूर्णांक फ़ंक्शन f अधिकतम है। न केवल गणना बल्कि अंतिम स्थिति भी आवश्यक रूप से विशिष्ट रूप से निर्धारित नहीं होती है।

अनुप्रयोग

निर्माण द्वारा सही प्रोग्राम

गार्डेड कमांडों के अवलोकन संबंधी अनुरूपता संबंध को एक जाली (कमांड) में सामान्यीकृत करने से शोधन कैलकुलस का मार्ग प्रशस्त हुआ है। इसे B-मेथड जैसी औपचारिक विधियों में यंत्रीकृत किया गया है जो किसी को उनके विनिर्देशों से औपचारिक रूप से प्रोग्राम प्राप्त करने की अनुमति देता है।

अतुल्यकालिक सर्किट

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

PullDownGuard → y := 0

PullUpGuard → y := 1

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

मॉडल जांच

गार्डेड कमांड का उपयोग प्रोमेला प्रोग्रामिंग लैंग्वेज में किया जाता है, जिसका उपयोग SPIN मॉडल चेकर द्वारा किया जाता है। SPIN समवर्ती सॉफ़्टवेयर अनुप्रयोगों के सही संचालन की पुष्टि करता है।

अन्य

पर्ल मॉड्यूल Commands::Guarded डिज्कस्ट्रा के गार्डेड कमांड पर एक नियतात्मक, सुधारात्मक संस्करण लागू करता है।