शोधन (कंप्यूटिंग): Difference between revisions

From Vigyanwiki
No edit summary
No edit summary
Line 1: Line 1:
{{Data transformation}}
{{Data transformation}}


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


==कार्यक्रम परिशोधन==
==प्रोग्राम परिशोधन==
औपचारिक तरीकों में, कार्यक्रम परिशोधन ''सार'' (उच्च-स्तरीय) औपचारिक विनिर्देश का ''ठोस'' (निम्न-स्तरीय) निष्पादन योग्य कार्यक्रम में [[औपचारिक सत्यापन]] परिवर्तन है।{{citation needed|date=September 2010}} [[चरणबद्ध शोधन]] इस प्रक्रिया को चरणों में पूरा करने की अनुमति देता है। तार्किक रूप से, परिशोधन में आम तौर पर [[तार्किक परिणाम]] शामिल होते हैं, लेकिन अतिरिक्त जटिलताएँ भी हो सकती हैं।
औपचारिक विधियों में, प्रोग्राम परिशोधन सार (उच्च-स्तरीय) औपचारिक विनिर्देश का जटिल (निम्न-स्तरीय) निष्पादन योग्य प्रोग्राम में [[औपचारिक सत्यापन]] योग्य परिवर्तन है। [[चरणबद्ध शोधन]] इस प्रक्रिया को चरणों में पूर्ण करने की अनुमति देता है। तार्किक रूप से, परिशोधन में सामान्यतः [[तार्किक परिणाम|निहितार्थ परिणाम]] सम्मिलित होते हैं, किंतु अतिरिक्त जटिलताएँ भी हो सकती हैं।


[[स्क्रम (सॉफ़्टवेयर विकास)]] जैसे फुर्तीले सॉफ़्टवेयर विकास दृष्टिकोणों में उत्पाद बैकलॉग (आवश्यकताओं की सूची) की प्रगतिशील समय-समय पर तैयारी को भी आमतौर पर शोधन के रूप में वर्णित किया जाता है।<ref>{{cite journal|last=Cho|first=L|title=एक चुस्त संस्कृति को अपनाना एक उपयोगकर्ता अनुभव टीम की यात्रा|journal=Agile Conference|year=2009|doi=10.1109/AGILE.2009.76|isbn=978-0-7695-3768-9|pages=416}}</ref>
[[स्क्रम (सॉफ़्टवेयर विकास)]] जैसे सक्रिय सॉफ़्टवेयर विकास दृष्टिकोणों में उत्पाद बैकलॉग (आवश्यकताओं की सूची) की समय-समय पर प्रगतिशील तैयारी को भी सामान्यतः शोधन के रूप में वर्णित किया जाता है।<ref>{{cite journal|last=Cho|first=L|title=एक चुस्त संस्कृति को अपनाना एक उपयोगकर्ता अनुभव टीम की यात्रा|journal=Agile Conference|year=2009|doi=10.1109/AGILE.2009.76|isbn=978-0-7695-3768-9|pages=416}}</ref>


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


==डेटा परिशोधन==
उदाहरण के लिए, x ∈ {1,2,3} (जहाँ x संचालन के पश्चात् [[ चर (प्रोग्रामिंग) |चर (प्रोग्रामिंग)]] x का मान है) को x ∈ {1,2} तक परिष्कृत किया जा सकता है, फिर x ∈ {1}, और x= 1 के रूप में कार्यान्वित किया जा सकता है। इस स्तिथि में x= 2 और x= 3 का कार्यान्वयन परिशोधन के लिए भिन्न मार्ग का उपयोग करके समान रूप से स्वीकार्य होगा। चूँकि, हमें सावधान रहना चाहिए कि x ∈ {} को परिष्कृत न करें क्योंकि यह कार्यान्वयन योग्य नहीं है; [[खाली सेट|रिक्त सेट]] से किसी [[तत्व (गणित)|सदस्य (गणित)]] का चयन करना असंभव है।
डेटा परिशोधन अमूर्त डेटा मॉडल (उदाहरण के लिए [[सेट (गणित)]] के संदर्भ में) को कार्यान्वयन योग्य डेटा संरचनाओं (जैसे ऐरे डेटा संरचना) में परिवर्तित करने के लिए उपयोग किया जाता है।{{citation needed|date=September 2010}} ऑपरेशन परिशोधन सिस्टम पर ऑपरेशन के [[विनिर्देश]] को कार्यान्वयन योग्य [[कंप्यूटर प्रोग्राम]] (उदाहरण के लिए, [[प्रक्रिया (कंप्यूटर विज्ञान)]]) में परिवर्तित करता है। इस प्रक्रिया में [[पोस्टकंडिशन]] को मजबूत किया जा सकता है और/या [[शर्त लगाना]] को कमजोर किया जा सकता है। यह विनिर्देश में किसी भी गैर-नियतात्मक एल्गोरिदम को कम कर देता है, आमतौर पर पूरी तरह से नियतात्मक कार्यान्वयन के लिए।


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


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


==शोधन प्रकार==
==शोधन प्रकार==
{{Main|Refinement type}}
{{Main|शोधन प्रकार}}


[[प्रकार सिद्धांत]] में, शोधन प्रकार<ref>{{cite conference|first1=T.|last1=Freeman|first2=F.|last2=Pfenning|url=https://www.cs.cmu.edu/~fp/papers/pldi91.pdf|doi=10.1145/113445.113468 |title=एमएल के लिए शोधन प्रकार|book-title=Proceedings of the ACM Conference on Programming Language Design and Implementation|pages=268–277|year=1991}}</ref><ref>{{cite conference|first=S.|last=Hayashi|title=शोधन प्रकार का तर्क|citeseerx = 10.1.1.38.6346|doi=10.1007/3-540-58085-9_74|book-title=Proceedings of the Workshop on Types for Proofs and Programs|pages=157–172|year=1993}}</ref><ref>{{cite conference|first=E.|last=Denney|citeseerx = 10.1.1.22.4988|title=विशिष्टता के लिए शोधन प्रकार|book-title=Proceedings of the IFIP International Conference on Programming Concepts and Methods|volume=125|pages=148–166|publisher=Chapman & Hall|year=1998}}</ref> प्रकार विधेय से संपन्न है जिसे परिष्कृत प्रकार के किसी भी तत्व के लिए धारण किया जाता है। शोधन प्रकार [[फ़ंक्शन तर्क]] के रूप में उपयोग किए जाने पर पूर्व शर्त या रिटर्न प्रकार के रूप में उपयोग किए जाने पर पोस्टकंडिशन व्यक्त कर सकते हैं: उदाहरण के लिए, फ़ंक्शन का प्रकार जो प्राकृतिक संख्याओं को स्वीकार करता है और 5 से अधिक प्राकृतिक संख्याओं को लौटाता है, उसे इस प्रकार लिखा जा सकता है <math>f: \mathbb{N} \rarr \{n: \mathbb{N} \, | \, n > 5\}</math>. इस प्रकार शोधन प्रकार [[व्यवहारिक उपप्रकार]] से संबंधित हैं।
[[प्रकार सिद्धांत]] में, शोधन प्रकार<ref>{{cite conference|first1=T.|last1=Freeman|first2=F.|last2=Pfenning|url=https://www.cs.cmu.edu/~fp/papers/pldi91.pdf|doi=10.1145/113445.113468 |title=एमएल के लिए शोधन प्रकार|book-title=Proceedings of the ACM Conference on Programming Language Design and Implementation|pages=268–277|year=1991}}</ref><ref>{{cite conference|first=S.|last=Hayashi|title=शोधन प्रकार का तर्क|citeseerx = 10.1.1.38.6346|doi=10.1007/3-540-58085-9_74|book-title=Proceedings of the Workshop on Types for Proofs and Programs|pages=157–172|year=1993}}</ref><ref>{{cite conference|first=E.|last=Denney|citeseerx = 10.1.1.22.4988|title=विशिष्टता के लिए शोधन प्रकार|book-title=Proceedings of the IFIP International Conference on Programming Concepts and Methods|volume=125|pages=148–166|publisher=Chapman & Hall|year=1998}}</ref> ऐसा प्रकार है जो विधेय से संपन्न है जिसे परिष्कृत प्रकार के किसी भी सदस्य के लिए धारण किया जाता है। शोधन प्रकार [[फ़ंक्शन तर्क|फलन तर्क]] के रूप में उपयोग किए जाने पर पूर्व नियम या रिटर्न प्रकार के रूप में उपयोग किए जाने पर पोस्टकंडिशन व्यक्त कर सकते हैं: उदाहरण के लिए, फलन का प्रकार जो प्राकृतिक संख्याओं को स्वीकार करता है और 5 से अधिक प्राकृतिक संख्याओं को रिटर्न है, उसे इस प्रकार <math>f: \mathbb{N} \rarr \{n: \mathbb{N} \, | \, n > 5\}</math> लिखा जा सकता है, इस प्रकार शोधन प्रकार [[व्यवहारिक उपप्रकार]] से संबंधित हैं।


==यह भी देखें==
==यह भी देखें==
* रीफिकेशन (कंप्यूटर विज्ञान)
* पुनःकरण (कंप्यूटर विज्ञान)


==संदर्भ==
==संदर्भ==

Revision as of 10:42, 5 July 2023

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

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

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

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

डेटा परिशोधन

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

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

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

शोधन कलन

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

शोधन प्रकार

प्रकार सिद्धांत में, शोधन प्रकार[2][3][4] ऐसा प्रकार है जो विधेय से संपन्न है जिसे परिष्कृत प्रकार के किसी भी सदस्य के लिए धारण किया जाता है। शोधन प्रकार फलन तर्क के रूप में उपयोग किए जाने पर पूर्व नियम या रिटर्न प्रकार के रूप में उपयोग किए जाने पर पोस्टकंडिशन व्यक्त कर सकते हैं: उदाहरण के लिए, फलन का प्रकार जो प्राकृतिक संख्याओं को स्वीकार करता है और 5 से अधिक प्राकृतिक संख्याओं को रिटर्न है, उसे इस प्रकार लिखा जा सकता है, इस प्रकार शोधन प्रकार व्यवहारिक उपप्रकार से संबंधित हैं।

यह भी देखें

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

संदर्भ

  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.