मैं होरे लॉजिक देख रहा हूं और मुझे लूप इनवेरिएंट खोजने की विधि समझने में समस्याएं आ रही हैं।होरे लॉजिक लूप इनवेरिएंट
क्या कोई लूप इनवेरिएंट की गणना करने के लिए उपयोग की जाने वाली विधि को समझा सकता है?
और लूप इनवेरिएंट को "उपयोगी" होना चाहिए?
मैं केवल की तरह, सरल उदाहरण के साथ काम कर अपरिवर्तनशीलताओं खोजने और आंशिक और पूर्ण सुधार साबित उदाहरण में हूँ:
{ i ≥ 0 } while i > 0 do i := i−1 { i = 0 }
हम साबित (आंशिक) कार्यक्रमों की सत्यता के लिए होरे के तर्क के बारे में बात कर रहे हैं, तो आप पूर्व शर्त और postcondition का उपयोग करें, कार्यक्रम विघटित और होरे के तर्क अनुमान प्रणाली के नियमों का उपयोग बना सकते हैं और एक आगमनात्मक सूत्र साबित करने के लिए।
अपने उदाहरण में, आप कार्यक्रम विघटित नियम
{p} while b do S {p^not(b)} <=> {p^b} S {p}
का उपयोग कर अपने मामले में चाहते हैं
तो अगले चरण में हम {i ≥ 0^i > 0} i := i−1 {i ≥ 0} का अनुमान लगाते हैं। इसे और अधिक आसानी से अनुमानित और साबित किया जा सकता है। मुझे उम्मीद है कि यह मदद करता है।
(अपने तर्क के लिए) उपयोगी होने के नाते अपरिवर्तनीय का मुख्य बिंदु है। तो, उस शर्त के बाद देखें जिसे आप साबित करना चाहते हैं और एक आविष्कार बनाने की कोशिश करें जो आपको बाद में चरण-दर-चरण पर पहुंचने में मदद करेगी और यह लूप के कोड से व्युत्पन्न है।
मैं अगर यह आपके प्रश्न का उत्तर होगा यकीन नहीं है, लेकिन सिर्फ मामले में यह करता है:
औपचारिक चीज़ के लिए बहुत अनौपचारिक स्पष्टीकरण :)। Invariants प्रारंभ और अंत में नहीं पकड़ते हैं, लेकिन जब तक इनपुट पूर्व शर्त को पूरा करता है तब तक उन्हें एक कार्यक्रम के प्रत्येक कथन के बाद पकड़ना चाहिए। होरे का तर्क एक साधारण कार्यक्रम स्कीमा पर आधारित है, ठोस कार्यान्वयन लैंगेज वास्तव में कोई फर्क नहीं पड़ता। –
हे, टिप्पणी के लिए धन्यवाद :) मेरी शिक्षा में शब्द 'invariant' को बहुत कुछ फेंक दिया गया था, बिना किसी औपचारिक स्पष्टीकरण के - मैंने स्पष्ट रूप से कुछ गलत विचार उठाए। –
मुझे लगता है कि जब होरे लॉजिक की बात आती है, तो इनवेरिएंट बिना किसी अच्छे स्पष्टीकरण के फेंक दिया जाता है ... – nunopolonia