औपचारिक सत्यापन और प्रूफ असिस्टेंट
औपचारिक सत्यापन, मशीन-जांच किए गए गणितीय प्रमाण द्वारा, यह स्थापित करता है कि सॉफ्टवेयर अपनी विशिष्टता को पूरा करता है; प्रूफ असिस्टेंट वे उपकरण हैं जो ऐसे प्रमाणों का निर्माण और जांच करते हैं।
Definition
औपचारिक सत्यापन एक कठोर, मशीन-जांच किए गए प्रमाण का निर्माण है कि एक प्रणाली एक औपचारिक विशिष्टता को संतुष्ट करती है, और एक प्रूफ असिस्टेंट एक सॉफ्टवेयर है जो उपयोगकर्ता को ऐसे प्रमाण विकसित करने में मदद करता है और यांत्रिक रूप से उनकी वैधता की जांच करता है।
Scope
यह विषय निगमनात्मक सत्यापन और इंटरैक्टिव प्रमेय सिद्ध करने को शामिल करता है: टाइप थ्योरी या उच्च-क्रम तर्क (जैसे Coq, Isabelle, Lean, और Agda) पर आधारित प्रूफ असिस्टेंट, विश्वसनीय प्रमाण के लिए LCF दृष्टिकोण, प्रस्ताव-के-रूप-में-प्रकार (propositions-as-types) नींव, प्रमाण स्वचालन और रणनीति, और कंपाइलर और ऑपरेटिंग-सिस्टम कर्नेल सहित ऐतिहासिक सत्यापित कलाकृतियाँ।
Core questions
- पूर्ण कार्यात्मक शुद्धता को कैसे सिद्ध और मशीन-जांच किया जा सकता है?
- प्रूफ असिस्टेंट विश्वसनीय क्यों हैं, और विश्वसनीय कंप्यूटिंग आधार क्या है?
- कर्री-हावर्ड पत्राचार (Curry-Howard correspondence) प्रमाणों और कार्यक्रमों को कैसे जोड़ता है?
- कंपाइलर और कर्नेल जैसी वास्तविक प्रणालियों को सत्यापित करने के लिए क्या करना पड़ता है?
Key theories
- विश्वसनीय प्रमाण के लिए LCF दृष्टिकोण
- गॉर्डन, मिलनर और वाड्सवर्थ के एडिनबर्ग LCF ने एक छोटा विश्वसनीय प्रमाण कर्नेल पेश किया जिसके माध्यम से सभी प्रमेयों को गुजरना चाहिए, ताकि जटिल स्वचालन भी गलत प्रमाण उत्पन्न न कर सके।
- सत्यापित कंपाइलर (CompCert)
- लेरॉय का CompCert एक C कंपाइलर है जिसे एक प्रूफ असिस्टेंट में सही साबित किया गया है, जिसमें एक मशीन-जांच किया गया प्रमेय है कि उत्पन्न कोड स्रोत कार्यक्रम के सिमेंटिक्स को परिष्कृत करता है।
- सत्यापित ऑपरेटिंग-सिस्टम कर्नेल (seL4)
- क्लेन और उनके सहयोगियों ने seL4 माइक्रोकर्नेल के लिए कार्यात्मक शुद्धता का एक मशीन-जांच किया गया प्रमाण तैयार किया, जो निम्न-स्तरीय सिस्टम सॉफ्टवेयर के एंड-टू-एंड सत्यापन को प्रदर्शित करता है।
Clinical relevance
मशीनीकृत सत्यापन महत्वपूर्ण सॉफ्टवेयर के लिए उपलब्ध उच्चतम आश्वासन प्रदान करता है, परीक्षण-आधारित विश्वास के बजाय सिद्ध गारंटी के साथ कंपाइलर, कर्नेल और क्रिप्टोग्राफिक लाइब्रेरी का उत्पादन करता है। प्रूफ असिस्टेंट का उपयोग तेजी से गणित को औपचारिक रूप देने के लिए भी किया जा रहा है।
History
इंटरैक्टिव प्रमेय सिद्ध करना 1970 के दशक में एडिनबर्ग LCF के साथ शुरू हुआ, जिसकी ML मेटाभाषा और विश्वसनीय कर्नेल ने बाद की प्रणालियों को आकार दिया। Coq और Agda जैसे टाइप-थ्योरी-आधारित असिस्टेंट और Isabelle/HOL जैसे उच्च-क्रम-तर्क प्रणालियाँ अगले दशकों में परिपक्व हुईं, जिसका समापन ऐतिहासिक सत्यापित कलाकृतियों में हुआ: CompCert कंपाइलर (2009) और seL4 कर्नेल (2009)।
Debates
- सत्यापन की लागत बनाम प्राप्त आश्वासन
- बड़ी प्रणालियों के मशीन-जांच किए गए प्रमाणों का निर्माण करने में अत्यधिक प्रयास लगता है, जिससे इस बात पर बहस छिड़ जाती है कि पूर्ण सत्यापन कहाँ उचित है बनाम कहाँ हल्के-फुल्के तरीके पर्याप्त हैं, और कितना प्रमाण स्वचालित किया जा सकता है।
Key figures
- Robin Milner
- Michael Gordon
- Xavier Leroy
- Gerwin Klein
- Robert Harper
Related topics
Seminal works
- gordon1979
- leroy2009
- klein2009
- harper2016
Frequently asked questions
- प्रूफ असिस्टेंट क्या है?
- एक प्रूफ असिस्टेंट एक सॉफ्टवेयर है जिसमें एक उपयोगकर्ता औपचारिक प्रमाणों का इंटरैक्टिव रूप से निर्माण करता है जबकि सिस्टम यांत्रिक रूप से हर कदम की जांच करता है, ताकि एक पूर्ण प्रमाण एक छोटे, अच्छी तरह से जांचे गए कर्नेल तक विश्वसनीय हो।
- किसी प्रोग्राम को सत्यापित करना उसका परीक्षण करने से कैसे भिन्न है?
- परीक्षण चयनित इनपुट पर व्यवहार की जांच करता है और केवल बग्स की उपस्थिति को प्रकट कर सकता है, जबकि औपचारिक सत्यापन विशिष्टता द्वारा अनुमत सभी इनपुट के लिए शुद्धता साबित करता है, निर्दिष्ट त्रुटियों की अनुपस्थिति को स्थापित करता है।