Coq के लिए नरम परिचय: शुरू

प्रस्तावना

यह कोई रहस्य नहीं है कि कार्यक्रमों में त्रुटियों से दु: खद परिणाम हो सकते हैं। इतिहास कई मामलों को जानता है जब एक काउंटर के अतिप्रवाह या एक अखंड अपवाद के परिणामस्वरूप बड़ी सामग्री लागत और मानव हताहत होते हैं। इसलिए, उदाहरण के लिए, 4 जून 1996 को, यूरोपीय एरियन 5 लॉन्च वाहन शाब्दिक रूप से उड़ान के 39 वें सेकंड में गिर गया। घटना के विश्लेषण से पता चला कि दुर्घटना एक सॉफ्टवेयर त्रुटि के कारण हुई। क्षति लगभग $ 7 बिलियन थी। फरवरी 1991 में, पैट्रियट मिसाइल एक गोल त्रुटि के कारण लक्ष्य से चूक गई, अतिरिक्त 500 मीटर की उड़ान भरने में सफल रही। नुकसान: 28 की मौत और सौ से ज्यादा घायल इस तरह की त्रुटियां हार्डवेयर में भी पाई जाती हैं। फ़्लोटिंग-पॉइंट संख्याओं के गलत विभाजन से संबंधित पेंटियम प्रोसेसर में हाल ही में बग ने इंटेल को दोषपूर्ण चिप्स को बदलने के लिए मजबूर किया। इस गलती की कीमत कंपनी को $ 475 मिलियन थी।

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

औपचारिक सत्यापन प्रक्रिया एक लंबा और नियमित कार्य है। इसलिए, यह सभी मामलों में उचित नहीं है। रोज़मर्रा के अनुप्रयोगों के लिए, नियमित परीक्षण भी उपयुक्त है। यहाँ यह समझना चाहिए कि परीक्षण कार्यक्रम में त्रुटियों की अनुपस्थिति और औपचारिक विवरण के अनुपालन को साबित नहीं कर सकता है।

बेशक, सभी कथन स्वचालित रूप से सिद्ध नहीं किए जा सकते हैं। ऐसे मामलों में, प्रूफ चेकर (प्रूफ असिस्टेंट) सिस्टम बचाव में आते हैं, जिनमें से एक Coq है।

परिचय

Coq प्रमेयों को साबित करने के लिए एक इंटरैक्टिव शेल है, जो आश्रित प्रकारों के साथ अपनी स्वयं की कार्यात्मक प्रोग्रामिंग भाषा का उपयोग करता है - गैलिना। यह 80 के दशक के मध्य में फ्रेंच INRIA संस्थान के कर्मचारियों द्वारा आविष्कार और कार्यान्वित किया गया था। Coq वर्तमान में GNU / Linux, Windows और MacOS के लिए उपलब्ध है। स्रोत कोड लाइसेंस LGPL v.2 की शर्तों के तहत वितरित किए जाते हैं।

Coq के साथ काम करने के कई तरीके हैं: इंटरैक्टिव मोड में कंसोल में, CoqIDE में ग्राफिकल मोड में या प्रूफ जनरल प्लगइन का उपयोग करके Emacs में।



तो, Coq स्थापित है और जाने के लिए तैयार है। चलो कुछ लिखने की कोशिश करो!

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

 आगमनात्मक दिन: प्रकार: =
   |  सोमवार: दिन
   |  tuesday: दिन
   |  वेडनेसडे: दिन
   |  थर्सडे: दिन
   |  शुक्रवार: दिन
   |  शनिवार: दिन
   |  रविवार: दिन।

इस घोषणा के साथ, हम Coq को बताते हैं कि हम डेटा मानों के एक नए सेट को परिभाषित करना चाहते हैं - एक प्रकार। इस प्रकार को day कहा जाता day , और इस प्रकार के मान monday , tuesday , आदि हैं, अब हम day प्रकार के मानों पर एक फ़ंक्शन लिख सकते day । हम एक फ़ंक्शन लिखेंगे जो अगले कार्य दिवस की गणना करता है:

 परिभाषा अगले_वेकडे (दिन: दिन): दिन: =
   मैच के साथ डी
   |  सोमवार => दशहरा
   |  tuesday => वेडनेसडे
   |  wednesday => थर्सडे
   |  थर्सडे => शुक्रवार
   |  शुक्रवार => सोमवार
   |  शनिवार => सोमवार
   |  रविवार => सोमवार
   अंत।

Coq में टाइप इंफ़ेक्शन, पैटर्न मिलान और अन्य चीजें हैं जो कार्यात्मक प्रोग्रामिंग भाषाओं के लिए सामान्य हैं।

हमने फ़ंक्शन को परिभाषित करने के बाद, कुछ उदाहरणों का उपयोग करके अपने प्रदर्शन का परीक्षण करने का समय दिया है। सबसे पहले, हम Eval simpl उपयोग कर सकते हैं:

 में सरल (अगले_दैवीय शुक्रवार)।
    (* ==> सोमवार: दिन *)
 में सरल (अगले_दिन का दिन (अगला_दिन का शनिवार))।
    (* ==> tuesday: दिन *)

दूसरे, हम स्पष्ट रूप से अपेक्षित परिणाम दिखा सकते हैं और इसे जाँचने के लिए Coq को निर्देश दे सकते हैं:

 उदाहरण test_next_weekday:
   (next_weekday (अगला_वीडे शनिवार)) = tuesday।
 सबूत।  simpl।  रिफ्लेक्सिविटी।  QED।

जब कोकिदे में काम करते हैं तो मध्यवर्ती परिणाम देखने के लिए चरण-दर-चरण कार्यक्रम निष्पादन का उपयोग करना सुविधाजनक होता है:


तीसरा तरीका परिभाषा को कुछ प्रोग्रामिंग भाषा (OCaml, स्कीम या हास्केल) में निकालना है। यह Coq प्रणाली की मुख्य विशेषताओं में से एक है, जिसके लिए सब कुछ विकसित किया गया था:

 निष्कर्षण भाषा Ocaml।
 एक्सट्रैक्शन "/tmp/day.ml" next_weekday।

यहाँ OCaml में हमारे फ़ंक्शन के निष्कर्षण के परिणामस्वरूप क्या हुआ है:

 प्रकार दिन =
 |  सोमवार
 |  मंगलवार
 |  बुधवार
 |  बृहस्पतिवार
 |  शुक्रवार
 |  शनिवार
 |  रविवार

 (** वैल नेक्स्ट_वीडेडे: दिन -> दिन **)

 चलिए अगला_वेकडे = फ़ंक्शन
 |  सोमवार -> मंगलवार
 |  मंगलवार -> बुधवार
 |  बुधवार -> गुरुवार
 |  गुरुवार -> शुक्रवार
 |  _ -> सोमवार

निष्कर्ष

निम्नलिखित अनुभागों में, हम पुनरावर्ती कार्यों को निर्धारित करने और साक्ष्य की मुख्य रणनीति के साथ काम करने के तरीकों पर विचार करेंगे।

अनुशंसित पढ़ने:

1. सॉफ्टवेयर नींव
2. निर्भर प्रकार के साथ प्रमाणित प्रोग्रामिंग

अगला भाग