होरे तर्क

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

होरे त्रिगुण

होरे तर्क की केंद्रीय विशेषता होरे त्रिगुण है। त्रिगुण बताता है कि कोड के एक टुकड़े का निष्पादन कैसे गणना की स्थिति को बदलता है। होरे त्रिगुण का रूप है

\{P\}C\{Q\}

जहां $P$ और $Q$ अभिकथन हैं और $C$ कमांड है।^{[note 1]} $P$ को पूर्व अवस्था और $Q$ को पश्च अवस्था नाम दिया गया है- जब पूर्व शर्त पूर्ण हो जाती है, तो कमांड निष्पादित करने से पश्च अवस्था स्थापित हो जाती है। विधेय तर्क में अभिकथन सूत्र हैं।

होरे तर्क साधारण अनिवार्य प्रोग्रामिंग भाषा के सभी निर्माणों के लिए स्वयंसिद्ध और अनुमान नियम प्रदान करता है। होरे के मूल पेपर में सरल भाषा के नियमों के अलावा, होरे और कई अन्य शोधकर्ताओं द्वारा तब से अन्य भाषा निर्माणों के लिए नियम विकसित किए गए हैं। समवर्ती, प्रक्रियाओं, व्यतिक्रम, और संकेत के लिए नियम हैं।

आंशिक और कुल शुद्धता

मानक होरे तर्क का उपयोग करते हुए, केवल आंशिक शुद्धता ही सिद्ध की जा सकती है। कुल शुद्धता के लिए अतिरिक्त रूप से समाप्ति की आवश्यकता होती है, जिसे अलग से या जबकि नियम के विस्तारित संस्करण के साथ सिद्ध किया जा सकता है।^[3] इस प्रकार होरे त्रिगुण का सहज ज्ञान युक्त पठन है- जब भी $P$ , $C$ के निष्पादन से पहली अवस्था को धारण करता है, तो $Q$ बाद में धारण करेगा, या $C$ समाप्त नहीं होता है। बाद की स्थिति में, कोई "बाद" नहीं है, इसलिए $Q$ कोई भी कथन हो सकता है। वास्तव में, यह व्यक्त करने के लिए कि $C$ समाप्त नहीं होता है, असत्य होने के लिए कोई भी $Q$ चुन सकता है।

यहाँ और इस लेख के अन्य भागों में "समाप्ति" का अर्थ व्यापक अर्थों में है कि गणना अंततः समाप्त हो जाएगी, अर्थात यह अनंत छोरों की अनुपस्थिति का अर्थ है यह कार्यान्वयन सीमा के उल्लंघन (जैसे शून्य से विभाजन) की अनुपस्थिति को प्रोग्राम को समय से पहले रोकना नहीं दर्शाता है। अपने 1969 के पेपर में, होरे ने समाप्ति की एक संकीर्ण धारणा का उपयोग किया, जिसमें कार्यान्वयन सीमा के उल्लंघन की अनुपस्थिति भी सम्मिलित थी, और समाप्ति की व्यापक धारणा के लिए अपनी प्राथमिकता व्यक्त की क्योंकि यह कार्यान्वयन-स्वतंत्र होने का दावा करता है-^[4]

ऊपर उद्धृत सिद्धांतों और नियमों में एक और कमी यह है कि वे इस बात के प्रमाण के लिए कोई आधार नहीं देते हैं कि प्रोग्राम सफलतापूर्वक समाप्त हो गया है। समाप्त करने में विफलता अनंत लूप के कारण हो सकती है या यह कार्यान्वयन-परिभाषित सीमा के उल्लंघन के कारण हो सकता है, उदाहरण के लिए, संख्यात्मक संकार्य की सीमा, स्टोरेज का आकार, या ऑपरेटिंग सिस्टम की समय सीमा। इस प्रकार अंकन “ $P\{Q\}R$ ” की व्याख्या की जानी चाहिए "बशर्ते कि कार्यक्रम सफलतापूर्वक समाप्त हो जाए, इसके परिणामों के गुणों को $R$ द्वारा वर्णित किया गया है।" स्वयंसिद्धों को अनुकूलित करना काफी आसान है ताकि उन्हें गैर-समाप्ति प्रोग्रामों के "परिणामों" की भविष्यवाणी करने के लिए उपयोग नहीं किया जा सके लेकिन स्वयंसिद्धों का वास्तविक उपयोग अब कई कार्यान्वयन-निर्भर विशेषताओं के ज्ञान पर निर्भर करेगा, उदाहरण के लिए, कंप्यूटर का आकार और गति, संख्याओं की सीमा और अतिप्रवाह तकनीक का विकल्प। अनंत लूप से बचने के प्रमाण के अलावा, किसी प्रोग्राम की "सशर्त" शुद्धता को सिद्ध करना और चेतावनी देने के लिए कार्यान्वयन पर भरोसा करना सम्भवतः बेहतर है, यदि इसे कार्यान्वयन सीमा के उल्लंघन के परिणामस्वरूप प्रोग्राम के निष्पादन को त्यागना पड़ा हो।

नियम

रिक्त कथन स्वयंसिद्ध स्कीमा

रिक्त कथन नियम यह दावा करता है कि स्किप कथन प्रोग्राम की स्थिति को नहीं बदलता है, इस प्रकार स्किप से पहले जो भी सही है वह बाद में भी सही रहेगा।^{[note 2]}

{\dfrac {}{\{P\}{\texttt {skip}}\{P\}}}

नियत कार्य स्वयंसिद्ध स्कीमा

नियत कार्य स्वयंसिद्ध कहता है कि, नियत कार्य के बाद, कोई भी विधेय जो पहले नियत कार्य के दाईं ओर के लिए सही था, अब चर के लिए मान्य है। औपचारिक रूप से, मान लीजिए कि $P$ अभिकथन है जिसमें चर $x$ मुक्त है। तब-

{\dfrac {}{\{P[E/x]\}x:=E\{P\}}}

जहां $P[E/x]$ अभिकथन $P$ को दर्शाता है जिसमें $x$ की प्रत्येक मुक्त घटना को अभिव्यक्ति $E$ द्वारा प्रतिस्थापित किया गया है।

नियत कार्य स्वयंसिद्ध योजना का अर्थ है कि $P[E/x]$ का सत्य $P$ के बाद के नियत कार्य सत्य के बराबर है। इस प्रकार $P[E/x]$ नियत कार्य से पहले सत्य थे, नियत कार्य स्वयंसिद्ध द्वारा, फिर $P$ जिसके बाद सत्य होगा। इसके विपरीत, $P[E/x]$ असत्य (अर्थात $\neg P[E/x]$ सत्य) नियत कार्य कथन से पहले थे, $P$ को बाद में असत्य होना चाहिए।

मान्य त्रिगुण के उदाहरणों में सम्मिलित हैं-

$\{x+1=43\}y:=x+1\{y=43\}$
$\{x+1\leq N\}x:=x+1\{x\leq N\}$

सभी पूर्व अवस्था जो अभिव्यक्ति द्वारा संशोधित नहीं की जाती हैं उन्हें पश्च अवस्था पर ले जाया जा सकता है। प्रथम उदाहरण में, $y:=x+1$ निर्दिष्ट करने से यह तथ्य नहीं बदलता है कि $x+1=43$ है, इसलिए दोनों कथन पश्च अवस्था में दिखाई दे सकते हैं। औपचारिक रूप से, यह परिणाम $P$ के साथ स्वयंसिद्ध स्कीमा को लागू करके प्राप्त किया जाता है ( $y=43$ और $x+1=43$ ), जो $P[(x+1)/y]$ को ( $x+1=43$ और $x+1=43$ ) की उपज देता है, जिसे बदले में दिए गए पूर्व अवस्था $x+1=43$ के लिए सरलीकृत किया जा सकता है। नियत कार्य स्वयंसिद्ध योजना यह कहने के बराबर है कि पूर्व अवस्था को खोजने के लिए, पहले पश्च-अवस्था को लें और नियत कार्य के बाएं हाथ की सभी घटनाओं को नियत कार्य के दाईं ओर के साथ बदल दें। सावधान रहें कि सोचने के इस गलत तरीके से पालन करके यह पीछे की ओर करने की कोशिश न करें- $\{P\}x:=E\{P[E/x]\}$ यह नियम निरर्थक उदाहरणों की ओर जाता है जैसे-