शोधन (कंप्यूटिंग)

रिफ़ाइनमेंट कंप्यूटर विज्ञान का सामान्य शब्द है जिसमें करेक्ट (कंप्यूटर विज्ञान) कंप्यूटर प्रोग्राम बनाने और उनके फॉर्मल वेरिफिकेशन को सक्षम करने के लिए उपस्थित प्रोग्राम को सरल बनाने के विभिन्न दृष्टिकोण सम्मिलित हैं।

प्रोग्राम रिफ़ाइनमेंट

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

स्क्रम (सॉफ़्टवेयर विकास) जैसे सक्रिय सॉफ़्टवेयर विकास दृष्टिकोणों में उत्पाद बैकलॉग (आवश्यकताओं की सूची) की समय-समय पर प्रगतिशील तैयारी को भी सामान्यतः रिफ़ाइनमेंट के रूप में वर्णित किया जाता है।^[1]

डेटा रिफ़ाइनमेंट

डेटा रिफ़ाइनमेंट करेक्ट डेटा मॉडल (उदाहरण के लिए सेट (गणित) के संदर्भ में) को कार्यान्वयन योग्य डेटा संरचनाओं (जैसे ऐरे डेटा संरचना) में परिवर्तित करने के लिए उपयोग किया जाता है। संचालन रिफ़ाइनमेंट सिस्टम पर संचालन के विनिर्देश को कार्यान्वयन योग्य कंप्यूटर प्रोग्राम (उदाहरण के लिए, प्रक्रिया (कंप्यूटर विज्ञान)) में परिवर्तित करता है। इस प्रक्रिया में पोस्टकंडिशन को स्थिर किया जा सकता है और प्रीकंडीशन को निर्बल किया जा सकता है। यह विनिर्देश में किसी भी गैर-नियतात्मक एल्गोरिदम को कम कर देता है, सामान्यतः पूर्ण रूप से नियतात्मक कार्यान्वयन के लिए किया जाता है।

उदाहरण के लिए, x ∈ {1,2,3} (जहाँ x संचालन के पश्चात् चर (प्रोग्रामिंग) x का मान है) को x ∈ {1,2} तक रिफाइंड किया जा सकता है, फिर x ∈ {1}, और x= 1 के रूप में कार्यान्वित किया जा सकता है। इस स्तिथि में x= 2 और x= 3 का कार्यान्वयन रिफ़ाइनमेंट के लिए भिन्न मार्ग का उपयोग करके समान रूप से स्वीकार्य होगा। चूँकि, हमें सावधान रहना चाहिए कि x ∈ {} को रिफाइंड न करें क्योंकि यह कार्यान्वयन योग्य नहीं है; रिक्त सेट से किसी एलिमेंट (गणित) का चयन करना असंभव है।

पुनःकरण (कंप्यूटर विज्ञान) शब्द का भी कभी-कभी उपयोग किया जाता है (क्लिफ जोन्स (कंप्यूटर वैज्ञानिक) द्वारा विकसित किया गया)। जब औपचारिक रिफ़ाइनमेंट संभव नहीं हो तो रिट्रेंचमेंट (कंप्यूटिंग) वैकल्पिक तकनीक है। रिफ़ाइनमेंट का विपरीत अमूर्तन (कंप्यूटर विज्ञान) है।

रिफ़ाइनमेंट कैलकुलस

रिफ़ाइनमेंट कैलकुलस ऐसी फॉर्मल सिस्टम है (होरे आर्गुमेंट्स से प्रेरित) जो प्रोग्राम रिफ़ाइनमेंट को बढ़ावा देती है। फ़र्माटी परिवर्तन सिस्टम रिफ़ाइनमेंट का औद्योगिक-शक्ति कार्यान्वयन है। बी-विधि भी औपचारिक विधि है जो घटक भाषा के साथ रिफ़ाइनमेंट कैलकुलस का विस्तार करती है: इसका उपयोग औद्योगिक विकास में किया गया है।

रिफ़ाइनमेंट टाइप

टाइप सिद्धांत में, रिफ़ाइनमेंट टाइप^[2]^[3]^[4] ऐसा टाइप है जो प्रेडीकेट से संपन्न है जिसे रिफाइंड टाइप के किसी भी एलिमेंट के लिए धारण किया जाता है। रिफ़ाइनमेंट टाइप फंक्शन आर्गुमेंट्स के रूप में उपयोग किए जाने पर पूर्व नियम या रिटर्न टाइप के रूप में उपयोग किए जाने पर पोस्टकंडिशन को व्यक्त कर सकते हैं: उदाहरण के लिए, फंक्शन का टाइप जो नेचुरल संख्याओं को स्वीकार करता है और 5 से अधिक नेचुरल संख्याओं को रिटर्न करता है, उसे इस प्रकार $f:\mathbb {N} \rightarrow \{n:\mathbb {N} \,|\,n>5\}$ लिखा जा सकता है, इस प्रकार रिफ़ाइनमेंट टाइप रिफिकेशन सबटाइपिंग से संबंधित हैं।

यह भी देखें

रिफिकेशन (कंप्यूटर विज्ञान)

संदर्भ

↑ Cho, L (2009). "एक चुस्त संस्कृति को अपनाना एक उपयोगकर्ता अनुभव टीम की यात्रा". Agile Conference: 416. doi:10.1109/AGILE.2009.76. ISBN 978-0-7695-3768-9.
↑ Freeman, T.; Pfenning, F. (1991). "एमएल के लिए शोधन प्रकार" (PDF). Proceedings of the ACM Conference on Programming Language Design and Implementation. pp. 268–277. doi:10.1145/113445.113468.
↑ Hayashi, S. (1993). "शोधन प्रकार का तर्क". Proceedings of the Workshop on Types for Proofs and Programs. pp. 157–172. CiteSeerX 10.1.1.38.6346. doi:10.1007/3-540-58085-9_74.
↑ Denney, E. (1998). "विशिष्टता के लिए शोधन प्रकार". Proceedings of the IFIP International Conference on Programming Concepts and Methods. Vol. 125. Chapman & Hall. pp. 148–166. CiteSeerX 10.1.1.22.4988.

This software-engineering-related article is a stub. You can help Wikipedia by expanding it.

[1] Cho, L (2009). "एक चुस्त संस्कृति को अपनाना एक उपयोगकर्ता अनुभव टीम की यात्रा". Agile Conference: 416. doi:10.1109/AGILE.2009.76. ISBN 978-0-7695-3768-9.

[2] Freeman, T.; Pfenning, F. (1991). "एमएल के लिए शोधन प्रकार" (PDF). Proceedings of the ACM Conference on Programming Language Design and Implementation. pp. 268–277. doi:10.1145/113445.113468.

[3] Hayashi, S. (1993). "शोधन प्रकार का तर्क". Proceedings of the Workshop on Types for Proofs and Programs. pp. 157–172. CiteSeerX 10.1.1.38.6346. doi:10.1007/3-540-58085-9_74.

[4] Denney, E. (1998). "विशिष्टता के लिए शोधन प्रकार". Proceedings of the IFIP International Conference on Programming Concepts and Methods. Vol. 125. Chapman & Hall. pp. 148–166. CiteSeerX 10.1.1.22.4988.

[1]

[2]

[3]

[4]