होरे तर्क: 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$

[1]

[2]

[note 1]

[3]

[4]

[note 2]

@@ 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 19: / Line 19: @@
 : <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> को [[पोस्टकंडिशन|पश्च अवस्था]] नाम दिया गया है- जब पूर्व अवस्था पूर्ण हो जाती है, तो कमांड निष्पादित करने से पश्च अवस्था स्थापित हो जाती है। [[विधेय तर्क]] में अभिकथन सूत्र हैं।
 होरे तर्क साधारण [[अनिवार्य प्रोग्रामिंग]] भाषा के सभी निर्माणों के लिए [[स्वयंसिद्ध]] और [[अनुमान नियम]] प्रदान करता है। होरे के मूल पेपर में सरल भाषा के नियमों के अलावा, होरे और कई अन्य शोधकर्ताओं द्वारा तब से अन्य भाषा निर्माणों के लिए नियम विकसित किए गए हैं। समवर्ती, प्रक्रियाओं, व्यतिक्रम, और संकेत के लिए नियम हैं।
@@ Line 119: / Line 119: @@
 यह नियम पूर्व अवस्था <math>P_2</math> को मजबूत करने और/या पश्च अवस्था <math>Q_2</math> को कमजोर करने की अनुमति देता है। इसका उपयोग किया जाता है उदाहरणार्थ तत्कालीन और अन्य भाग के लिए शाब्दिक रूप से समान पश्च अवस्था प्राप्त करना।
-उदाहरण के लिए, का प्रमाण
+उदाहरण के लिए, का प्रमाण है
 :<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>
 सशर्त नियम को लागू करने की आवश्यकता है, जिसे सिद्ध करने की आवश्यकता है
@@ Line 129: / Line 129: @@
 दूसरे भाग के लिए।
-हालाँकि, तत्कालीन भाग के लिए असाइनमेंट नियम को {{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> तक दृढ़ करने के लिए परिणाम नियम की आवश्यकता है।
@@ Line 152: / Line 152: @@
 :<math>\{x < 10\}   x := x + 1   \{x \leq 10 \}</math>,
-जो नियतन नियम द्वारा आसानी से प्राप्त हो जाता है। अंत में, पश्च अवस्था <math>\{\neg x <10 \wedge x\leq 10\}</math> को <math>\{x=10\}</math> में सरलीकृत किया जा सकता है।
+जो नियत कार्य नियम द्वारा आसानी से प्राप्त हो जाता है। अंत में, पश्च अवस्था <math>\{\neg x <10 \wedge x\leq 10\}</math> को <math>\{x=10\}</math> में सरलीकृत किया जा सकता है।
 एक अन्य उदाहरण के लिए, जबकि नियम का उपयोग निम्नलिखित असामान्य प्रोग्राम को औपचारिक रूप से सत्यापित करने के लिए किया जा सकता है ताकि किसी मनमानी संख्या {{mvar|a}} के सटीक वर्गमूल {{mvar|x}} की गणना की जा सके, भले ही {{mvar|x}} एक पूर्णांक चर हो और {{mvar|a}} वर्ग संख्या न हो-
@@ Line 164: / Line 164: @@
 === कुल शुद्धता के लिए जबकि नियम ===
-यदि उपरोक्त सामान्य जबकि नियम को निम्नलिखित द्वारा प्रतिस्थापित किया जाता है, तो होरे गणना का उपयोग कुल शुद्धता, अर्थात समाप्ति के साथ-साथ आंशिक शुद्धता को सिद्ध करने के लिए भी किया जा सकता है।     प्रायः, प्रोग्राम शुद्धता की विभिन्न धारणाओं को इंगित करने के लिए धनु कोष्ठकों के स्थान पर वर्ग कोष्ठकों का उपयोग किया जाता है।
+यदि उपरोक्त सामान्य जबकि नियम को निम्नलिखित द्वारा प्रतिस्थापित किया जाता है, तो होरे गणना का उपयोग कुल शुद्धता, अर्थात समाप्ति के साथ-साथ आंशिक शुद्धता को सिद्ध करने के लिए भी किया जा सकता है। प्रायः प्रोग्राम शुद्धता की विभिन्न धारणाओं को इंगित करने के लिए धनु कोष्ठकों के स्थान पर वर्ग कोष्ठकों का उपयोग किया जाता है।
 :<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>
@@ Line 181: / Line 181: @@
 जिसे इस प्रकार सिद्ध किया जा सकता है-
 :<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}} नहीं पाई जा सकती है जो रिक्त लूप निकाय से कम हो जाती है, इसलिए समाप्ति सिद्ध नहीं की जा सकती।
+:पिछले खंड के दूसरे उदाहरण के लिए, निश्चित रूप से कोई अभिव्यक्ति {{mvar|t}} नहीं पाई जा सकती है जो रिक्त लूप निकाय से कम हो जाती है, इसलिए समाप्ति सिद्ध नहीं की जा सकती हैl
 == यह भी देखें ==
 {{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

Namespaces

More

Page actions