शोधन (कंप्यूटिंग): Difference between revisions
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> | ||
| Line 10: | Line 10: | ||
==डेटा परिशोधन== | ==डेटा परिशोधन== | ||
डेटा परिशोधन | डेटा परिशोधन अमूर्त डेटा मॉडल (उदाहरण के लिए [[सेट (गणित)]] के संदर्भ में) को कार्यान्वयन योग्य डेटा संरचनाओं (जैसे ऐरे डेटा संरचना) में परिवर्तित करने के लिए उपयोग किया जाता है।{{citation needed|date=September 2010}} ऑपरेशन परिशोधन सिस्टम पर ऑपरेशन के [[विनिर्देश]] को कार्यान्वयन योग्य [[कंप्यूटर प्रोग्राम]] (उदाहरण के लिए, [[प्रक्रिया (कंप्यूटर विज्ञान)]]) में परिवर्तित करता है। इस प्रक्रिया में [[पोस्टकंडिशन]] को मजबूत किया जा सकता है और/या [[शर्त लगाना]] को कमजोर किया जा सकता है। यह विनिर्देश में किसी भी गैर-नियतात्मक एल्गोरिदम को कम कर देता है, आमतौर पर पूरी तरह से नियतात्मक कार्यान्वयन के लिए। | ||
उदाहरण के लिए, x ∈ {1,2,3} (जहाँ x | उदाहरण के लिए, x ∈ {1,2,3} (जहाँ x ऑपरेशन के बाद [[ चर (प्रोग्रामिंग) ]] x का मान है) को x ∈ {1,2} तक परिष्कृत किया जा सकता है, फिर x ∈ {1}, और कार्यान्वित किया जा सकता है x := 1 के रूप में। इस मामले में x := 2 और x := 3 का कार्यान्वयन समान रूप से स्वीकार्य होगा, शोधन के लिए अलग मार्ग का उपयोग किया जाएगा। हालाँकि, हमें सावधान रहना चाहिए कि हम x ∈ {} (झूठे के बराबर) को परिष्कृत न करें क्योंकि यह कार्यान्वयन योग्य नहीं है; [[खाली सेट]] से [[तत्व (गणित)]] का चयन करना असंभव है। | ||
[[रीफिकेशन (कंप्यूटर विज्ञान)]] शब्द का भी कभी-कभी उपयोग किया जाता है ([[क्लिफ जोन्स (कंप्यूटर वैज्ञानिक)]] द्वारा गढ़ा गया)। जब औपचारिक शोधन संभव नहीं हो तो [[छंटनी (कंप्यूटिंग)]] | [[रीफिकेशन (कंप्यूटर विज्ञान)]] शब्द का भी कभी-कभी उपयोग किया जाता है ([[क्लिफ जोन्स (कंप्यूटर वैज्ञानिक)]] द्वारा गढ़ा गया)। जब औपचारिक शोधन संभव नहीं हो तो [[छंटनी (कंप्यूटिंग)]] वैकल्पिक तकनीक है। शोधन का विपरीत है [[अमूर्तन (कंप्यूटर विज्ञान)]]। | ||
==शोधन कलन== | ==शोधन कलन== | ||
शोधन कैलकुलस | शोधन कैलकुलस [[औपचारिक प्रणाली]] है ([[होरे तर्क]] से प्रेरित) जो कार्यक्रम शोधन को बढ़ावा देती है। FermaT परिवर्तन प्रणाली शोधन का औद्योगिक-शक्ति कार्यान्वयन है। [[बी-विधि]] भी [[औपचारिक विधि]] है जो घटक भाषा के साथ शोधन कैलकुलस का विस्तार करती है: इसका उपयोग औद्योगिक विकास में किया गया है। | ||
==शोधन प्रकार== | ==शोधन प्रकार== | ||
{{Main|Refinement type}} | {{Main|Refinement type}} | ||
[[प्रकार सिद्धांत]] में, | [[प्रकार सिद्धांत]] में, शोधन प्रकार<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:21, 5 July 2023
| Data transformation |
|---|
| Concepts |
| Transformation languages |
| Techniques and transforms |
| Applications |
| Related |
शोधन कंप्यूटर विज्ञान का सामान्य शब्द है जिसमें शुद्धता (कंप्यूटर विज्ञान) कंप्यूटर प्रोग्राम तैयार करने और उनके औपचारिक सत्यापन को सक्षम करने के लिए मौजूदा प्रोग्राम को सरल बनाने के विभिन्न दृष्टिकोण शामिल हैं।
कार्यक्रम परिशोधन
औपचारिक तरीकों में, कार्यक्रम परिशोधन सार (उच्च-स्तरीय) औपचारिक विनिर्देश का ठोस (निम्न-स्तरीय) निष्पादन योग्य कार्यक्रम में औपचारिक सत्यापन परिवर्तन है।[citation needed] चरणबद्ध शोधन इस प्रक्रिया को चरणों में पूरा करने की अनुमति देता है। तार्किक रूप से, परिशोधन में आम तौर पर तार्किक परिणाम शामिल होते हैं, लेकिन अतिरिक्त जटिलताएँ भी हो सकती हैं।
स्क्रम (सॉफ़्टवेयर विकास) जैसे फुर्तीले सॉफ़्टवेयर विकास दृष्टिकोणों में उत्पाद बैकलॉग (आवश्यकताओं की सूची) की प्रगतिशील समय-समय पर तैयारी को भी आमतौर पर शोधन के रूप में वर्णित किया जाता है।[1]
डेटा परिशोधन
डेटा परिशोधन अमूर्त डेटा मॉडल (उदाहरण के लिए सेट (गणित) के संदर्भ में) को कार्यान्वयन योग्य डेटा संरचनाओं (जैसे ऐरे डेटा संरचना) में परिवर्तित करने के लिए उपयोग किया जाता है।[citation needed] ऑपरेशन परिशोधन सिस्टम पर ऑपरेशन के विनिर्देश को कार्यान्वयन योग्य कंप्यूटर प्रोग्राम (उदाहरण के लिए, प्रक्रिया (कंप्यूटर विज्ञान)) में परिवर्तित करता है। इस प्रक्रिया में पोस्टकंडिशन को मजबूत किया जा सकता है और/या शर्त लगाना को कमजोर किया जा सकता है। यह विनिर्देश में किसी भी गैर-नियतात्मक एल्गोरिदम को कम कर देता है, आमतौर पर पूरी तरह से नियतात्मक कार्यान्वयन के लिए।
उदाहरण के लिए, x ∈ {1,2,3} (जहाँ x ऑपरेशन के बाद चर (प्रोग्रामिंग) x का मान है) को x ∈ {1,2} तक परिष्कृत किया जा सकता है, फिर x ∈ {1}, और कार्यान्वित किया जा सकता है x := 1 के रूप में। इस मामले में x := 2 और x := 3 का कार्यान्वयन समान रूप से स्वीकार्य होगा, शोधन के लिए अलग मार्ग का उपयोग किया जाएगा। हालाँकि, हमें सावधान रहना चाहिए कि हम x ∈ {} (झूठे के बराबर) को परिष्कृत न करें क्योंकि यह कार्यान्वयन योग्य नहीं है; खाली सेट से तत्व (गणित) का चयन करना असंभव है।
रीफिकेशन (कंप्यूटर विज्ञान) शब्द का भी कभी-कभी उपयोग किया जाता है (क्लिफ जोन्स (कंप्यूटर वैज्ञानिक) द्वारा गढ़ा गया)। जब औपचारिक शोधन संभव नहीं हो तो छंटनी (कंप्यूटिंग) वैकल्पिक तकनीक है। शोधन का विपरीत है अमूर्तन (कंप्यूटर विज्ञान)।
शोधन कलन
शोधन कैलकुलस औपचारिक प्रणाली है (होरे तर्क से प्रेरित) जो कार्यक्रम शोधन को बढ़ावा देती है। FermaT परिवर्तन प्रणाली शोधन का औद्योगिक-शक्ति कार्यान्वयन है। बी-विधि भी औपचारिक विधि है जो घटक भाषा के साथ शोधन कैलकुलस का विस्तार करती है: इसका उपयोग औद्योगिक विकास में किया गया है।
शोधन प्रकार
प्रकार सिद्धांत में, शोधन प्रकार[2][3][4] प्रकार विधेय से संपन्न है जिसे परिष्कृत प्रकार के किसी भी तत्व के लिए धारण किया जाता है। शोधन प्रकार फ़ंक्शन तर्क के रूप में उपयोग किए जाने पर पूर्व शर्त या रिटर्न प्रकार के रूप में उपयोग किए जाने पर पोस्टकंडिशन व्यक्त कर सकते हैं: उदाहरण के लिए, फ़ंक्शन का प्रकार जो प्राकृतिक संख्याओं को स्वीकार करता है और 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. |
