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

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

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

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

यह भी देखें

• एफिल (प्रोग्रामिंग लैंग्वेज)