होरे तर्क

होरे तर्क (फ्लोयड-होरे तर्क या होरे नियम के रूप में भी जाना जाता है) कंप्यूटर प्रोग्राम की शुद्धता के बारे में दृढ़ता से तर्क करने के लिए तार्किक नियमों के एक क्रम के साथ औपचारिक प्रणाली है। यह 1969 में ब्रिटिश कंप्यूटर वैज्ञानिक और तर्कशास्त्री टोनी होरे द्वारा प्रस्तावित किया गया था, और बाद में होरे और अन्य शोधकर्ताओं द्वारा परिष्कृत किया गया था। मूल विचार रॉबर्ट डब्ल्यू फ़्लॉइड के काम से उत्पन्न हुए थे, जिन्होंने फ्लोचार्ट के लिए समान प्रणाली प्रकाशित की थी।

होरे त्रिगुण

होरे तर्क की केंद्रीय विशेषता होरे त्रिगुण है। त्रिगुण बताता है कि कोड के एक टुकड़े का निष्पादन कैसे गणना की स्थिति को बदलता है। होरे त्रिगुण का रूप है

$\{P\}C\{Q\}$

जहां $P$ और $Q$ अभिकथन हैं और $C$ कमांड है। $P$ को पूर्व अवस्था और $Q$ को पश्च अवस्था नाम दिया गया है- जब पूर्व शर्त पूर्ण हो जाती है, तो कमांड निष्पादित करने से पश्च अवस्था स्थापित हो जाती है। विधेय तर्क में अभिकथन सूत्र हैं।

होरे तर्क साधारण अनिवार्य प्रोग्रामिंग भाषा के सभी निर्माणों के लिए स्वयंसिद्ध और अनुमान नियम प्रदान करता है। होरे के मूल पेपर में सरल भाषा के नियमों के अलावा, होरे और कई अन्य शोधकर्ताओं द्वारा तब से अन्य भाषा निर्माणों के लिए नियम विकसित किए गए हैं। समवर्ती, प्रक्रियाओं, व्यतिक्रम, और संकेत के लिए नियम हैं।

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

मानक होरे तर्क का उपयोग करते हुए, केवल आंशिक शुद्धता ही सिद्ध की जा सकती है। कुल शुद्धता के लिए अतिरिक्त रूप से समाप्ति की आवश्यकता होती है, जिसे अलग से या जबकि नियम के विस्तारित संस्करण के साथ सिद्ध किया जा सकता है। इस प्रकार होरे त्रिगुण का सहज ज्ञान युक्त पठन है- जब भी $P$, $C$ के निष्पादन से पहली अवस्था को धारण करता है, तो $Q$ बाद में धारण करेगा, या $C$ समाप्त नहीं होता है। बाद की स्थिति में, कोई "बाद" नहीं है, इसलिए $Q$ कोई भी कथन हो सकता है। वास्तव में, यह व्यक्त करने के लिए कि $C$ समाप्त नहीं होता है, असत्य होने के लिए कोई भी $Q$ चुन सकता है।

यहाँ और इस लेख के अन्य भागों में "समाप्ति" का अर्थ व्यापक अर्थों में है कि गणना अंततः समाप्त हो जाएगी, अर्थात यह अनंत छोरों की अनुपस्थिति का अर्थ है यह कार्यान्वयन सीमा के उल्लंघन (जैसे शून्य से विभाजन) की अनुपस्थिति को प्रोग्राम को समय से पहले रोकना नहीं दर्शाता है। अपने 1969 के पेपर में, होरे ने समाप्ति की एक संकीर्ण धारणा का उपयोग किया, जिसमें कार्यान्वयन सीमा के उल्लंघन की अनुपस्थिति भी सम्मिलित थी, और समाप्ति की व्यापक धारणा के लिए अपनी प्राथमिकता व्यक्त की क्योंकि यह कार्यान्वयन-स्वतंत्र होने का दावा करता है-

ऊपर उद्धृत सिद्धांतों और नियमों में एक और कमी यह है कि वे इस बात के प्रमाण के लिए कोई आधार नहीं देते हैं कि प्रोग्राम सफलतापूर्वक समाप्त हो गया है। समाप्त करने में विफलता अनंत लूप के कारण हो सकती है या यह कार्यान्वयन-परिभाषित सीमा के उल्लंघन के कारण हो सकता है, उदाहरण के लिए, संख्यात्मक संकार्य की सीमा, स्टोरेज का आकार, या ऑपरेटिंग सिस्टम की समय सीमा। इस प्रकार अंकन “$P\{Q\}R$” की व्याख्या की जानी चाहिए "बशर्ते कि कार्यक्रम सफलतापूर्वक समाप्त हो जाए, इसके परिणामों के गुणों को $R$ द्वारा वर्णित किया गया है।" स्वयंसिद्धों को अनुकूलित करना काफी आसान है ताकि उन्हें गैर-समाप्ति प्रोग्रामों के "परिणामों" की भविष्यवाणी करने के लिए उपयोग नहीं किया जा सके लेकिन स्वयंसिद्धों का वास्तविक उपयोग अब कई कार्यान्वयन-निर्भर विशेषताओं के ज्ञान पर निर्भर करेगा, उदाहरण के लिए, कंप्यूटर का आकार और गति, संख्याओं की सीमा और अतिप्रवाह तकनीक का विकल्प। अनंत लूप से बचने के प्रमाण के अलावा, किसी प्रोग्राम की "सशर्त" शुद्धता को सिद्ध करना और चेतावनी देने के लिए कार्यान्वयन पर भरोसा करना सम्भवतः बेहतर है, यदि इसे कार्यान्वयन सीमा के उल्लंघन के परिणामस्वरूप प्रोग्राम के निष्पादन को त्यागना पड़ा हो।

नियम

खाली कथन स्वयंसिद्ध स्कीमा

NOP (कोड) नियम का दावा है कि skip कथन कार्यक्रम की स्थिति को नहीं बदलता है, इस प्रकार जो कुछ भी पहले सत्य है skip बाद में भी सही है।

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