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

Revision as of 02:27, 13 March 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]$ को (

[1]

[2]

[note 1]

[3]

[4]

[note 2]

@@ 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 187: / Line 187: @@
 {{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.
@@ Line 215: / Line 209: @@
 {{Program analysis}}
-{{Authority control}}[[Category: कंप्यूटिंग में 1969]] [[Category: कार्यक्रम तर्क]] [[Category: स्थैतिक कार्यक्रम विश्लेषण]]
+[[Category: कंप्यूटिंग में 1969]] [[Category: कार्यक्रम तर्क]] [[Category: स्थैतिक कार्यक्रम विश्लेषण]]

Anonymous

Search

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

Namespaces

More

Page actions