होरे तर्क

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

होरे त्रिगुण

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

$\{P\}C\{Q\}$

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

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

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

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

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

Another deficiency in the axioms and rules quoted above is that they give no basis for a proof that a program successfully terminates. Failure to terminate may be due to an infinite loop; or it may be due to violation of an implementation-defined limit, for example, the range of numeric operands, the size of storage, or an operating system time limit. Thus the notation “$P\{Q\}R$” should be interpreted “provided that the program successfully terminates, the properties of its results are described by $R$.” It is fairly easy to adapt the axioms so that they cannot be used to predict the “results” of nonterminating programs; but the actual use of the axioms would now depend on knowledge of many implementation-dependent features, for example, the size and speed of the computer, the range of numbers, and the choice of overflow technique. Apart from proofs of the avoidance of infinite loops, it is probably better to prove the “conditional” correctness of a program and rely on an implementation to give a warning if it has had to abandon execution of the program as a result of violation of an implementation limit.

नियम

खाली कथन स्वयंसिद्ध स्कीमा

NOP (कोड) नियम का दावा है कि skip कथन कार्यक्रम की स्थिति को नहीं बदलता है, इस प्रकार जो कुछ भी पहले सत्य है skip बाद में भी सही है।

${\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]\}$; यह नियम निरर्थक उदाहरणों की ओर ले जाता है जैसे:

$\{x=5\}x:=3\{3=5\}$

पहली नज़र में आकर्षक लगने वाला एक और गलत नियम है $\{P\}x:=E\{P\wedge x=E\}$; यह निरर्थक उदाहरणों की ओर ले जाता है जैसे:

$\{x=5\}x:=x+1\{x=5\wedge x=x+1\}$

जबकि एक दी गई पोस्टकंडिशन P विशिष्ट रूप से पूर्व शर्त निर्धारित करता है $P[E/x]$, इसका उलट सत्य नहीं है। उदाहरण के लिए:

• $\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge x\leq 9\}$,
• $\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge y\cdot y\leq 9\}$,
• $\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge x\leq 9\}$, और
• $\{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge y\cdot y\leq 9\}$

असाइनमेंट स्वयंसिद्ध योजना के मान्य उदाहरण हैं।

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

$\{y=3\}x:=2\{y=3\}$

गलत है अगर x और y एक ही चर (अलियासिंग (कंप्यूटिंग)) का संदर्भ लें, हालांकि यह असाइनमेंट स्वयंसिद्ध योजना (दोनों के साथ) का एक उचित उदाहरण है $\{P\}$ और $\{P[2/x]\}$ प्राणी $\{y=3\}$).

रचना का नियम

Verifying swap-code without auxiliary variables

The three statements below (line 2, 4, 6) exchange the values of the variables a and b, without needing an auxiliary variable. In the verification proof, the initial value of a and b is denoted by the constant A and B, respectively. The proof is best read backwards, starting from line 7; for example, line 5 is obtained from line 7 by replacing a (target expression in line 6) by $a-b$ (source expression in line 6). Some arithmetical simplifications are used tacitly, viz. $a-(a-b)=b$ (line 5→3), and $a+b-b=a$ (line 3→1). Nr Code Assertions 1:       $\{a=A\wedge b=B\}$ 2: $a:=a+b;$       3: $\{a-b=A\wedge b=B\}$ 4: $b:=a-b;$ 5: $\{b=A\wedge a-b=B\}$ 6: $a:=a-b$ 7: $\{b=A\wedge a=B\}$

होरे की रचना का नियम क्रमिक रूप से निष्पादित कार्यक्रमों पर लागू होता है S और T, कहाँ S से पहले निष्पादित करता है T और लिखा है $S;T$ (Q को मध्य स्थिति कहा जाता है):

${\dfrac {\{P\}S\{Q\}\quad ,\quad \{Q\}T\{R\}}{\{P\}S;T\{R\}}}$

उदाहरण के लिए, असाइनमेंट स्वयंसिद्ध के निम्नलिखित दो उदाहरणों पर विचार करें:

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

और

$\{y=43\}z:=y\{z=43\}$

अनुक्रमण नियम से, एक निष्कर्ष निकलता है:

$\{x+1=43\}y:=x+1;z:=y\{z=43\}$

एक और उदाहरण सही बॉक्स में दिखाया गया है।

सशर्त नियम

${\dfrac {\{B\wedge P\}S\{Q\}\quad ,\quad \{\neg B\wedge P\}T\{Q\}}{\{P\}{\texttt {if}}\ B\ {\texttt {then}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}\{Q\}}}$

सशर्त नियम कहता है कि एक पोस्टकंडीशन Q के लिए समान then और else भाग भी पूर्ण की एक पश्च शर्त है if...endif कथन। में then और यह else हिस्सा, अस्वीकृत और नकारात्मक स्थिति B पूर्व शर्त में जोड़ा जा सकता है P, क्रमश। स्थिति, B, के दुष्प्रभाव नहीं होने चाहिए।

1. परिणाम_नियम में एक उदाहरण दिया गया है।

यह नियम होरे के मूल प्रकाशन में निहित नहीं था।हालांकि, एक बयान के बाद से

${\texttt {if}}\ B\ {\texttt {then}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}$

वन-टाइम लूप निर्माण के समान प्रभाव है

${\texttt {bool}}\ b:={\texttt {true}};{\texttt {while}}\ B\wedge b\ {\texttt {do}}\ S;b:={\texttt {false}}\ {\texttt {done}};b:={\texttt {true}};{\texttt {while}}\ \neg B\wedge b\ {\texttt {do}}\ T;b:={\texttt {false}}\ {\texttt {done}}$

सशर्त नियम अन्य होरे नियमों से प्राप्त किया जा सकता है। इसी तरह, अन्य व्युत्पन्न प्रोग्राम निर्माण के लिए नियम, जैसे for कुंडली, do...until कुंडली, switch, break, continue को होरे के मूल पेपर से नियमों में परिवर्तन करके कम किया जा सकता है।

परिणाम नियम

${\dfrac {P_{1}\rightarrow P_{2}\quad ,\quad \{P_{2}\}S\{Q_{2}\}\quad ,\quad Q_{2}\rightarrow Q_{1}}{\{P_{1}\}S\{Q_{1}\}}}$

यह नियम पूर्व शर्त को मजबूत करने की अनुमति देता है $P_{2}$ और/या स्थिति को कमजोर करने के लिए $Q_{2}$. इसका उपयोग किया जाता है उदा। के लिए वस्तुतः समान पोस्टकंडिशन प्राप्त करने के लिए then और यह else भाग।

उदाहरण के लिए, का प्रमाण

$\{0\leq x\leq 15\}{\texttt {if}}\ x<15\ {\texttt {then}}\ x:=x+1\ {\texttt {else}}\ x:=0\ {\texttt {endif}}\{0\leq x\leq 15\}$

सशर्त नियम लागू करने की आवश्यकता है, जो बदले में सिद्ध करने की आवश्यकता है

$\{0\leq x\leq 15\wedge x<15\}x:=x+1\{0\leq x\leq 15\}$,   या सरलीकृत

$\{0\leq x<15\}x:=x+1\{0\leq x\leq 15\}$

के लिए then भाग, और

$\{0\leq x\leq 15\wedge x\geq 15\}x:=0\{0\leq x\leq 15\}$,   या सरलीकृत

$\{x=15\}x:=0\{0\leq x\leq 15\}$

के लिए else भाग।

हालाँकि, के लिए असाइनमेंट नियम then भाग को चुनने की आवश्यकता है P जैसा $0\leq x\leq 15$; नियम आवेदन इसलिए पैदावार

$\{0\leq x+1\leq 15\}x:=x+1\{0\leq x\leq 15\}$,   जो तार्किक रूप से समतुल्य है

$\{-1\leq x<15\}x:=x+1\{0\leq x\leq 15\}$.

पूर्व शर्त को मजबूत करने के लिए परिणाम नियम की आवश्यकता है $\{-1\leq x<15\}$ असाइनमेंट नियम से प्राप्त करने के लिए $\{0\leq x<15\}$ सशर्त नियम के लिए आवश्यक है।

इसी प्रकार, के लिए else भाग, असाइनमेंट नियम पैदावार

$\{0\leq 0\leq 15\}x:=0\{0\leq x\leq 15\}$,   या समकक्ष

$\{{\texttt {true}}\}x:=0\{0\leq x\leq 15\}$,

इसलिए परिणाम नियम के साथ लागू किया जाना है $P_{1}$ और $P_{2}$ प्राणी $\{x=15\}$ और $\{{\texttt {true}}\}$, क्रमशः, फिर से पूर्व शर्त को मजबूत करने के लिए। अनौपचारिक रूप से, परिणाम नियम का प्रभाव उसे भूल जाना है $\{x=15\}$ के प्रवेश पर जाना जाता है else भाग, चूंकि असाइनमेंट नियम के लिए उपयोग किया जाता है else भाग को उस जानकारी की आवश्यकता नहीं है।

जबकि नियम

${\dfrac {\{P\wedge B\}S\{P\}}{\{P\}{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}\{\neg B\wedge P\}}}$

यहाँ P पाश अपरिवर्तनीय है, जिसे लूप बॉडी द्वारा संरक्षित किया जाना है S. लूप समाप्त होने के बाद, यह invariant P अभी भी धारण करता है, और इसके अलावा $\neg B$ लूप को समाप्त करने का कारण होना चाहिए। सशर्त नियम के रूप में, B के दुष्प्रभाव नहीं होने चाहिए।

उदाहरण के लिए, का प्रमाण

$\{x\leq 10\}{\texttt {while}}\ x<10\ {\texttt {do}}\ x:=x+1\ {\texttt {done}}\{\neg x<10\wedge x\leq 10\}$

जबकि नियम को सिद्ध करने की आवश्यकता है

$\{x\leq 10\wedge x<10\}x:=x+1\{x\leq 10\}$,   या सरलीकृत

$\{x<10\}x:=x+1\{x\leq 10\}$,

जो कार्य नियम से आसानी से प्राप्त हो जाता है। अंत में, पोस्टकंडिशन $\{\neg x<10\wedge x\leq 10\}$ करने के लिए सरलीकृत किया जा सकता है $\{x=10\}$.

एक अन्य उदाहरण के लिए, सटीक वर्गमूल की गणना करने के लिए निम्न अजीब प्रोग्राम को औपचारिक रूप से सत्यापित करने के लिए नियम का उपयोग किया जा सकता है x एक मनमानी संख्या का a-भले ही x एक पूर्णांक चर है और a वर्ग संख्या नहीं है:

$\{{\texttt {true}}\}{\texttt {while}}\ x\cdot x\neq a\ {\texttt {do}}\ {\texttt {skip}}\ {\texttt {done}}\{x\cdot x=a\wedge {\texttt {true}}\}$

के साथ समय नियम लागू करने के बाद P प्राणी true, यह साबित करना बाकी है

$\{{\texttt {true}}\wedge x\cdot x\neq a\}{\texttt {skip}}\{{\texttt {true}}\}$,

जो स्किप नियम और परिणाम नियम से अनुसरण करता है।

वास्तव में, अजीब कार्यक्रम आंशिक रूप से सही है: यदि यह समाप्त हो गया है, तो यह निश्चित है x में (संयोग से) का मान होना चाहिए a का वर्गमूल। अन्य सभी मामलों में, यह समाप्त नहीं होगा; इसलिए यह पूरी तरह से सही नहीं है।

जबकि कुल शुद्धता के लिए नियम

यदि #जबकि_नियम को निम्नलिखित द्वारा प्रतिस्थापित किया जाता है, तो होरे कैलकुलस का उपयोग कुल शुद्धता, यानी समाप्ति के साथ-साथ आंशिक शुद्धता को साबित करने के लिए भी किया जा सकता है। आमतौर पर, प्रोग्राम शुद्धता की विभिन्न धारणाओं को इंगित करने के लिए घुंघराले ब्रेसिज़ के बजाय स्क्वायर ब्रैकेट का उपयोग किया जाता है।

${\dfrac {<\ {\text{is a well-founded ordering on the set}}\ D\quad ,\quad [P\wedge B\wedge t\in D\wedge t=z]S[P\wedge t\in D\wedge t<z]}{[P\wedge t\in D]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[\neg B\wedge P\wedge t\in D]}}$

इस नियम में, लूप इनवेरिएंट को बनाए रखने के अलावा, एक एक्सप्रेशन के माध्यम से समाप्ति प्रमाण भी साबित होता है t, जिसे लूप वेरिएंट कहा जाता है, जिसका मूल्य एक अच्छी तरह से स्थापित संबंध के संबंध में सख्ती से घटता है < कुछ डोमेन सेट पर D प्रत्येक पुनरावृत्ति के दौरान। तब से < के सदस्यों की एक सख्ती से घटती श्रृंखला (आदेश सिद्धांत) अच्छी तरह से स्थापित है D की केवल सीमित लंबाई हो सकती है, इसलिए t हमेशा के लिए घटता नहीं रह सकता। (उदाहरण के लिए, सामान्य क्रम < सकारात्मक पूर्णांकों पर अच्छी तरह से स्थापित है $\mathbb {N}$, लेकिन न तो पूर्णांकों पर $\mathbb {Z}$ न ही धनात्मक वास्तविक संख्याओं पर $\mathbb {R} ^{+}$; ये सभी सेट गणितीय अर्थ में हैं, कंप्यूटिंग अर्थ में नहीं, ये सभी विशेष रूप से अनंत हैं।)

लूप इनवेरिएंट को देखते हुए P, स्थिति B का अर्थ होना चाहिए t का न्यूनतम तत्व नहीं है D, अन्यथा शरीर के लिए S कम नहीं हो सका t आगे कोई भी, यानी नियम का आधार झूठा होगा। (यह कुल शुद्धता के लिए विभिन्न नोटेशनों में से एक है।)

के पूर्ण-शुद्धता प्रमाण के लिए, #जबकि_नियम के पहले उदाहरण को फिर से शुरू करना

$[x\leq 10]{\texttt {while}}\ x<10\ {\texttt {do}}\ x:=x+1\ {\texttt {done}}[\neg x<10\wedge x\leq 10]$

कुल शुद्धता के लिए जबकि नियम लागू किया जा सकता है उदा। D सामान्य क्रम और अभिव्यक्ति के साथ गैर-ऋणात्मक पूर्णांक हैं t प्राणी $10-x$, जिसे बाद में साबित करने की आवश्यकता होती है

$[x\leq 10\wedge x<10\wedge 10-x\geq 0\wedge 10-x=z]x:=x+1[x\leq 10\wedge 10-x\geq 0\wedge 10-x<z]$

अनौपचारिक रूप से बोलते हुए, हमें यह साबित करना होगा कि दूरी $10-x$ प्रत्येक पाश चक्र में घटता है, जबकि यह हमेशा गैर-ऋणात्मक रहता है; यह प्रक्रिया सीमित चक्रों तक ही चल सकती है।

पिछले प्रमाण लक्ष्य को सरल बनाया जा सकता है

$[x<10\wedge 10-x=z]x:=x+1[x\leq 10\wedge 10-x<z]$,

जिसे इस प्रकार सिद्ध किया जा सकता है:

$[x+1\leq 10\wedge 10-x-1<z]x:=x+1[x\leq 10\wedge 10-x<z]$ असाइनमेंट नियम द्वारा प्राप्त किया जाता है, और

$[x+1\leq 10\wedge 10-x-1<z]$ तक मजबूत किया जा सकता है $[x<10\wedge 10-x=z]$ परिणाम नियम द्वारा।

1. जबकि_नियम के दूसरे उदाहरण के लिए, निश्चित रूप से कोई अभिव्यक्ति नहीं t पाया जा सकता है कि खाली लूप बॉडी द्वारा घटाया गया है, इसलिए समाप्ति सिद्ध नहीं की जा सकती।

यह भी देखें

• Assertion (software development)
• Denotational semantics
• Design by contract
• Dynamic logic
• Formal verification
• Loop invariant
• Predicate transformer semantics
• Static program analysis

अग्रिम पठन

• Robert D. Tennent. Specifying Software (a textbook that includes an introduction to Hoare logic, written in 2002) ISBN 0-521-00401-2

बाहरी संबंध

• KeY-Hoare is a semi-automatic verification system built on top of the KeY theorem prover. It features a Hoare calculus for a simple while language.
• j-Algo-modul Hoare calculus — A visualisation of the Hoare calculus in the algorithm visualisation program j-Algo