होरे तर्क: Difference between revisions
(Created page with "{{short description|Rules to verify computer program correctness}} होरे लॉजिक (फ्लोयड-होरे लॉजिक या होरे निय...") |
No edit summary |
||
| Line 1: | Line 1: | ||
{{short description|Rules to verify computer program correctness}} | {{short description|Rules to verify computer program correctness}} | ||
होरे | होरे तर्क (फ्लोयड-होरे तर्क या होरे नियम के रूप में भी जाना जाता है) [[कंप्यूटर प्रोग्राम की शुद्धता]] के बारे में दृढ़ता से तर्क करने के लिए तार्किक नियमों के एक क्रम के साथ [[औपचारिक प्रणाली]] है। यह 1969 में ब्रिटिश कंप्यूटर वैज्ञानिक और [[गणितीय तर्क|तर्कशास्त्री]] [[टोनी होरे]] द्वारा प्रस्तावित किया गया था, और बाद में होरे और अन्य शोधकर्ताओं द्वारा परिष्कृत किया गया था।<ref name="hoare">{{Cite journal | ||
|last1=Hoare | |last1=Hoare | ||
|first1=C. A. R. | |first1=C. A. R. | ||
| Line 13: | Line 13: | ||
|s2cid=207726175 | |s2cid=207726175 | ||
|url=https://dl.acm.org/doi/pdf/10.1145/363235.363259 | |url=https://dl.acm.org/doi/pdf/10.1145/363235.363259 | ||
}}</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\} 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> को [[पोस्टकंडिशन|पश्च अवस्था]] नाम दिया गया है- जब पूर्व शर्त पूर्ण हो जाती है, तो कमांड निष्पादित करने से पश्च अवस्था स्थापित हो जाती है। [[विधेय तर्क]] में अभिकथन सूत्र हैं। | |||
होरे | होरे तर्क साधारण [[अनिवार्य प्रोग्रामिंग]] भाषा के सभी निर्माणों के लिए [[स्वयंसिद्ध]] और [[अनुमान नियम]] प्रदान करता है। होरे के मूल पेपर में सरल भाषा के नियमों के अलावा, होरे और कई अन्य शोधकर्ताओं द्वारा तब से अन्य भाषा निर्माणों के लिए नियम विकसित किए गए हैं। समवर्ती, प्रक्रियाओं, व्यतिक्रम, और संकेत के लिए नियम हैं। | ||
== आंशिक और [[कुल शुद्धता]] == | == आंशिक और [[कुल शुद्धता]] == | ||
मानक होरे तर्क का | मानक होरे तर्क का उपयोग करते हुए, केवल [[आंशिक शुद्धता]] ही सिद्ध की जा सकती है। कुल शुद्धता के लिए अतिरिक्त रूप से [[समाप्ति विश्लेषण|समाप्ति]] की आवश्यकता होती है, जिसे अलग से या जबकि नियम के विस्तारित संस्करण के साथ सिद्ध किया जा सकता है।<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> | |||
{{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|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.}} | ||
| Line 35: | Line 35: | ||
=== खाली कथन स्वयंसिद्ध स्कीमा === | === खाली कथन स्वयंसिद्ध स्कीमा === | ||
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|α}} and {{mvar|β}} hold, then also {{mvar|φ}} holds"; {{mvar|α}} and {{mvar|β}} are called antecedents of the rule, {{mvar|φ}} is called its succedent. A rule without antecedents is called an axiom, and written as <math>\dfrac{}{\quad\phi\quad}</math>.</ref> | 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|α}} and {{mvar|β}} hold, then also {{mvar|φ}} holds"; {{mvar|α}} and {{mvar|β}} are called antecedents of the rule, {{mvar|φ}} 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> | : <math>\dfrac{}{\{P\}\texttt{skip}\{P\}}</math> | ||
Revision as of 16:40, 12 March 2023
होरे तर्क (फ्लोयड-होरे तर्क या होरे नियम के रूप में भी जाना जाता है) कंप्यूटर प्रोग्राम की शुद्धता के बारे में दृढ़ता से तर्क करने के लिए तार्किक नियमों के एक क्रम के साथ औपचारिक प्रणाली है। यह 1969 में ब्रिटिश कंप्यूटर वैज्ञानिक और तर्कशास्त्री टोनी होरे द्वारा प्रस्तावित किया गया था, और बाद में होरे और अन्य शोधकर्ताओं द्वारा परिष्कृत किया गया था।[1] मूल विचार रॉबर्ट डब्ल्यू फ़्लॉइड के काम से उत्पन्न हुए थे, जिन्होंने फ्लोचार्ट के लिए समान प्रणाली[2] प्रकाशित की थी।
होरे त्रिगुण
होरे तर्क की केंद्रीय विशेषता होरे त्रिगुण है। त्रिगुण बताता है कि कोड के एक टुकड़े का निष्पादन कैसे गणना की स्थिति को बदलता है। होरे त्रिगुण का रूप है
जहां और अभिकथन हैं और कमांड है।[note 1] को पूर्व अवस्था और को पश्च अवस्था नाम दिया गया है- जब पूर्व शर्त पूर्ण हो जाती है, तो कमांड निष्पादित करने से पश्च अवस्था स्थापित हो जाती है। विधेय तर्क में अभिकथन सूत्र हैं।
होरे तर्क साधारण अनिवार्य प्रोग्रामिंग भाषा के सभी निर्माणों के लिए स्वयंसिद्ध और अनुमान नियम प्रदान करता है। होरे के मूल पेपर में सरल भाषा के नियमों के अलावा, होरे और कई अन्य शोधकर्ताओं द्वारा तब से अन्य भाषा निर्माणों के लिए नियम विकसित किए गए हैं। समवर्ती, प्रक्रियाओं, व्यतिक्रम, और संकेत के लिए नियम हैं।
आंशिक और कुल शुद्धता
मानक होरे तर्क का उपयोग करते हुए, केवल आंशिक शुद्धता ही सिद्ध की जा सकती है। कुल शुद्धता के लिए अतिरिक्त रूप से समाप्ति की आवश्यकता होती है, जिसे अलग से या जबकि नियम के विस्तारित संस्करण के साथ सिद्ध किया जा सकता है।[3] इस प्रकार होरे त्रिगुण का सहज ज्ञान युक्त पठन है- जब भी , के निष्पादन से पहली अवस्था को धारण करता है, तो बाद में धारण करेगा, या समाप्त नहीं होता है। बाद की स्थिति में, कोई "बाद" नहीं है, इसलिए कोई भी कथन हो सकता है। वास्तव में, यह व्यक्त करने के लिए कि समाप्त नहीं होता है, असत्य होने के लिए कोई भी चुन सकता है।
यहाँ और इस लेख के अन्य भागों में "समाप्ति" का अर्थ व्यापक अर्थों में है कि गणना अंततः समाप्त हो जाएगी, अर्थात यह अनंत छोरों की अनुपस्थिति का अर्थ है यह कार्यान्वयन सीमा के उल्लंघन (जैसे शून्य से विभाजन) की अनुपस्थिति को प्रोग्राम को समय से पहले रोकना नहीं दर्शाता है। अपने 1969 के पेपर में, होरे ने समाप्ति की एक संकीर्ण धारणा का उपयोग किया, जिसमें कार्यान्वयन सीमा के उल्लंघन की अनुपस्थिति भी सम्मिलित थी, और समाप्ति की व्यापक धारणा के लिए अपनी प्राथमिकता व्यक्त की क्योंकि यह कार्यान्वयन-स्वतंत्र होने का दावा करता है-[4]
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 “” should be interpreted “provided that the program successfully terminates, the properties of its results are described by .” 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 बाद में भी सही है।[note 2]
असाइनमेंट स्वयंसिद्ध स्कीमा
असाइनमेंट स्वयंसिद्ध बताता है कि, असाइनमेंट के बाद, कोई भी विधेय जो पहले असाइनमेंट के दाईं ओर के लिए सही था, अब वेरिएबल के लिए है। औपचारिक रूप से, चलो P एक अभिकथन हो जिसमें चर हो x मुक्त चर और बाध्य चर हैं। तब:
कहाँ कथन को दर्शाता है P जिसमें प्रत्येक फ्री वेरिएबल्स और बाउंड वेरिएबल्स हैं x अभिव्यक्ति द्वारा प्रतिस्थापन (तर्क) किया गया है E.
असाइनमेंट स्वयंसिद्ध योजना का अर्थ है कि सच्चाई के आफ्टर-असाइनमेंट सत्य के बराबर है P. इस प्रकार थे असाइनमेंट से पहले सत्य, असाइनमेंट स्वयंसिद्ध द्वारा, फिर P जिसके बाद सच होगा। इसके विपरीत थे झूठा (यानी सच) असाइनमेंट स्टेटमेंट से पहले, P बाद में गलत होना चाहिए।
मान्य ट्रिपल्स के उदाहरणों में शामिल हैं: