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

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

कार्यक्रम परिशोधन

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

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

डेटा परिशोधन

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

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

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

शोधन कलन

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

शोधन प्रकार

Main article: Refinement type

प्रकार सिद्धांत में, शोधन प्रकार प्रकार विधेय से संपन्न है जिसे परिष्कृत प्रकार के किसी भी तत्व के लिए धारण किया जाता है। शोधन प्रकार फ़ंक्शन तर्क के रूप में उपयोग किए जाने पर पूर्व शर्त या रिटर्न प्रकार के रूप में उपयोग किए जाने पर पोस्टकंडिशन व्यक्त कर सकते हैं: उदाहरण के लिए, फ़ंक्शन का प्रकार जो प्राकृतिक संख्याओं को स्वीकार करता है और 5 से अधिक प्राकृतिक संख्याओं को लौटाता है, उसे इस प्रकार लिखा जा सकता है $f:\mathbb {N} \rightarrow \{n:\mathbb {N} \,|\,n>5\}$. इस प्रकार शोधन प्रकार व्यवहारिक उपप्रकार से संबंधित हैं।

यह भी देखें

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