होरे तर्क: Difference between revisions
(→नियम) |
|||
| Line 152: | Line 152: | ||
:<math>\{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|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> | :<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}} के सत्य होने के साथ, जबकि नियम लागू करने के बाद, यह सिद्ध करना शेष रह जाता है | ||
:<math>\{\texttt{true} \wedge x\cdot x \neq a\} \texttt{skip} \{\texttt{true}\}</math>, | :<math>\{\texttt{true} \wedge x\cdot x \neq a\} \texttt{skip} \{\texttt{true}\}</math>, | ||
जो स्किप नियम और परिणाम नियम से अनुसरण करता है। | जो स्किप नियम और परिणाम नियम से अनुसरण करता है। | ||
वास्तव में, | वास्तव में, असामान्य प्रोग्राम आंशिक रूप से सही है- यदि यह समाप्त हो गया, तो यह निश्चित है कि {{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> | :<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|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}} को कम नहीं कर सकता है, अर्थात नियम का आधार असत्य होगा। (यह कुल शुद्धता के लिए विभिन्न संकेतन में से एक है।){{#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> | :<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> है, जिसे बाद में सिद्ध करने की आवश्यकता होती है | ||
:<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>[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>[x < 10 \wedge 10-x = z] x:=x+1 [x \leq 10 \wedge 10-x < z]</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+1 \leq 10 \wedge 10-x-1 < z]</math> को दृढ़ किया जा सकता है<math> [x < 10 \wedge 10-x = z]</math> परिणाम नियम द्वारा। | ||
:पिछले खंड के दूसरे उदाहरण के लिए, निश्चित रूप से कोई अभिव्यक्ति {{mvar|t}} नहीं पाई जा सकती है जो रिक्त लूप निकाय से कम हो जाती है, इसलिए समाप्ति सिद्ध नहीं की जा सकती। | |||
== यह भी देखें == | == यह भी देखें == | ||
Revision as of 02:17, 13 March 2023
होरे तर्क (फ्लोयड-होरे तर्क या होरे नियम के रूप में भी जाना जाता है) कंप्यूटर प्रोग्राम की शुद्धता के बारे में दृढ़ता से तर्क करने के लिए तार्किक नियमों के एक क्रम के साथ औपचारिक प्रणाली है। यह 1969 में ब्रिटिश कंप्यूटर वैज्ञानिक और तर्कशास्त्री टोनी होरे द्वारा प्रस्तावित किया गया था, और बाद में होरे और अन्य शोधकर्ताओं द्वारा परिष्कृत किया गया था।[1] मूल विचार रॉबर्ट डब्ल्यू फ़्लॉइड के काम से उत्पन्न हुए थे, जिन्होंने फ्लोचार्ट के लिए समान प्रणाली[2] प्रकाशित की थी।
होरे त्रिगुण
होरे तर्क की केंद्रीय विशेषता होरे त्रिगुण है। त्रिगुण बताता है कि कोड के एक टुकड़े का निष्पादन कैसे गणना की स्थिति को बदलता है। होरे त्रिगुण का रूप है
जहां और अभिकथन हैं और कमांड है।[note 1] को पूर्व अवस्था और को पश्च अवस्था नाम दिया गया है- जब पूर्व शर्त पूर्ण हो जाती है, तो कमांड निष्पादित करने से पश्च अवस्था स्थापित हो जाती है। विधेय तर्क में अभिकथन सूत्र हैं।
होरे तर्क साधारण अनिवार्य प्रोग्रामिंग भाषा के सभी निर्माणों के लिए स्वयंसिद्ध और अनुमान नियम प्रदान करता है। होरे के मूल पेपर में सरल भाषा के नियमों के अलावा, होरे और कई अन्य शोधकर्ताओं द्वारा तब से अन्य भाषा निर्माणों के लिए नियम विकसित किए गए हैं। समवर्ती, प्रक्रियाओं, व्यतिक्रम, और संकेत के लिए नियम हैं।
आंशिक और कुल शुद्धता
मानक होरे तर्क का उपयोग करते हुए, केवल आंशिक शुद्धता ही सिद्ध की जा सकती है। कुल शुद्धता के लिए अतिरिक्त रूप से समाप्ति की आवश्यकता होती है, जिसे अलग से या जबकि नियम के विस्तारित संस्करण के साथ सिद्ध किया जा सकता है।[3] इस प्रकार होरे त्रिगुण का सहज ज्ञान युक्त पठन है- जब भी , के निष्पादन से पहली अवस्था को धारण करता है, तो बाद में धारण करेगा, या समाप्त नहीं होता है। बाद की स्थिति में, कोई "बाद" नहीं है, इसलिए कोई भी कथन हो सकता है। वास्तव में, यह व्यक्त करने के लिए कि समाप्त नहीं होता है, असत्य होने के लिए कोई भी चुन सकता है।
यहाँ और इस लेख के अन्य भागों में "समाप्ति" का अर्थ व्यापक अर्थों में है कि गणना अंततः समाप्त हो जाएगी, अर्थात यह अनंत छोरों की अनुपस्थिति का अर्थ है यह कार्यान्वयन सीमा के उल्लंघन (जैसे शून्य से विभाजन) की अनुपस्थिति को प्रोग्राम को समय से पहले रोकना नहीं दर्शाता है। अपने 1969 के पेपर में, होरे ने समाप्ति की एक संकीर्ण धारणा का उपयोग किया, जिसमें कार्यान्वयन सीमा के उल्लंघन की अनुपस्थिति भी सम्मिलित थी, और समाप्ति की व्यापक धारणा के लिए अपनी प्राथमिकता व्यक्त की क्योंकि यह कार्यान्वयन-स्वतंत्र होने का दावा करता है-[4]
ऊपर उद्धृत सिद्धांतों और नियमों में एक और कमी यह है कि वे इस बात के प्रमाण के लिए कोई आधार नहीं देते हैं कि प्रोग्राम सफलतापूर्वक समाप्त हो गया है। समाप्त करने में विफलता अनंत लूप के कारण हो सकती है या यह कार्यान्वयन-परिभाषित सीमा के उल्लंघन के कारण हो सकता है, उदाहरण के लिए, संख्यात्मक संकार्य की सीमा, स्टोरेज का आकार, या ऑपरेटिंग सिस्टम की समय सीमा। इस प्रकार अंकन “” की व्याख्या की जानी चाहिए "बशर्ते कि कार्यक्रम सफलतापूर्वक समाप्त हो जाए, इसके परिणामों के गुणों को द्वारा वर्णित किया गया है।" स्वयंसिद्धों को अनुकूलित करना काफी आसान है ताकि उन्हें गैर-समाप्ति प्रोग्रामों के "परिणामों" की भविष्यवाणी करने के लिए उपयोग नहीं किया जा सके लेकिन स्वयंसिद्धों का वास्तविक उपयोग अब कई कार्यान्वयन-निर्भर विशेषताओं के ज्ञान पर निर्भर करेगा, उदाहरण के लिए, कंप्यूटर का आकार और गति, संख्याओं की सीमा और अतिप्रवाह तकनीक का विकल्प। अनंत लूप से बचने के प्रमाण के अलावा, किसी प्रोग्राम की "सशर्त" शुद्धता को सिद्ध करना और चेतावनी देने के लिए कार्यान्वयन पर भरोसा करना सम्भवतः बेहतर है, यदि इसे कार्यान्वयन सीमा के उल्लंघन के परिणामस्वरूप प्रोग्राम के निष्पादन को त्यागना पड़ा हो।
नियम
रिक्त कथन स्वयंसिद्ध स्कीमा
रिक्त कथन नियम यह दावा करता है कि स्किप कथन प्रोग्राम की स्थिति को नहीं बदलता है, इस प्रकार स्किप से पहले जो भी सही है वह बाद में भी सही रहेगा।[note 2]
नियत कार्य स्वयंसिद्ध स्कीमा
नियत कार्य स्वयंसिद्ध कहता है कि, नियत कार्य के बाद, कोई भी विधेय जो पहले नियत कार्य के दाईं ओर के लिए सही था, अब चर के लिए मान्य है। औपचारिक रूप से, मान लीजिए कि P अभिकथन है जिसमें चर x मुक्त है। तब-
जहां अभिकथन P को दर्शाता है जिसमें x की प्रत्येक मुक्त घटना को अभिव्यक्ति E द्वारा प्रतिस्थापित किया गया है।
नियत कार्य स्वयंसिद्ध योजना का अर्थ है कि का सत्य P के बाद के नियत कार्य सत्य के बराबर है। इस प्रकार नियत कार्य से पहले सत्य थे, नियत कार्य स्वयंसिद्ध द्वारा, फिर P जिसके बाद सत्य होगा। इसके विपरीत, असत्य (अर्थात सत्य) नियत कार्य कथन से पहले थे, P को बाद में असत्य होना चाहिए।
मान्य त्रिगुण के उदाहरणों में सम्मिलित हैं-