अपरिवर्तनीय-आधारित प्रोग्रामिंग

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

अधिकांश मौजूदा प्रोग्रामिंग भाषाओं में मुख्य आयोजन संरचनाएं फॉर लूप जैसे नियंत्रण प्रवाह ब्लॉक हैंfor लूप, जबकि लूप|while लूप्स और इफ स्टेटमेंट|if बयान. ऐसी भाषाएं इनवेरिएंट-फर्स्ट प्रोग्रामिंग के लिए आदर्श नहीं हो सकती हैं, क्योंकि वे प्रोग्रामर को इनवेरिएंट लिखने से पहले नियंत्रण प्रवाह के बारे में निर्णय लेने के लिए मजबूर करती हैं। इसके अलावा, अधिकांश प्रोग्रामिंग भाषाओं में विशिष्टताओं और अपरिवर्तनीयताओं को लिखने के लिए अच्छा समर्थन नहीं है, क्योंकि उनमें क्वांटिफायर ऑपरेटरों की कमी है और कोई आमतौर पर उच्च क्रम के गुणों को व्यक्त नहीं कर सकता है।

कार्यक्रम को उसके प्रमाण के साथ विकसित करने का विचार एड्सगर डिज्क्स्ट्रा|ई.डब्ल्यू. से उत्पन्न हुआ। दिज्क्स्ट्रा। दरअसल प्रोग्राम स्टेटमेंट से पहले इनवेरिएंट लिखने पर एम.एच. द्वारा कई अलग-अलग रूपों में विचार किया गया है। वैन एम्डेन, जॉन सी. रेनॉल्ड्स|जे.सी. रेनॉल्ड्स और राल्फ-जोहान वापस|आर-जे वापस।

यह भी देखें

• एफिल (प्रोग्रामिंग भाषा)

टिप्पणियाँ

[Category:Programming paradig