Predicative programming
प्रेडिकेटिव प्रोग्रामिंग कार्यक्रम विनिर्देश और परिशोधन के लिए एक औपचारिक विधि का मूल नाम है, जिसे हाल ही में एरिक हेनर द्वारा आविष्कार किया गया प्रोग्रामिंग का व्यावहारिक सिद्धांत कहा जाता है। केंद्रीय विचार यह है कि प्रत्येक विनिर्देश एक द्विआधारी (बूलियन) अभिव्यक्ति है जो स्वीकार्य कंप्यूटर व्यवहार के लिए सही है और अस्वीकार्य व्यवहार के लिए गलत है। यह इस प्रकार है कि परिष्करण केवल निहितार्थ है। यह सबसे सरल औपचारिक विधि है, और सबसे सामान्य है, जो अनुक्रमिक, समानांतर, स्वतंत्र, संचार, समाप्ति, गैर-समाप्ति, प्राकृतिक-समय, वास्तविक-समय, नियतात्मक और संभावित कार्यक्रमों पर लागू होती है, और इसमें समय और स्थान सीमा शामिल हैं। एक प्रोग्रामिंग भाषा में आदेशों को विनिर्देशन का एक विशेष मामला माना जाता है-वे विनिर्देश जो संकलन योग्य हैं। उदाहरण के लिए, यदि प्रोग्राम चर हैं, और, आदेशः = + 1 विनिर्देशन (द्विआधारी अभिव्यक्ति) = + 1 के बराबर है, जिसमें, और असाइनमेंट से पहले प्रोग्राम चर के मूल्यों का प्रतिनिधित्व करता है, और, और असाइनमेंट के बाद प्रोग्राम चर के मूल्यों का प्रतिनिधित्व करता है। यदि विनिर्देशन> है, तो हम आसानी से (: = + 1) ⇒ (>) साबित करते हैं, जो कहता है किः = + 1 का तात्पर्य है, या परिष्कृत करता है, या लागू करता है>। लूप प्रूफ बहुत सरल हैं। उदाहरण के लिए, यदि एक पूर्णांक चर है, तो यह साबित करने के लिए कि जबकि> 0 करता हैः =-1 od परिष्कृत करता है, या विनिर्देश को लागू करता है, तो साबित करें कि यदि> 0 तोः =-1; (≤0 ियम = 0) अन्यथा फाई णि (≤0 णि = 0) जहां = (=) खाली है, या कुछ भी नहीं कमांड है। लूप अपरिवर्तनीय या न्यूनतम निश्चित बिंदु की कोई आवश्यकता नहीं है। कई मध्यवर्ती उथले और गहरे निकास वाले लूप एक ही तरह से काम करते हैं। प्रमाण का यह सरलीकृत रूप संभव है क्योंकि कार्यक्रम आदेशों और विनिर्देशों को सार्थक रूप से एक साथ मिलाया जा सकता है। निष्पादन समय (ऊपरी सीमा, निचली सीमा, सटीक समय) को उसी तरह से साबित किया जा सकता है, केवल एक समय चर पेश करके। समाप्ति साबित करने के लिए, साबित करें कि निष्पादन का समय सीमित है। गैर-समाप्ति साबित करने के लिए, साबित करें कि निष्पादन का समय अनंत है। उदाहरण के लिए, यदि समय चर है, और समय को पुनरावृत्तियों की गिनती करके मापा जाता है, तो यह साबित करने के लिए कि पिछले वाइल-लूप के निष्पादन में समय लगता है जब शुरू में गैर-नकारात्मक होता है, और हमेशा के लिए लेता है जब शुरू में नकारात्मक होता है, तो साबित करें कि यदि> 0 तोः =-1;: = + 1; (ω0 α = +) α (<0 α = α) अन्यथा α (α0 α = α) α (<0 α = α) α (α0 α = α) जहाँ = (= α =)। ग्रंथ सूची ई. सी. आर. हेनर, प्रोग्रामिंग का एक व्यावहारिक सिद्धांत, स्प्रिंगर-वेरलैग 1993। प्रोग्रामिंग के एक व्यावहारिक सिद्धांत पर सबसे हालिया संस्करण ऑनलाइन। बाहरी लिंक एरिक हेनर द्वारा प्रकाशन। औपचारिक विधियाँ औपचारिक विनिर्देशन भाषाएँ तार्किक गणना