होरे तर्क: Difference between revisions

Latest revision as of 09:52, 29 August 2023

होरे तर्क (फ्लोयड-होरे तर्क या होरे नियम के रूप में भी जाना जाता है) कंप्यूटर प्रोग्राम की शुद्धता के बारे में दृढ़ता से तर्क करने के लिए तार्किक नियमों के एक क्रम के साथ औपचारिक प्रणाली है। यह 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]\}$ यह नियम निरर्थक उदाहरणों की ओर जाता है जैसे-

\{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$ को मध्य अवस्था कहा जाता है)-^[5]

{\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$ सामान्य है और अन्य भाग भी पूरे की पश्च अवस्था है यदि ...यदि अंत कथन।^[6] तत्कालीन और अन्य भाग में, अनपेक्षित और ऋणात्मक स्थिति $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}}

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

परिणाम नियम

{\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}$ को कमजोर करने की अनुमति देता है। इसका उपयोग किया जाता है उदाहरणार्थ तत्कालीन और अन्य भाग के लिए शाब्दिक रूप से समान पश्च अवस्था प्राप्त करना।

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

\{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\}

तत्कालीन भाग के लिए, और

\{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\}

दूसरे भाग के लिए।

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

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

, जो तार्किक रूप से समतुल्य हैl

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

.

सशर्त नियम के लिए आवश्यक पूर्व अवस्था $\{-1\leq x<15\}$ को नियत कार्य नियम से $\{0\leq x<15\}$ तक दृढ़ करने के लिए परिणाम नियम की आवश्यकता है।

इसी प्रकार, दूसरे भाग के लिए, नियत कार्य नियम उत्पन्न करता है

\{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\}$ अन्य भाग के प्रवेश पर जाना जाता है, क्योंकि अन्य भाग के लिए उपयोग किए जाने वाले नियत कार्य नियम को उस जानकारी की आवश्यकता नहीं है।

जबकि नियम

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

यहाँ $P$ लूप अचर है, जिसे लूप बॉडी $S$ द्वारा संरक्षित किया जाना है। लूप समाप्त होने के बाद, यह अचर $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\}$ में सरलीकृत किया जा सकता है।

एक अन्य उदाहरण के लिए, जबकि नियम का उपयोग निम्नलिखित असामान्य प्रोग्राम को औपचारिक रूप से सत्यापित करने के लिए किया जा सकता है ताकि किसी मनमानी संख्या $a$ के सटीक वर्गमूल $x$ की गणना की जा सके, भले ही $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$ के सत्य होने के साथ, जबकि नियम लागू करने के बाद, यह सिद्ध करना शेष रह जाता है

\{{\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$ को कम नहीं कर सकता है, अर्थात नियम का आधार असत्य होगा। (यह कुल शुद्धता के लिए विभिन्न संकेतन में से एक है।)^{[note 3]}

कुल शुद्धता के प्रमाण के लिए पिछले अनुभाग के प्रथम उदाहरण को फिर से प्रारम्भ करना

[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]

परिणाम नियम द्वारा है।

पिछले खंड के दूसरे उदाहरण के लिए, निश्चित रूप से कोई अभिव्यक्ति

t

नहीं पाई जा सकती है जो रिक्त लूप निकाय से कम हो जाती है, इसलिए समाप्ति सिद्ध नहीं की जा सकती हैl

यह भी देखें

↑ Hoare originally wrote " $P\{C\}Q$ " rather than " $\{P\}C\{Q\}$ ".
↑ This article uses a natural deduction style notation for rules. For example, ${\dfrac {\alpha ,\beta }{\phi }}$ informally means "If both $α$ and $β$ hold, then also $φ$ holds"; $α$ and $β$ are called antecedents of the rule, $φ$ is called its succedent. A rule without antecedents is called an axiom, and written as ${\dfrac {}{\quad \phi \quad }}$ .
↑ Hoare's 1969 paper didn't provide a total correctness rule; cf. his discussion on p.579 (top left). For example Reynolds' textbook^[3] gives the following version of a total correctness rule: ${\dfrac {P\wedge B\rightarrow 0\leq t\quad ,\quad [P\wedge B\wedge t=z]S[P\wedge t<z]}{[P]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[P\wedge \neg B]}}$ when $z$ is an integer variable that doesn't occur free in $P$ , $B$ , $S$ , or $t$ , and $t$ is an integer expression (Reynolds' variables renamed to fit with this article's settings).

संदर्भ

↑ ^1.0 ^1.1 Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming". Communications of the ACM. 12 (10): 576–580. doi:10.1145/363235.363259. S2CID 207726175.
↑ R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.
↑ ^3.0 ^3.1 John C. Reynolds (2009). प्रोग्रामिंग भाषाओं का सिद्धांत. Cambridge University Press.) Here: Sect. 3.4, p. 64.
↑ Hoare (1969), p.578-579
↑ Huth, Michael; Ryan, Mark (2004-08-26). कंप्यूटर विज्ञान में तर्क (second ed.). CUP. p. 276. ISBN 978-0521543101.
↑ Apt, Krzysztof R.; Olderog, Ernst-Rüdiger (December 2019). "होरे के तर्क के पचास साल". Formal Aspects of Computing. 31 (6): 759. doi:10.1007/s00165-019-00501-3. S2CID 102351597.

अग्रिम पठन

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

[3] Hoare originally wrote " $P\{C\}Q$ " rather than " $\{P\}C\{Q\}$ ".

[6] This article uses a natural deduction style notation for rules. For example, ${\dfrac {\alpha ,\beta }{\phi }}$ informally means "If both $α$ and $β$ hold, then also $φ$ holds"; $α$ and $β$ are called antecedents of the rule, $φ$ is called its succedent. A rule without antecedents is called an axiom, and written as ${\dfrac {}{\quad \phi \quad }}$ .

[9] Hoare's 1969 paper didn't provide a total correctness rule; cf. his discussion on p.579 (top left). For example Reynolds' textbook^[3] gives the following version of a total correctness rule: ${\dfrac {P\wedge B\rightarrow 0\leq t\quad ,\quad [P\wedge B\wedge t=z]S[P\wedge t<z]}{[P]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[P\wedge \neg B]}}$ when $z$ is an integer variable that doesn't occur free in $P$ , $B$ , $S$ , or $t$ , and $t$ is an integer expression (Reynolds' variables renamed to fit with this article's settings).

[hoare-1] 1.0 ^1.1 Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming". Communications of the ACM. 12 (10): 576–580. doi:10.1145/363235.363259. S2CID 207726175.

[2] R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.

[Reynolds.2009-4] 3.0 ^3.1 John C. Reynolds (2009). प्रोग्रामिंग भाषाओं का सिद्धांत. Cambridge University Press.) Here: Sect. 3.4, p. 64.

[5] Hoare (1969), p.578-579

[7] Huth, Michael; Ryan, Mark (2004-08-26). कंप्यूटर विज्ञान में तर्क (second ed.). CUP. p. 276. ISBN 978-0521543101.

[8] Apt, Krzysztof R.; Olderog, Ernst-Rüdiger (December 2019). "होरे के तर्क के पचास साल". Formal Aspects of Computing. 31 (6): 759. doi:10.1007/s00165-019-00501-3. S2CID 102351597.

[1]

[2]

[note 1]

[3]

[4]

[note 2]

[5]

[6]

[note 3]

Anonymous

Search

होरे तर्क: Difference between revisions

Namespaces

More

Page actions

Latest revision as of 09:52, 29 August 2023

Contents

होरे त्रिगुण

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

नियम

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

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

रचना का नियम

सशर्त नियम

परिणाम नियम

जबकि नियम

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

यह भी देखें

टिप्पणियाँ

संदर्भ

अग्रिम पठन

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

@@ Line 1: / Line 1: @@
 {{short description|Rules to verify computer program correctness}}
-होरे लॉजिक (फ्लोयड-होरे लॉजिक या होरे नियम के रूप में भी जाना जाता है) [[कंप्यूटर प्रोग्राम की शुद्धता]] के बारे में सख्ती से तर्क करने के लिए तार्किक नियमों के एक सेट के साथ एक [[औपचारिक प्रणाली]] है। यह 1969 में ब्रिटिश कंप्यूटर वैज्ञानिक और [[गणितीय तर्क]]शास्त्री [[टोनी होरे]] द्वारा प्रस्तावित किया गया था, और बाद में होरे और अन्य शोधकर्ताओं द्वारा परिष्कृत किया गया था।<ref name="hoare">{{Cite journal
+'''होरे तर्क''' (फ्लोयड-होरे तर्क या होरे नियम के रूप में भी जाना जाता है) [[कंप्यूटर प्रोग्राम की शुद्धता]] के बारे में दृढ़ता से तर्क करने के लिए तार्किक नियमों के एक क्रम के साथ [[औपचारिक प्रणाली]] है। यह 1969 में ब्रिटिश कंप्यूटर वैज्ञानिक और [[गणितीय तर्क|तर्कशास्त्री]] [[टोनी होरे]] द्वारा प्रस्तावित किया गया था, और बाद में होरे और अन्य शोधकर्ताओं द्वारा परिष्कृत किया गया था।<ref name="hoare">{{Cite journal
   |last1=Hoare
   |first1=C. A. R.
@@ Line 13: / Line 13: @@
   |s2cid=207726175
   |url=https://dl.acm.org/doi/pdf/10.1145/363235.363259
-  }}</ref> मूल विचारों को रॉबर्ट डब्ल्यू फ्लॉयड के काम से बीजित किया गया था, जिन्होंने एक समान प्रणाली प्रकाशित की थी<ref>[[Robert W. Floyd|R. W. Floyd]]. "[https://www.cs.tau.ac.il/~nachumd/term/FloydMeaning.pdf Assigning meanings to programs.]" Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.</ref> [[प्रवाह संचित्र]] के लिए।
+  }}</ref> मूल विचार रॉबर्ट डब्ल्यू फ़्लॉइड के काम से उत्पन्न हुए थे, जिन्होंने [[प्रवाह संचित्र|फ्लोचार्ट]] के लिए समान प्रणाली<ref>[[Robert W. Floyd|R. W. Floyd]]. "[https://www.cs.tau.ac.il/~nachumd/term/FloydMeaning.pdf Assigning meanings to programs.]" Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.</ref> प्रकाशित की थी।
-== होरे ट्रिपल ==
+== होरे त्रिगुण ==
-होरे लॉजिक की केंद्रीय विशेषता होरे ट्रिपल है। एक ट्रिपल बताता है कि कैसे कोड के एक टुकड़े का निष्पादन गणना की स्थिति को बदलता है। एक होरे ट्रिपल फॉर्म का है
+होरे तर्क की केंद्रीय विशेषता होरे त्रिगुण है। त्रिगुण बताता है कि कोड के एक टुकड़े का निष्पादन कैसे गणना की स्थिति को बदलता है। होरे त्रिगुण का रूप है
 : <math>\{P\} C \{Q\}</math>
-कहाँ <math>P</math> और <math>Q</math> अभिकथन (कंप्यूटिंग) हैं और <math>C</math> एक आज्ञा है।<ref group=note>Hoare originally wrote "<math>P\{C\}Q</math>" rather than "<math>\{P\}C\{Q\}</math>".</ref> <math>P</math> पूर्व शर्त कहा जाता है और <math>Q</math> [[पोस्टकंडिशन]]: जब पूर्व शर्त पूरी हो जाती है, कमांड निष्पादित करने से पोस्टकंडिशन स्थापित होता है। अभिकथन [[विधेय तर्क]] में सूत्र हैं।
+जहां <math>P</math> और <math>Q</math> अभिकथन हैं और <math>C</math> कमांड है।<ref group="note">Hoare originally wrote "<math>P\{C\}Q</math>" rather than "<math>\{P\}C\{Q\}</math>".</ref> <math>P</math> को पूर्व अवस्था और <math>Q</math> को [[पोस्टकंडिशन|पश्च अवस्था]] नाम दिया गया है- जब पूर्व अवस्था पूर्ण हो जाती है, तो कमांड निष्पादित करने से पश्च अवस्था स्थापित हो जाती है। [[विधेय तर्क]] में अभिकथन सूत्र हैं।
-होरे लॉजिक एक साधारण [[अनिवार्य प्रोग्रामिंग]] के सभी निर्माणों के लिए [[स्वयंसिद्ध]] और [[अनुमान नियम]] प्रदान करता है। होरे के मूल पेपर में सरल भाषा के नियमों के अलावा, होरे और कई अन्य शोधकर्ताओं द्वारा तब से अन्य भाषा निर्माणों के लिए नियम विकसित किए गए हैं। Concurrency (कंप्यूटर साइंस), प्रोसीजर (कंप्यूटर साइंस), जंप (कंप्यूटर साइंस) और पॉइंटर (कंप्यूटर प्रोग्रामिंग) के लिए नियम हैं।
+होरे तर्क साधारण [[अनिवार्य प्रोग्रामिंग]] भाषा के सभी निर्माणों के लिए [[स्वयंसिद्ध]] और [[अनुमान नियम]] प्रदान करता है। होरे के मूल पेपर में सरल भाषा के नियमों के अलावा, होरे और कई अन्य शोधकर्ताओं द्वारा तब से अन्य भाषा निर्माणों के लिए नियम विकसित किए गए हैं। समवर्ती, प्रक्रियाओं, व्यतिक्रम, और संकेत के लिए नियम हैं।
 == आंशिक और [[कुल शुद्धता]] ==
-मानक होरे तर्क का प्रयोग करके, केवल [[आंशिक शुद्धता]] ही सिद्ध की जा सकती है। कुल शुद्धता के लिए अतिरिक्त रूप से [[समाप्ति विश्लेषण]] की आवश्यकता होती है, जिसे अलग से या जबकि नियम के विस्तारित संस्करण के साथ सिद्ध किया जा सकता है।<ref name="Reynolds.2009">{{cite book |title=प्रोग्रामिंग भाषाओं का सिद्धांत|author=John C. Reynolds |author-link=John C. Reynolds |publisher=Cambridge University Press |year=2009}}) Here: Sect. 3.4, p. 64.</ref> इस प्रकार एक होरे ट्रिपल का सहज ज्ञान है: जब भी <math>P</math> के निष्पादन से पहले राज्य की पकड़ <math>C</math>, तब <math>Q</math> बाद में होल्ड करेगा, या <math>C</math> समाप्त नहीं होता। बाद के मामले में, कोई बाद नहीं है, इसलिए <math>Q</math> कोई भी कथन हो सकता है। वास्तव में, कोई चुन सकता है <math>Q</math> इसे व्यक्त करने के लिए झूठा होना <math>C</math> समाप्त नहीं होता।
+मानक होरे तर्क का उपयोग करते हुए, केवल [[आंशिक शुद्धता]] ही सिद्ध की जा सकती है। कुल शुद्धता के लिए अतिरिक्त रूप से [[समाप्ति विश्लेषण|समाप्ति]] की आवश्यकता होती है, जिसे अलग से या जबकि नियम के विस्तारित संस्करण के साथ सिद्ध किया जा सकता है।<ref name="Reynolds.2009">{{cite book |title=प्रोग्रामिंग भाषाओं का सिद्धांत|author=John C. Reynolds |author-link=John C. Reynolds |publisher=Cambridge University Press |year=2009}}) Here: Sect. 3.4, p. 64.</ref> इस प्रकार होरे त्रिगुण का सहज ज्ञान युक्त पठन है- जब भी <math>P</math>, <math>C</math> के निष्पादन से पहली अवस्था को धारण करता है, तो <math>Q</math> बाद में धारण करेगा, या <math>C</math> समाप्त नहीं होता है। बाद की स्थिति में, कोई "बाद" नहीं है, इसलिए <math>Q</math> कोई भी कथन हो सकता है। वास्तव में, यह व्यक्त करने के लिए कि <math>C</math> समाप्त नहीं होता है, असत्य होने के लिए कोई भी <math>Q</math> चुन सकता है।
- यहाँ और इस लेख के बाकी हिस्सों में समाप्ति का अर्थ व्यापक अर्थों में है कि गणना अंततः समाप्त हो जाएगी, अर्थात यह अनंत छोरों की अनुपस्थिति को दर्शाता है; यह कार्यान्वयन सीमा के उल्लंघन (जैसे शून्य से विभाजन) की अनुपस्थिति को कार्यक्रम को समय से पहले रोकना नहीं दर्शाता है। अपने 1969 के पेपर में, होरे ने समाप्ति की एक संकीर्ण धारणा का उपयोग किया, जिसमें कार्यान्वयन सीमा के उल्लंघन की अनुपस्थिति भी शामिल थी, और समाप्ति की व्यापक धारणा के लिए अपनी प्राथमिकता व्यक्त की क्योंकि यह कार्यान्वयन-स्वतंत्र होने का दावा करता है:<ref>Hoare (1969), p.578-579</ref>
+यहाँ और इस लेख के अन्य भागों में "समाप्ति" का अर्थ व्यापक अर्थों में है कि गणना अंततः समाप्त हो जाएगी, अर्थात यह अनंत छोरों की अनुपस्थिति का अर्थ है यह कार्यान्वयन सीमा के उल्लंघन (जैसे शून्य से विभाजन) की अनुपस्थिति को प्रोग्राम को समय से पहले रोकना नहीं दर्शाता है। अपने 1969 के पेपर में, होरे ने समाप्ति की एक संकीर्ण धारणा का उपयोग किया, जिसमें कार्यान्वयन सीमा के उल्लंघन की अनुपस्थिति भी सम्मिलित थी, और समाप्ति की व्यापक धारणा के लिए अपनी प्राथमिकता व्यक्त की क्योंकि यह कार्यान्वयन-स्वतंत्र होने का दावा करता है-<ref>Hoare (1969), p.578-579</ref>
-{{quote|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 “<math>P\{Q\}R</math>” should be interpreted “provided that the program successfully terminates, the properties of its results are described by <math>R</math>.” 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.}}
+{{quote|ऊपर उद्धृत सिद्धांतों और नियमों में एक और कमी यह है कि वे इस बात के प्रमाण के लिए कोई आधार नहीं देते हैं कि प्रोग्राम सफलतापूर्वक समाप्त हो गया है। समाप्त करने में विफलता अनंत लूप के कारण हो सकती है या यह कार्यान्वयन-परिभाषित सीमा के उल्लंघन के कारण हो सकता है, उदाहरण के लिए, संख्यात्मक संकार्य की सीमा, स्टोरेज का आकार, या ऑपरेटिंग सिस्टम की समय सीमा। इस प्रकार अंकन “<math>P\{Q\}R</math>” की व्याख्या की जानी चाहिए "बशर्ते कि कार्यक्रम सफलतापूर्वक समाप्त हो जाए, इसके परिणामों के गुणों को <math>R</math> द्वारा वर्णित किया गया है।" स्वयंसिद्धों को अनुकूलित करना काफी आसान है ताकि उन्हें गैर-समाप्ति प्रोग्रामों के "परिणामों" की भविष्यवाणी करने के लिए उपयोग नहीं किया जा सके लेकिन स्वयंसिद्धों का वास्तविक उपयोग अब कई कार्यान्वयन-निर्भर विशेषताओं के ज्ञान पर निर्भर करेगा, उदाहरण के लिए, कंप्यूटर का आकार और गति, संख्याओं की सीमा और अतिप्रवाह तकनीक का विकल्प। अनंत लूप से बचने के प्रमाण के अलावा, किसी प्रोग्राम की "सशर्त" शुद्धता को सिद्ध करना और चेतावनी देने के लिए कार्यान्वयन पर भरोसा करना सम्भवतः बेहतर है, यदि इसे कार्यान्वयन सीमा के उल्लंघन के परिणामस्वरूप प्रोग्राम के निष्पादन को त्यागना पड़ा हो।}}
 == नियम ==
-=== खाली कथन स्वयंसिद्ध स्कीमा ===
+=== रिक्त कथन स्वयंसिद्ध स्कीमा ===
-NOP (कोड) नियम का दावा है कि {{mono|skip}} कथन कार्यक्रम की स्थिति को नहीं बदलता है, इस प्रकार जो कुछ भी पहले सत्य है {{mono|skip}} बाद में भी सही है।<ref group=note>This article uses a [[natural deduction]] style notation for rules. For example, <math>\dfrac{\alpha,\beta}{\phi}</math> informally means "If both {{mvar|&alpha;}} and {{mvar|&beta;}} hold, then also {{mvar|&phi;}} holds"; {{mvar|&alpha;}} and {{mvar|&beta;}} are called antecedents of the rule, {{mvar|&phi;}} is called its succedent. A rule without antecedents is called an axiom, and written as <math>\dfrac{}{\quad\phi\quad}</math>.</ref>
+रिक्त कथन नियम यह दावा करता है कि स्किप कथन प्रोग्राम की स्थिति को नहीं बदलता है, इस प्रकार स्किप से पहले जो भी सही है वह बाद में भी सही रहेगा।<ref group="note">This article uses a [[natural deduction]] style notation for rules. For example, <math>\dfrac{\alpha,\beta}{\phi}</math> informally means "If both {{mvar|&alpha;}} and {{mvar|&beta;}} hold, then also {{mvar|&phi;}} holds"; {{mvar|&alpha;}} and {{mvar|&beta;}} are called antecedents of the rule, {{mvar|&phi;}} is called its succedent. A rule without antecedents is called an axiom, and written as <math>\dfrac{}{\quad\phi\quad}</math>.</ref>
 : <math>\dfrac{}{\{P\}\texttt{skip}\{P\}}</math>
+=== नियत कार्य स्वयंसिद्ध स्कीमा ===
+नियत कार्य स्वयंसिद्ध कहता है कि, नियत कार्य के बाद, कोई भी विधेय जो पहले नियत कार्य के दाईं ओर के लिए सही था, अब चर के लिए मान्य है। औपचारिक रूप से, मान लीजिए कि {{mvar|P}} अभिकथन है जिसमें चर {{mvar|x}} [[मुक्त चर और बाध्य चर|मुक्त]] है। तब-
-=== असाइनमेंट स्वयंसिद्ध स्कीमा ===
-असाइनमेंट स्वयंसिद्ध बताता है कि, असाइनमेंट के बाद, कोई भी विधेय जो पहले असाइनमेंट के दाईं ओर के लिए सही था, अब वेरिएबल के लिए है। औपचारिक रूप से, चलो {{mvar|P}} एक अभिकथन हो जिसमें चर हो {{mvar|x}} [[मुक्त चर और बाध्य चर]] हैं। तब:
-<!-- NB: This version of the axiom schema is sound. Do not exchange the precondition with the postcondition. -->
 : <math>\dfrac{}{\{P[E/x]\} x := E \{P\}}</math>
-कहाँ <math>P[E/x]</math> कथन को दर्शाता है {{mvar|P}} जिसमें प्रत्येक फ्री वेरिएबल्स और बाउंड वेरिएबल्स हैं {{mvar|x}} अभिव्यक्ति द्वारा [[प्रतिस्थापन (तर्क)]] किया गया है {{mvar|E}}.
+जहां <math>P[E/x]</math> अभिकथन {{mvar|P}} को दर्शाता है जिसमें {{mvar|x}} की प्रत्येक मुक्त घटना को अभिव्यक्ति {{mvar|E}} द्वारा [[प्रतिस्थापन (तर्क)|प्रतिस्थापित]] किया गया है।
-असाइनमेंट स्वयंसिद्ध योजना का अर्थ है कि सच्चाई <math>P[E/x]</math> के आफ्टर-असाइनमेंट सत्य के बराबर है {{mvar|P}}. इस प्रकार थे <math>P[E/x]</math> असाइनमेंट से पहले सत्य, असाइनमेंट स्वयंसिद्ध द्वारा, फिर {{mvar|P}} जिसके बाद सच होगा। इसके विपरीत थे <math>P[E/x]</math> झूठा (यानी <math>\neg P[E/x]</math> सच) असाइनमेंट स्टेटमेंट से पहले, {{mvar|P}} बाद में गलत होना चाहिए।
+नियत कार्य स्वयंसिद्ध योजना का अर्थ है कि <math>P[E/x]</math> का सत्य {{mvar|P}} के बाद के नियत कार्य सत्य के बराबर है। इस प्रकार <math>P[E/x]</math> नियत कार्य से पहले सत्य थे, नियत कार्य स्वयंसिद्ध द्वारा, फिर {{mvar|P}} जिसके बाद सत्य होगा। इसके विपरीत, <math>P[E/x]</math> असत्य (अर्थात <math>\neg P[E/x]</math> सत्य) नियत कार्य कथन से पहले थे, {{mvar|P}} को बाद में असत्य होना चाहिए।
-मान्य ट्रिपल्स के उदाहरणों में शामिल हैं:
+मान्य त्रिगुण के उदाहरणों में सम्मिलित हैं-
 :*<math>\{ x+1 = 43 \}   y := x + 1   \{ y = 43 \}</math>
 :*<math>\{ x + 1 \leq N \}  x := x  + 1  \{ x \leq N \}</math>
-सभी पूर्व शर्त जो एक्सप्रेशन द्वारा संशोधित नहीं की जाती हैं उन्हें पोस्टकंडिशन में ले जाया जा सकता है। पहले उदाहरण में, असाइन करना <math>y:=x+1</math> इस तथ्य को नहीं बदलता है <math>x+1=43</math>, इसलिए दोनों कथन पश्च शर्त में प्रकट हो सकते हैं। औपचारिक रूप से, यह परिणाम स्वयंसिद्ध स्कीमा को लागू करके प्राप्त किया जाता है {{mvar|P}} प्राणी (<math>y=43</math> और <math>x+1=43</math>), कौन सी पैदावार <math>P[(x+1)/y]</math> प्राणी (<math>x+1=43</math> और <math>x+1=43</math>), जिसे बदले में दी गई पूर्व शर्त में सरलीकृत किया जा सकता है <math>x+1=43</math>.
+सभी पूर्व अवस्था जो अभिव्यक्ति द्वारा संशोधित नहीं की जाती हैं उन्हें पश्च अवस्था पर ले जाया जा सकता है। प्रथम उदाहरण में, <math>y:=x+1</math> निर्दिष्ट करने से यह तथ्य नहीं बदलता है कि <math>x+1=43</math> है, इसलिए दोनों कथन पश्च अवस्था में दिखाई दे सकते हैं। औपचारिक रूप से, यह परिणाम {{mvar|P}} के साथ स्वयंसिद्ध स्कीमा को लागू करके प्राप्त किया जाता है (<math>y=43</math> और <math>x+1=43</math>), जो <math>P[(x+1)/y]</math> को (<math>x+1=43</math> और <math>x+1=43</math>) की उपज देता है, जिसे बदले में दिए गए पूर्व अवस्था <math>x+1=43</math> के लिए सरलीकृत किया जा सकता है। नियत कार्य स्वयंसिद्ध योजना यह कहने के बराबर है कि पूर्व अवस्था को खोजने के लिए, पहले पश्च-अवस्था को लें और नियत कार्य के बाएं हाथ की सभी घटनाओं को नियत कार्य के दाईं ओर के साथ बदल दें। सावधान रहें कि सोचने के इस गलत तरीके से पालन करके यह पीछे की ओर करने की कोशिश न करें- <math>\{P\} x:=E \{P[E/x]\}</math> यह नियम निरर्थक उदाहरणों की ओर जाता है जैसे-
-असाइनमेंट स्वयंसिद्ध योजना यह कहने के बराबर है कि पूर्व शर्त को खोजने के लिए, पहले पोस्ट-कंडीशन लें और असाइनमेंट के बायीं ओर की सभी घटनाओं को असाइनमेंट के दायीं ओर से बदलें। इस गलत तरीके से सोचने के द्वारा इसे पीछे की ओर करने की कोशिश न करने के लिए सावधान रहें: <math>\{P\} x:=E \{P[E/x]\}</math>;
-यह नियम निरर्थक उदाहरणों की ओर ले जाता है जैसे:
 : <math>\{ x = 5 \} x := 3 \{ 3 = 5 \}</math>
-पहली नज़र में आकर्षक लगने वाला एक और गलत नियम है <math>\{P\} x:=E \{P \wedge x=E\}</math>; यह निरर्थक उदाहरणों की ओर ले जाता है जैसे:
+पहली नज़र में लुभाने वाली एक और गलत नियम <math>\{P\} x:=E \{P \wedge x=E\}</math> है, यह निरर्थक उदाहरणों की ओर जाता है जैसे-
 : <math>\{ x = 5 \}   x := x + 1   \{ x = 5 \wedge x = x + 1 \}</math>
-जबकि एक दी गई पोस्टकंडिशन {{mvar|P}} विशिष्ट रूप से पूर्व शर्त निर्धारित करता है <math>P[E/x]</math>, इसका उलट सत्य नहीं है। उदाहरण के लिए:
+जबकि दिए गए पश्च अवस्था {{mvar|P}} विशिष्ट रूप से पूर्व अवस्था <math>P[E/x]</math> को निर्धारित करता है, इसका विपरीत सत्य नहीं है। उदाहरण के लिए-
 :*<math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}   x := y \cdot y   \{ 0 \leq x \wedge x \leq 9 \}</math>,
 :*<math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}   x := y \cdot y   \{ 0 \leq x \wedge y\cdot y \leq 9 \}</math>,
 :*<math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}   x := y \cdot y   \{ 0 \leq y\cdot y \wedge x \leq 9 \} </math>, और
 :*<math>\{ 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 \}</math>
-असाइनमेंट स्वयंसिद्ध योजना के मान्य उदाहरण हैं।
+नियत कार्य स्वयंसिद्ध योजना के मान्य उदाहरण हैं।
-होरे द्वारा प्रस्तावित असाइनमेंट स्वयंसिद्ध तब लागू नहीं होता है जब एक से अधिक नाम एक ही संग्रहित मूल्य को संदर्भित कर सकते हैं। उदाहरण के लिए,
+होरे द्वारा प्रस्तावित नियत कार्य स्वयंसिद्ध तब लागू नहीं होता है जब एक से अधिक नाम एक ही संग्रहीत मान को संदर्भित कर सकते हैं। उदाहरण के लिए,
 : <math>\{ y = 3 \}   x := 2   \{ y = 3 \}</math>
-गलत है अगर {{mvar|x}} और {{mvar|y}} एक ही चर ([[अलियासिंग (कंप्यूटिंग)]]) का संदर्भ लें, हालांकि यह असाइनमेंट स्वयंसिद्ध योजना (दोनों के साथ) का एक उचित उदाहरण है <math>\{P\}</math> और <math>\{P[2/x]\}</math> प्राणी <math>\{y=3\}</math>).
+यदि {{mvar|x}} और {{mvar|y}} एक ही चर ([[अलियासिंग (कंप्यूटिंग)|उपनाम]]) को संदर्भित करते हैं, तो यह गलत है, हालांकि यह नियत कार्य स्वयंसिद्ध योजना (<math>\{P\}</math>और <math>\{P[2/x]\}</math> दोनों के साथ <math>\{y=3\}</math>) का उचित उदाहरण है।
 === रचना का नियम ===
@@ Line 97: / Line 90: @@
 |}
 |}
-होरे की रचना का नियम क्रमिक रूप से निष्पादित कार्यक्रमों पर लागू होता है {{mvar|S}} और {{mvar|T}}, कहाँ {{mvar|S}} से पहले निष्पादित करता है {{mvar|T}} और लिखा है <math>S;T</math> ({{mvar|Q}} को मध्य स्थिति कहा जाता है):<ref>{{cite book|first1=Michael|last1=Huth|first2=Mark|last2=Ryan|publisher=CUP|url=http://www.cs.bham.ac.uk/research/projects/lics/|isbn=978-0521543101|title=कंप्यूटर विज्ञान में तर्क|edition=second |pages= 276|date=2004-08-26}}</ref>
+होरे की रचना का नियम क्रमिक रूप से निष्पादित प्रोग्रामों {{mvar|S}} और {{mvar|T}} पर लागू होता है, जहां {{mvar|S}} {{mvar|T}} से पहले निष्पादित करता है और <math>S;T</math> को लिखा जाता है ({{mvar|Q}} को मध्य अवस्था कहा जाता है)-<ref>{{cite book|first1=Michael|last1=Huth|first2=Mark|last2=Ryan|publisher=CUP|url=http://www.cs.bham.ac.uk/research/projects/lics/|isbn=978-0521543101|title=कंप्यूटर विज्ञान में तर्क|edition=second |pages= 276|date=2004-08-26}}</ref>
 :<math>\dfrac{\{P\} S \{Q\}\quad,\quad   \{Q\} T \{R\}}{\{P\} S;T \{R\}}</math>
-उदाहरण के लिए, असाइनमेंट स्वयंसिद्ध के निम्नलिखित दो उदाहरणों पर विचार करें:
+उदाहरण के लिए, नियत कार्य स्वयंसिद्ध के निम्नलिखित दो उदाहरणों पर विचार करें-
 :<math>\{ x + 1 = 43 \}   y := x + 1   \{ y = 43 \}</math>
@@ Line 105: / Line 98: @@
 :<math>\{ y = 43 \}   z := y   \{ z = 43 \}</math>
-अनुक्रमण नियम से, एक निष्कर्ष निकलता है:
+अनुक्रमण नियम द्वारा, एक निष्कर्ष निकाला गया-
 :<math>\{ x + 1 = 43 \}   y := x + 1; z := y   \{ z = 43 \}</math>
-एक और उदाहरण सही बॉक्स में दिखाया गया है।
+एक अन्य उदाहरण सही बॉक्स में दिखाया गया है।
 === सशर्त नियम ===
 :<math>\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\}}</math>
-सशर्त नियम कहता है कि एक पोस्टकंडीशन {{mvar|Q}} के लिए समान {{mono|then}} और {{mono|else}} भाग भी पूर्ण की एक पश्च शर्त है {{mono|if...endif}} कथन।<ref>{{cite journal |last1=Apt |first1=Krzysztof R. |last2=Olderog |first2=Ernst-Rüdiger |title=होरे के तर्क के पचास साल|journal=Formal Aspects of Computing |date=December 2019 |volume=31 |issue=6 |page=759 |doi=10.1007/s00165-019-00501-3|s2cid=102351597 |url=https://ir.cwi.nl/pub/29146 }}</ref>
+सशर्त नियम में कहा गया है कि पश्च अवस्था {{mvar|Q}} सामान्य है और अन्य भाग भी पूरे की पश्च अवस्था है यदि ...यदि अंत कथन।<ref>{{cite journal |last1=Apt |first1=Krzysztof R. |last2=Olderog |first2=Ernst-Rüdiger |title=होरे के तर्क के पचास साल|journal=Formal Aspects of Computing |date=December 2019 |volume=31 |issue=6 |page=759 |doi=10.1007/s00165-019-00501-3|s2cid=102351597 |url=https://ir.cwi.nl/pub/29146 }}</ref> तत्कालीन और अन्य भाग में, अनपेक्षित और ऋणात्मक स्थिति {{mvar|B}} को क्रमशः पूर्व अवस्था {{mvar|P}} में जोड़ा जा सकता है। स्थिति, {{mvar|B}}, के दुष्प्रभाव नहीं होने चाहिए। अगले भाग में उदाहरण दिया गया है।
-में {{mono|then}} और यह {{mono|else}} हिस्सा, अस्वीकृत और नकारात्मक स्थिति {{mvar|B}} पूर्व शर्त में जोड़ा जा सकता है {{mvar|P}}, क्रमश।
-स्थिति, {{mvar|B}}, के दुष्प्रभाव नहीं होने चाहिए।
-#परिणाम_नियम में एक उदाहरण दिया गया है।
-यह नियम होरे के मूल प्रकाशन में निहित नहीं था।<ref name="hoare"/>हालांकि, एक बयान के बाद से
+यह नियम होरे के मूल प्रकाशन में निहित नहीं था।<ref name="hoare"/> हालांकि, कथन के बाद से
 :<math>\texttt{if}\ B\ \texttt{then}\ S\ \texttt{else}\ T\ \texttt{endif}</math>
-वन-टाइम लूप निर्माण के समान प्रभाव है
+एक-बार के लूप निर्माण के समान प्रभाव होते है
 :<math>\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}</math>
-सशर्त नियम अन्य होरे नियमों से प्राप्त किया जा सकता है।
+सशर्त नियम अन्य होरे नियमों से व्युत्पन्न किया जा सकता है। इसी तरह, अन्य व्युत्पन्न प्रोग्राम निर्माणों के लिए नियम, जैसे लूप के लिए, लूप तक करें, स्विच करें, ब्रेक करें, जारी रखें को होरे के मूल पेपर से नियमों में परिवर्तन करके कम किया जा सकता है।
-इसी तरह, अन्य व्युत्पन्न प्रोग्राम निर्माण के लिए नियम, जैसे {{mono|for}} कुंडली, {{mono|do...until}} कुंडली, {{mono|switch}}, {{mono|break}}, {{mono|continue}} को होरे के मूल पेपर से नियमों में परिवर्तन करके कम किया जा सकता है।
 === परिणाम नियम ===
 :<math>\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\}}</math>
-यह नियम पूर्व शर्त को मजबूत करने की अनुमति देता है <math>P_2</math> और/या स्थिति को कमजोर करने के लिए <math>Q_2</math>.
+यह नियम पूर्व अवस्था <math>P_2</math> को मजबूत करने और/या पश्च अवस्था <math>Q_2</math> को कमजोर करने की अनुमति देता है। इसका उपयोग किया जाता है उदाहरणार्थ तत्कालीन और अन्य भाग के लिए शाब्दिक रूप से समान पश्च अवस्था प्राप्त करना।
-इसका उपयोग किया जाता है उदा। के लिए वस्तुतः समान पोस्टकंडिशन प्राप्त करने के लिए {{mono|then}} और यह {{mono|else}} भाग।
-उदाहरण के लिए, का प्रमाण
+उदाहरण के लिए, का प्रमाण है
 :<math>\{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 \}</math>
-सशर्त नियम लागू करने की आवश्यकता है, जो बदले में सिद्ध करने की आवश्यकता है
+सशर्त नियम को लागू करने की आवश्यकता है, जिसे सिद्ध करने की आवश्यकता है
 :<math>\{0 \leq x \leq 15 \wedge x < 15 \}   x:=x+1   \{ 0 \leq x \leq 15 \}</math>,   या सरलीकृत
 :<math>\{0 \leq x < 15 \}   x:=x+1   \{0 \leq x \leq 15 \}</math>
-के लिए {{mono|then}} भाग, और
+तत्कालीन भाग के लिए, और
 :<math>\{0 \leq x \leq 15 \wedge x \geq 15\}   x:=0   \{0 \leq x \leq 15\}</math>,   या सरलीकृत
 :<math>\{x=15\}   x:=0   \{0 \leq x \leq 15 \}</math>
-के लिए {{mono|else}} भाग।
+दूसरे भाग के लिए।
-हालाँकि, के लिए असाइनमेंट नियम {{mono|then}} भाग को चुनने की आवश्यकता है {{mvar|P}} जैसा <math>0\leq x \leq 15</math>; नियम आवेदन इसलिए पैदावार
+हालाँकि, तत्कालीन भाग के लिए असाइनमेंट नियम को {{mvar|P}} को <math>0\leq x \leq 15</math> के रूप में चुनने की आवश्यकता है नियम लागू होता है इसलिए उत्पन्न होती हैl
-:<math>\{0 \leq x+1 \leq 15\}   x:=x+1   \{0 \leq x \leq 15\}</math>,   जो तार्किक रूप से समतुल्य है
+:<math>\{0 \leq x+1 \leq 15\}   x:=x+1   \{0 \leq x \leq 15\}</math>,  जो तार्किक रूप से समतुल्य हैl
 :<math>\{-1 \leq x < 15\}   x:=x+1   \{0 \leq x \leq 15\}</math>.
-पूर्व शर्त को मजबूत करने के लिए परिणाम नियम की आवश्यकता है <math>\{-1 \leq x < 15\}</math> असाइनमेंट नियम से प्राप्त करने के लिए <math>\{0 \leq x < 15\}</math> सशर्त नियम के लिए आवश्यक है।
+सशर्त नियम के लिए आवश्यक पूर्व अवस्था <math>\{-1 \leq x < 15\}</math> को नियत कार्य नियम से <math>\{0 \leq x < 15\}</math> तक दृढ़ करने के लिए परिणाम नियम की आवश्यकता है।
-इसी प्रकार, के लिए {{mono|else}} भाग, असाइनमेंट नियम पैदावार
+इसी प्रकार, दूसरे भाग के लिए, नियत कार्य नियम उत्पन्न करता है
 :<math>\{0 \leq 0 \leq 15\}   x:=0   \{0 \leq x \leq 15\}</math>,   या समकक्ष
 :<math>\{\texttt{true}\}   x:=0   \{0 \leq x \leq 15\}</math>,
-इसलिए परिणाम नियम के साथ लागू किया जाना है <math>P_1</math> और <math>P_2</math> प्राणी <math>\{x=15\}</math> और <math>\{\texttt{true}\}</math>, क्रमशः, फिर से पूर्व शर्त को मजबूत करने के लिए। अनौपचारिक रूप से, परिणाम नियम का प्रभाव उसे भूल जाना है <math>\{x=15\}</math> के प्रवेश पर जाना जाता है {{mono|else}} भाग, चूंकि असाइनमेंट नियम के लिए उपयोग किया जाता है {{mono|else}} भाग को उस जानकारी की आवश्यकता नहीं है।
+इसलिए परिणाम नियम को <math>P_1</math> और <math>P_2</math> क्रमशः <math>\{x=15\}</math> और <math>\{\texttt{true}\}</math> के साथ लागू करना होगा, पूर्व अवस्था को फिर से दृढ़ करने के लिए।
+अनौपचारिक रूप से, परिणाम नियम का प्रभाव "भूल जाना" है कि <math>\{x=15\}</math> अन्य भाग के प्रवेश पर जाना जाता है, क्योंकि अन्य भाग के लिए उपयोग किए जाने वाले नियत कार्य नियम को उस जानकारी की आवश्यकता नहीं है।
 === जबकि नियम ===
 :<math>\dfrac{\{P \wedge B\} S \{P\}}{\{P\} \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done} \{\neg B \wedge P\}}</math>
-यहाँ {{mvar|P}} [[ पाश अपरिवर्तनीय ]] है, जिसे लूप बॉडी द्वारा संरक्षित किया जाना है {{mvar|S}}.
+यहाँ {{mvar|P}} [[ पाश अपरिवर्तनीय |लूप अचर]] है, जिसे लूप बॉडी {{mvar|S}} द्वारा संरक्षित किया जाना है। लूप समाप्त होने के बाद, यह अचर {{mvar|P}} अभी भी धारण करता है, और इसके अलावा <math>\neg B</math> ने लूप को समाप्त करने का कारण बना दिया होगा। जैसा कि सशर्त नियम में है, {{mvar|B}} के दुष्प्रभाव नहीं होने चाहिए।
-लूप समाप्त होने के बाद, यह invariant {{mvar|P}} अभी भी धारण करता है, और इसके अलावा <math>\neg B</math> लूप को समाप्त करने का कारण होना चाहिए।
-सशर्त नियम के रूप में, {{mvar|B}} के दुष्प्रभाव नहीं होने चाहिए।
 उदाहरण के लिए, का प्रमाण
 :<math>\{x \leq 10\} \texttt{while}\ x<10\ \texttt{do}\ x:=x+1\ \texttt{done} \{\neg x < 10 \wedge x \leq 10\}</math>
-जबकि नियम को सिद्ध करने की आवश्यकता है
+जबकि नियम द्वारा सिद्ध करने की आवश्यकता है
 :<math>\{x \leq 10 \wedge x < 10\}   x := x + 1   \{x \leq 10 \}</math>,   या सरलीकृत
 :<math>\{x < 10\}   x := x + 1   \{x \leq 10 \}</math>,
-जो कार्य नियम से आसानी से प्राप्त हो जाता है।
-अंत में, पोस्टकंडिशन <math>\{\neg x <10 \wedge x\leq 10\}</math> करने के लिए सरलीकृत किया जा सकता है <math>\{x=10\}</math>.
-एक अन्य उदाहरण के लिए, सटीक वर्गमूल की गणना करने के लिए निम्न अजीब प्रोग्राम को औपचारिक रूप से सत्यापित करने के लिए नियम का उपयोग किया जा सकता है {{mvar|x}} एक मनमानी संख्या का {{mvar|a}}-भले ही {{mvar|x}} एक पूर्णांक चर है और {{mvar|a}} वर्ग संख्या नहीं है:
+जो नियत कार्य नियम द्वारा आसानी से प्राप्त हो जाता है। अंत में, पश्च अवस्था <math>\{\neg x <10 \wedge x\leq 10\}</math> को <math>\{x=10\}</math> में सरलीकृत किया जा सकता है।
+एक अन्य उदाहरण के लिए, जबकि नियम का उपयोग निम्नलिखित असामान्य प्रोग्राम को औपचारिक रूप से सत्यापित करने के लिए किया जा सकता है ताकि किसी मनमानी संख्या {{mvar|a}} के सटीक वर्गमूल {{mvar|x}} की गणना की जा सके, भले ही {{mvar|x}} एक पूर्णांक चर हो और {{mvar|a}} वर्ग संख्या न हो-
 :<math>\{\texttt{true}\}   \texttt{while}\ x\cdot x \neq a\ \texttt{do}\ \texttt{skip}\ \texttt{done}   \{x \cdot x = a \wedge \texttt{true}\}</math>
-के साथ समय नियम लागू करने के बाद {{mvar|P}} प्राणी {{mono|true}}, यह साबित करना बाकी है
+{{mvar|P}} के सत्य होने के साथ, जबकि नियम लागू करने के बाद, यह सिद्ध करना शेष रह जाता है
 :<math>\{\texttt{true} \wedge x\cdot x \neq a\}   \texttt{skip}   \{\texttt{true}\}</math>,
 जो स्किप नियम और परिणाम नियम से अनुसरण करता है।
-वास्तव में, अजीब कार्यक्रम आंशिक रूप से सही है: यदि यह समाप्त हो गया है, तो यह निश्चित है {{mvar|x}} में (संयोग से) का मान होना चाहिए {{mvar|a}} का वर्गमूल।
+वास्तव में, असामान्य प्रोग्राम आंशिक रूप से सही है- यदि यह समाप्त हो गया, तो यह निश्चित है कि {{mvar|x}} में (संयोग से) {{mvar|a}} के वर्गमूल का मान होना चाहिए। अन्य सभी स्थितियों में, यह समाप्त नहीं होगा इसलिए यह पूरी तरह से सही नहीं है।
-अन्य सभी मामलों में, यह समाप्त नहीं होगा; इसलिए यह पूरी तरह से सही नहीं है।
-=== जबकि कुल शुद्धता के लिए नियम ===
+=== कुल शुद्धता के लिए जबकि नियम ===
-यदि #जबकि_नियम को निम्नलिखित द्वारा प्रतिस्थापित किया जाता है, तो होरे कैलकुलस का उपयोग कुल शुद्धता, यानी समाप्ति के साथ-साथ आंशिक शुद्धता को साबित करने के लिए भी किया जा सकता है। आमतौर पर, प्रोग्राम शुद्धता की विभिन्न धारणाओं को इंगित करने के लिए घुंघराले ब्रेसिज़ के बजाय स्क्वायर ब्रैकेट का उपयोग किया जाता है।
+यदि उपरोक्त सामान्य जबकि नियम को निम्नलिखित द्वारा प्रतिस्थापित किया जाता है, तो होरे गणना का उपयोग कुल शुद्धता, अर्थात समाप्ति के साथ-साथ आंशिक शुद्धता को सिद्ध करने के लिए भी किया जा सकता है। प्रायः प्रोग्राम शुद्धता की विभिन्न धारणाओं को इंगित करने के लिए धनु कोष्ठकों के स्थान पर वर्ग कोष्ठकों का उपयोग किया जाता है।
 :<math>\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]}</math>
-इस नियम में, लूप इनवेरिएंट को बनाए रखने के अलावा, एक एक्सप्रेशन के माध्यम से [[ समाप्ति प्रमाण ]] भी साबित होता है {{mvar|t}}, जिसे [[लूप वेरिएंट]] कहा जाता है, जिसका मूल्य एक [[अच्छी तरह से स्थापित संबंध]] के संबंध में सख्ती से घटता है {{mvar|<}} कुछ डोमेन सेट पर {{mvar|D}} प्रत्येक पुनरावृत्ति के दौरान। तब से {{mvar|<}} के सदस्यों की एक सख्ती से घटती [[श्रृंखला (आदेश सिद्धांत)]] अच्छी तरह से स्थापित है {{mvar|D}} की केवल सीमित लंबाई हो सकती है, इसलिए {{mvar|t}} हमेशा के लिए घटता नहीं रह सकता। (उदाहरण के लिए, सामान्य क्रम {{mvar|<}} सकारात्मक [[पूर्णांक]]ों पर अच्छी तरह से स्थापित है <math>\mathbb{N}</math>, लेकिन न तो पूर्णांकों पर <math>\mathbb{Z}</math> न ही धनात्मक वास्तविक संख्याओं पर <math>\mathbb{R}^+</math>; ये सभी सेट गणितीय अर्थ में हैं, कंप्यूटिंग अर्थ में नहीं, ये सभी विशेष रूप से अनंत हैं।)
+इस नियम में, लूप अचर को बनाए रखने के अलावा, एक अभिव्यक्ति {{mvar|t}} के माध्यम से [[ समाप्ति प्रमाण |समापन]] भी सिद्ध होता है, जिसे [[लूप वेरिएंट|लूप चर]] कहा जाता है, जिसका मान प्रत्येक पुनरावृत्ति के दौरान कुछ क्षेत्र क्रम {{mvar|D}} पर [[अच्छी तरह से स्थापित संबंध]] {{mvar|<}} के संबंध में दृढ़ता से घटता है। चूंकि {{mvar|<}} अच्छी तरह से स्थापित है, {{mvar|D}} के सदस्यों की दृढ़ता से घटती [[श्रृंखला (आदेश सिद्धांत)|श्रृंखला]] में केवल परिमित लंबाई हो सकती है, इसलिए {{mvar|t}} सदैव के लिए घटता नहीं रह सकता है। (उदाहरण के लिए, सामान्य क्रम {{mvar|<}} धनात्मक [[पूर्णांक]] <math>\mathbb{N}</math> पर अच्छी तरह से स्थापित है, लेकिन न तो पूर्णांक <math>\mathbb{Z}</math> पर और न ही धनात्मक वास्तविक संख्याओं <math>\mathbb{R}^+</math>पर ये सभी क्रम गणितीय अर्थ में हैं, कंप्यूटिंग अर्थ में नहीं, ये सभी विशेष रूप से अनंत हैं।)
-लूप इनवेरिएंट को देखते हुए {{mvar|P}}, स्थिति {{mvar|B}} का अर्थ होना चाहिए {{mvar|t}} का [[न्यूनतम तत्व]] नहीं है {{mvar|D}}, अन्यथा शरीर के लिए {{mvar|S}} कम नहीं हो सका {{mvar|t}} आगे कोई भी, यानी नियम का आधार झूठा होगा। (यह कुल शुद्धता के लिए विभिन्न नोटेशनों में से एक है।)
+लूप अचर {{mvar|P}} को देखते हुए, स्थिति {{mvar|B}} को यह बताना चाहिए कि {{mvar|t}}, {{mvar|D}} का [[न्यूनतम तत्व]] नहीं है, अन्यथा निकाय {{mvar|S}} आगे {{mvar|t}} को कम नहीं कर सकता है, अर्थात नियम का आधार असत्य होगा। (यह कुल शुद्धता के लिए विभिन्न संकेतन में से एक है।){{#tag:ref| Hoare's 1969 paper didn't provide a total correctness rule; cf. his discussion on p.579 (top left). For example Reynolds' textbook<ref name="Reynolds.2009"/>  gives the following version of a total correctness rule: <math>\dfrac{P \wedge B \rightarrow 0\leq t\quad ,\quad   [P \wedge B \wedge t=z] S [P \wedge t<z]}{[P] \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done} [P \wedge \neg B]}</math>  when {{mvar|z}} is an integer variable that doesn't occur free in {{mvar|P}}, {{mvar|B}}, {{mvar|S}}, or {{mvar|t}}, and {{mvar|t}} is an integer expression (Reynolds' variables renamed to fit with this article's settings). |group=note}}
-{{#tag:ref| Hoare's 1969 paper didn't provide a total correctness rule; cf. his discussion on p.579 (top left). For example Reynolds' textbook<ref name="Reynolds.2009"/>  gives the following version of a total correctness rule: <math>\dfrac{P \wedge B \rightarrow 0\leq t\quad ,\quad   [P \wedge B \wedge t=z] S [P \wedge t<z]}{[P] \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done} [P \wedge \neg B]}</math>  when {{mvar|z}} is an integer variable that doesn't occur free in {{mvar|P}}, {{mvar|B}}, {{mvar|S}}, or {{mvar|t}}, and {{mvar|t}} is an integer expression (Reynolds' variables renamed to fit with this article's settings). |group=note}}
-के पूर्ण-शुद्धता प्रमाण के लिए, #जबकि_नियम के पहले उदाहरण को फिर से शुरू करना
+कुल शुद्धता के प्रमाण के लिए पिछले अनुभाग के प्रथम उदाहरण को फिर से प्रारम्भ करना
 :<math>[x \leq 10]\texttt{while}\ x < 10\ \texttt{do}\ x:=x+1\ \texttt{done} [\neg x < 10 \wedge x \leq 10]</math>
-कुल शुद्धता के लिए जबकि नियम लागू किया जा सकता है उदा। {{mvar|D}} सामान्य क्रम और अभिव्यक्ति के साथ गैर-ऋणात्मक पूर्णांक हैं {{mvar|t}} प्राणी  <math>10 - x</math>, जिसे बाद में साबित करने की आवश्यकता होती है
+कुल शुद्धता के लिए जबकि नियम लागू किया जा सकता है उदाहरण- {{mvar|D}} सामान्य क्रम के साथ गैर-ऋणात्मक पूर्णांक है, और अभिव्यक्ति {{mvar|t}}, <math>10 - x</math> है, जिसे बाद में सिद्ध करने की आवश्यकता होती है
 :<math>[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]</math>
-अनौपचारिक रूप से बोलते हुए, हमें यह साबित करना होगा कि दूरी <math>10-x</math> प्रत्येक पाश चक्र में घटता है, जबकि यह हमेशा गैर-ऋणात्मक रहता है; यह प्रक्रिया सीमित चक्रों तक ही चल सकती है।
+अनौपचारिक रूप से, हमें यह सिद्ध करना होगा कि प्रत्येक लूप चक्र में <math>10-x</math> की दूरी घट जाती है, जबकि यह सदैव गैर-ऋणात्मक रहती है, यह प्रक्रिया केवल सीमित संख्या में चक्रों के लिए ही चल सकती है।
 पिछले प्रमाण लक्ष्य को सरल बनाया जा सकता है
 :<math>[x < 10 \wedge 10-x = z]   x:=x+1   [x \leq 10 \wedge 10-x < z]</math>,
-जिसे इस प्रकार सिद्ध किया जा सकता है:
+जिसे इस प्रकार सिद्ध किया जा सकता है-
-:<math>[x+1 \leq 10 \wedge 10-x-1 < z]   x:=x+1   [x \leq 10 \wedge 10-x < z]</math> असाइनमेंट नियम द्वारा प्राप्त किया जाता है, और
+:<math>[x+1 \leq 10 \wedge 10-x-1 < z]   x:=x+1   [x \leq 10 \wedge 10-x < z]</math> नियत कार्य नियम द्वारा प्राप्त किया जाता है, और
-:<math>[x+1 \leq 10 \wedge 10-x-1 < z]</math> तक मजबूत किया जा सकता है <math> [x < 10 \wedge 10-x = z]</math> परिणाम नियम द्वारा।
+:<math>[x+1 \leq 10 \wedge 10-x-1 < z]</math> को दृढ़ किया जा सकता है <math> [x < 10 \wedge 10-x = z]</math> परिणाम नियम द्वारा है।
+:पिछले खंड के दूसरे उदाहरण के लिए, निश्चित रूप से कोई अभिव्यक्ति {{mvar|t}} नहीं पाई जा सकती है जो रिक्त लूप निकाय से कम हो जाती है, इसलिए समाप्ति सिद्ध नहीं की जा सकती हैl
-#जबकि_नियम के दूसरे उदाहरण के लिए, निश्चित रूप से कोई अभिव्यक्ति नहीं {{mvar|t}} पाया जा सकता है कि खाली लूप बॉडी द्वारा घटाया गया है, इसलिए समाप्ति सिद्ध नहीं की जा सकती।
 == यह भी देखें ==
 {{columns-list|colwidth=20em|
-* [[Assertion (software development)]]
+* [[अभिकथन (सॉफ्टवेयर विकास)]]
-* [[Denotational semantics]]
+* [[सांकेतिक अर्थ विज्ञान]]
-* [[Design by contract]]
+* [[अनुबंध द्वारा डिजाइन]]
-* [[Dynamic logic (modal logic)|Dynamic logic]]
+* [[गतिशील तर्क (modal logic)|गतिशील तर्क]]
-* [[Formal verification]]
+* [[औपचारिक सत्यापन]]
-* [[Loop invariant]]
+* [[लूप अपरिवर्तनीय]]
-* [[Predicate transformer semantics]]
+* [[विधेय परिवर्तक अर्थ विज्ञान]]
-* [[Static program analysis]]
+* [[स्थैतिक प्रोग्राम विश्लेषण]]
 }}
 == टिप्पणियाँ ==
 {{reflist|group=note}}
 == संदर्भ ==
 {{Reflist|30em}}
 == अग्रिम पठन ==
 * Robert D. Tennent. ''[http://www.cs.queensu.ca/home/specsoft/ Specifying Software]'' (a textbook that includes an introduction to Hoare logic, written in 2002) {{ISBN|0-521-00401-2}}
 == बाहरी संबंध==
 * [https://web.archive.org/web/20071117054808/http://www.key-project.org/download/hoare/ 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.
 * [http://j-algo.binaervarianz.de/index.php?language=en j-Algo-modul Hoare calculus] &mdash; A visualisation of the Hoare calculus in the algorithm visualisation program j-Algo
-{{Program analysis}}
-{{Authority control}}[[Category: कंप्यूटिंग में 1969]] [[Category: कार्यक्रम तर्क]] [[Category: स्थैतिक कार्यक्रम विश्लेषण]]
-[[Category: Machine Translated Page]]
 [[Category:Created On 02/03/2023]]
+[[Category:Lua-based templates]]
+[[Category:Machine Translated Page]]
+[[Category:Multi-column templates]]
+[[Category:Pages using div col with small parameter]]
+[[Category:Pages with script errors]]
+[[Category:Short description with empty Wikidata description]]
+[[Category:Templates Vigyan Ready]]
+[[Category:Templates that add a tracking category]]
+[[Category:Templates that generate short descriptions]]
+[[Category:Templates using TemplateData]]
+[[Category:Templates using under-protected Lua modules]]
+[[Category:Wikipedia fully protected templates|Div col]]
+[[Category:कंप्यूटिंग में 1969]]
+[[Category:कार्यक्रम तर्क]]
+[[Category:स्थैतिक कार्यक्रम विश्लेषण]]

Anonymous

Search

होरे तर्क: Difference between revisions

Latest revision as of 09:52, 29 August 2023

होरे त्रिगुण

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

नियम

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

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

रचना का नियम

सशर्त नियम

परिणाम नियम

जबकि नियम

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

यह भी देखें

टिप्पणियाँ

संदर्भ

अग्रिम पठन

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories