स्वयंसिद्ध सिमेंटिक्स और प्रोग्राम लॉजिक्स

स्वयंसिद्ध सिमेंटिक्स कार्यक्रमों को उनकी अवस्थाओं के बारे में तार्किक अभिकथन (logical assertions) द्वारा चित्रित करता है, जिसमें होरे लॉजिक और उसके उत्तराधिकारी कार्यक्रमों को सही साबित करने के लिए नियम प्रदान करते हैं।

Definition

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

Scope

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

Core questions

• किसी विनिर्देशन के सापेक्ष किसी प्रोग्राम को सही कैसे सिद्ध किया जा सकता है?
• लूप इनवेरिएंट क्या है और यह सत्यापन के लिए इतना महत्वपूर्ण क्यों है?
• प्रेडिकेट ट्रांसफॉर्मर शुद्धता के लिए आवश्यक शर्तों की गणना कैसे करते हैं?
• साझा हीप मेमोरी को बदलने वाले कार्यक्रमों के बारे में मॉड्यूलर तरीके से कैसे तर्क किया जा सकता है?

Key theories

होरे लॉजिक

होरे ने {P} C {Q} ट्रिपल्स पर अनुमान नियमों की एक स्वयंसिद्ध प्रणाली प्रस्तुत की, जो यह साबित करने के लिए एक रचनात्मक विधि प्रदान करती है कि एक प्रोग्राम अपने विनिर्देशन को पूरा करता है।

सबसे कमजोर पूर्वशर्तें और गार्डेड कमांड

डिज्क्स्ट्रा का प्रेडिकेट-ट्रांसफॉर्मर सिमेंटिक्स सबसे कमजोर पूर्वशर्त को परिभाषित करता है जो यह गारंटी देता है कि एक प्रोग्राम एक उत्तरशर्त प्राप्त करता है, जो सही कार्यक्रमों के व्यवस्थित व्युत्पत्ति का समर्थन करता है।

सेपरेशन लॉजिक

रेनॉल्ड्स और ओ'हर्न ने होरे लॉजिक को एक सेपरेटिंग कंजंक्शन के साथ विस्तारित किया जो साझा परिवर्तनीय डेटा संरचनाओं और पॉइंटर्स को हेरफेर करने वाले कार्यक्रमों के बारे में स्थानीय, मॉड्यूलर तर्क को सक्षम बनाता है।

Clinical relevance

प्रोग्राम लॉजिक्स निगमनात्मक प्रोग्राम सत्यापन की रीढ़ हैं, जिनका उपयोग महत्वपूर्ण सॉफ्टवेयर की शुद्धता को साबित करने वाले उपकरणों में और ऑपरेटिंग-सिस्टम और कंपाइलर घटकों के मशीनीकृत प्रमाणों में किया जाता है। विशेष रूप से सेपरेशन लॉजिक ने पॉइंटर-मैनिपुलेटिंग कोड के स्केलेबल सत्यापन को व्यावहारिक बनाया।

History

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

Debates

सत्यापन प्रयास बनाम आश्वासन

एक लगातार प्रश्न यह है कि विनिर्देशों और इनवेरिएंट्स को लिखने के पर्याप्त मैन्युअल प्रयास को निगमनात्मक सत्यापन द्वारा प्रदान की जाने वाली मजबूत शुद्धता गारंटी के साथ कैसे संतुलित किया जाए, जो स्वचालन और हल्के-फुल्के तरीकों को प्रेरित करता है।

Key figures

• C. A. R. Hoare
• Robert Floyd
• Edsger Dijkstra
• John Reynolds
• Peter O'Hearn

Seminal works

• hoare1969
• dijkstra1975
• reynolds2002
• floyd1967

Frequently asked questions

होरे ट्रिपल क्या है?

एक होरे ट्रिपल {P} C {Q} यह दावा करता है कि यदि कमांड C को निष्पादित करने से पहले पूर्वशर्त P मान्य है, तो उसके बाद उत्तरशर्त Q मान्य होती है (आंशिक शुद्धता के लिए, बशर्ते C समाप्त हो)।

सेपरेशन लॉजिक महत्वपूर्ण क्यों है?

सेपरेशन लॉजिक हीप के अलग-अलग क्षेत्रों के बारे में स्वतंत्र रूप से तर्क करने की अनुमति देता है, जिससे पॉइंटर्स और साझा परिवर्तनीय अवस्था वाले कार्यक्रमों को मॉड्यूलर तरीके से सत्यापित करना संभव हो जाता है।