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

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

प्रोग्राम परिशोधन

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

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

डेटा परिशोधन

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

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

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

शोधन कलन

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

शोधन प्रकार

Main article: शोधन प्रकार

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

यह भी देखें

• पुनःकरण (कंप्यूटर विज्ञान)