की शुद्धता की पुष्टि करना सबसे पहले, क्या यह केवल एल्गोरिदम पर संभव है जिसका कोई दुष्प्रभाव नहीं है?औपचारिक रूप से एल्गोरिदम
दूसरा, मैं इस प्रक्रिया, किसी भी अच्छी किताबें, लेख इत्यादि के बारे में कहां से सीख सकता हूं?
COQ एक सबूत सहायक है जो सही ओकंपल आउटपुट उत्पन्न करता है। हालांकि यह बहुत जटिल है। मैं इसे देखने के लिए कभी नहीं मिला, लेकिन मेरे सहकर्मी ने शुरू किया और फिर दो महीने के बाद इसका इस्तेमाल बंद कर दिया। यह ज्यादातर इसलिए था क्योंकि वह चीजें जल्दी करना चाहता था, लेकिन अगर आपको एल्गोरिदम सत्यापित करने की आवश्यकता है तो यह एक अच्छा विचार हो सकता है।
Here is a course जो सीओक्यू का उपयोग करता है और एल्गोरिदम साबित करने के बारे में वार्ता करता है। सीओक्यू में अकादमिक पत्र लिखने के बारे में
और here is a tutorial।
भी, यहां, http://www.lix.polytechnique.fr/coq/getting-started – nlucaroni
आमतौर पर शुद्धता के प्रमाण हाथ में एल्गोरिदम के लिए बहुत विशिष्ट होते हैं।
हालांकि, कई अच्छी तरह से ज्ञात चालें हैं जिनका उपयोग किया जाता है और दोबारा उपयोग किया जाता है। उदाहरण के लिए, रिकर्सिव एल्गोरिदम के साथ आप loop invariants का उपयोग कर सकते हैं।
एक और आम चाल मूल समस्या को किसी समस्या के लिए कम कर रही है जिसके लिए आपके एल्गोरिदम का शुद्धता का सबूत दिखाना आसान है, फिर या तो आसान समस्या को सामान्यीकृत करना या यह दिखा रहा है कि मूल समस्या के समाधान में आसान समस्या का अनुवाद किया जा सकता है। Here एक विवरण है।
यदि आपके पास एक विशेष एल्गोरिदम दिमाग में है, तो आप सामान्य जवाब के बजाय उस एल्गोरिदम के लिए सबूत बनाने का तरीका पूछने में बेहतर कर सकते हैं।
एल्गोरिदम कमी (विशेष रूप से आपके द्वारा ऑफ़र किए गए लिंक में वर्णित) यह दिखाने के लिए एक सैद्धांतिक उपकरण है कि एक समस्या कम से कम किसी अन्य के रूप में कठिन है। ये प्रमाण, अक्सर ट्यूरिंग मशीन गणना मॉडल में किए जाते हैं, वे हैंड-वेवी मामलों और औपचारिक (मशीन-चेक करने योग्य) सबूत जैसे कुछ भी नहीं। वे अक्सर अभ्यास में उपयोगी होने के लिए कठोर परिस्थितियों के लिए किए जाते हैं (आपके लिंक में उदाहरण हैलटिंग समस्या के लिए है; एक समस्या को दिखाकर एनपी-हार्ड एक ज्ञात एनपी-हार्ड समस्या को कम करके भी लोकप्रिय है)। संक्षेप में, मुझे यकीन नहीं है कि समस्या में कमी, लिंक के रूप में, औपचारिक शुद्धता के साथ कुछ भी करने के लिए है। –
हम्म शायद कमी सही शब्द नहीं है जिसका उपयोग मुझे यहां करना चाहिए। जब मैं कमी कहता हूं तो मेरा मतलब निम्नलिखित उदाहरणों के साथ कुछ था। मान लीजिए कि आपके पास एक एल्गोरिदम है जो एन आयतों के चौराहे की गणना करता है, जिसे आप जानते हैं सही है। मान लीजिए कि आपके पास एक और समस्या है जिसके लिए एन आयताकारों के चौराहे की गणना करने की समस्या के लिए उस समस्या का एक गैर-तुच्छ अनुवाद है। फिर आप बाद की समस्या के समाधान की गणना करने के लिए पहले एल्गोरिदम का उपयोग करते हैं।यह सब बनी हुई है यह दिखा रहा है कि अनुवाद सही है। – ldog
लेकिन मैं देख सकता हूं कि यह भ्रमित है, यह एक चाल है जो इस तथ्य पर निर्भर करती है कि आप एक प्रसिद्ध एल्गोरिदम का उपयोग करते हैं जिसे सही माना जाता है (इस मामले में एन एन आयतों के चौराहे की गणना करने के लिए।) मैं कर सकता हूं देखें कि भ्रम कहां आता है कि यह सही एल्गोरिदम साबित करने या प्रदान करने का एक तरीका है या नहीं। – ldog
मुझे लगता है कि एल्गोरिदम की शुद्धता की पुष्टि करना एक विनिर्देश के अनुरूप है। Formal Methods नामक सैद्धांतिक कंप्यूटर विज्ञान की एक शाखा है जो आप जो भी खोज रहे हैं, वह हो सकता है यदि आपको सबूत के करीब पहुंचने की आवश्यकता हो। विकिपीडिया से,
औपचारिक तरीके एक विशेष प्रकार विनिर्देश, विकास के लिए गणितीय-आधारित तकनीकों और सॉफ्टवेयर और हार्डवेयर के सत्यापन सिस्टम
हैं
आप कई सीखने को खोजने के लिए सक्षम हो जाएगा लिंक किए गए विकिपीडिया पृष्ठ पर और Formal Methods wiki से लिंक की भीड़ से संसाधन और उपकरण।
इन किताबों को खरीदें: http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800
Gries पुस्तक, वैज्ञानिक प्रोग्रामिंग कमाल की चीज़ है। रोगी, पूरी तरह से, पूर्ण।
और यदि आपको ज़ेड पसंद है, तो आश्वस्त रहें कि आपको औपचारिक रूप से सही एल्गोरिदम लिखने की प्रक्रिया में इसे शामिल करने के लिए टूल मिलेंगे: http : //www.bmethod.com/php/methode-b-en.php –
ह्यूथ और रयान द्वारा कंप्यूटर साइंस में तर्क, सिस्टम की पुष्टि के लिए आधुनिक प्रणालियों का एक उचित पठनीय अवलोकन देता है।एक बार लोगों ने कार्यक्रमों को सही साबित करने के बारे में बात की - प्रोग्रामिंग भाषाओं के साथ जो साइड इफेक्ट्स हो सकते हैं या नहीं। इस पुस्तक और अन्यत्र से मुझे जो प्रभाव मिलता है वह यह है कि वास्तविक अनुप्रयोग अलग-अलग हैं - उदाहरण के लिए यह साबित करना कि प्रोटोकॉल सही है, या चिप की फ़्लोटिंग पॉइंट इकाई सही ढंग से विभाजित हो सकती है, या लिंक की गई सूचियों में हेरफेर करने के लिए लॉक-फ्री रूटीन सही है।
एसीएम कंप्यूटिंग सर्वेक्षण वॉल्यूम 41 अंक 4 (अक्टूबर 200 9) सॉफ्टवेयर सत्यापन पर एक विशेष मुद्दा है। ऐसा लगता है कि आप "औपचारिक तरीके: अभ्यास और अनुभव" की खोज करके एसीएम खाते के बिना कम से कम एक कागजात प्राप्त कर सकते हैं।
"औपचारिक विधियों" में आपके द्वारा उद्धृत सभी उद्देश्यों को शामिल किया गया है। मैं "सिद्ध कार्यक्रमों को सही साबित करने" के उप-क्षेत्र में हूं और मुझे यह स्वीकार करना है कि अब तक बड़ी औद्योगिक सफलताएं अन्य उप-क्षेत्रों से आ गई हैं (बस अगले वर्ष तक प्रतीक्षा करें!)। एफएमडब्ल्यूईईके जैसे एक सम्मेलन कुछ हद तक परेशान है क्योंकि यह इन सभी अलग-अलग दृष्टिकोणों और उद्देश्यों के साथ लोगों को इकट्ठा करता है, लेकिन हमारे पास बहुत आम है और विनिमय करने के लिए बहुत कुछ है। –
उपकरण Frama-C, जिसके लिए Elazar टिप्पणी में एक डेमो वीडियो से पता चलता है, तो आप एक विनिर्देश भाषा देता है, ACSL, पुष्टि करने के लिए एक सी समारोह में इस तरह के अभाव के रूप में अपने अनुबंध और सुरक्षा गुण को संतुष्ट करता है कि के लिए समारोह के ठेके और विभिन्न विश्लेषक लिखने के लिए रन-टाइम त्रुटियों का।
एक विस्तारित ट्यूटोरियल, ACSL by example, से पता चलता वास्तविक सी एल्गोरिदम के उदाहरण निर्दिष्ट किया जा रहा है और सत्यापित, और (पक्ष प्रभाव से मुक्त लोगों को आसान माना जाता है और में पहले आओ रहे effectful लोगों से पक्ष प्रभाव से मुक्त कार्यों को अलग करती है ट्यूटोरियल)। यह दस्तावेज भी दिलचस्प है कि यह उन उपकरणों के डिजाइनरों द्वारा लिखा नहीं गया था जो वर्णन करते हैं, इसलिए यह इन तकनीकों पर एक ताजा और अधिक व्यावहारिक रूप प्रदान करता है। प्रोग्रामिंग की http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html
आप लिस्प से परिचित हैं, तो आप निश्चित रूप से बाहर की जाँच करनी चाहिए ACL2। एक आसान काम है विर्थ का सिस्टमैटिक प्रोग्रामिंग, जो सत्यापन का उपयोग करने के लिए सरल दृष्टिकोण से शुरू होता है। विर्थ भाषा के लिए पूर्व-आईएसओ पास्कल का उपयोग करता है; डिजस्ट्रा गार्डन (जीसीएल) नामक एक अल्गोल -68-जैसे औपचारिकता का उपयोग करता है। औपचारिक सत्यापन डिजस्ट्रा और होरे के बाद परिपक्व हो गया है, लेकिन ये पुराने ग्रंथ अभी भी एक अच्छा प्रारंभिक बिंदु हो सकते हैं।
डिज्कस्ट्रा के अनुशासन और उसके EWDs प्रोग्रामिंग में एक विज्ञान के रूप औपचारिक सत्यापन के लिए नींव रखना:
स्टैनफोर्ड लड़कों द्वारा विकसित पीवीएस उपकरण एक विनिर्देश और सत्यापन प्रणाली है। मैंने इस पर काम किया और थोरम प्रोविंग के लिए यह बहुत उपयोगी पाया।
डब्लूआरटी (1), आपको शायद इस तरह के राज्य-आधारित दुष्प्रभावों को मॉडल करने के उद्देश्य से प्रोग्राम चर में एल्गोरिदम के दुष्प्रभावों को "कैप्चर" करने के लिए एल्गोरिदम का एक मॉडल बनाना होगा।
मुझे यकीन नहीं है कि साइड इफेक्ट्स के बारे में आपका क्या मतलब है। – ldog
इसे देखें: http://en.wikipedia.org/wiki/Side_effect_%28computer_science%29 – joemoe
http://stackoverflow.com/questions/476959/why-cant-programs-be-proven देखें जिनके कुछ अच्छे उत्तर हैं। –