संकलक शुद्धता

From alpha
Jump to navigation Jump to search

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

औपचारिक सत्यापन

संकलन की शुद्धता स्थापित करने के लिए दो मुख्य औपचारिक सत्यापन दृष्टिकोण सभी इनपुट के लिए संकलक की शुद्धता साबित कर रहे हैं और एक विशेष कार्यक्रम (अनुवाद सत्यापन) के संकलन की शुद्धता साबित कर रहे हैं।

सभी इनपुट प्रोग्राम्स के लिए कंपाइलर शुद्धता

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

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

औपचारिक रूप से सही संकलक प्राप्त करने के लिए एक अन्य दृष्टिकोण शब्दार्थ-निर्देशित संकलक पीढ़ी का उपयोग करना है।[6]


===अनुवाद सत्यापन: किसी दिए गए कार्यक्रम === पर संकलक शुद्धता

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

परीक्षण

परीक्षण एक कंपाइलर शिपिंग में प्रयास के एक महत्वपूर्ण हिस्से का प्रतिनिधित्व करता है, लेकिन मानक साहित्य में तुलनात्मक रूप से कम कवरेज प्राप्त करता है। कंपाइलर्स के 1986 के संस्करण: सिद्धांत, तकनीक और उपकरण | अहो, सेठी, और उलमैन में कंपाइलर परीक्षण पर एक पृष्ठ का खंड है, जिसमें कोई नाम नहीं है।[8] 2006 संस्करण परीक्षण पर अनुभाग को छोड़ देता है, लेकिन इसके महत्व पर जोर देता है: "संकलकों का अनुकूलन करना इतना मुश्किल है कि हम यह कहने की हिम्मत करते हैं कि कोई अनुकूलन संकलक पूरी तरह से त्रुटि मुक्त नहीं है! इस प्रकार, एक कंपाइलर लिखने में सबसे महत्वपूर्ण उद्देश्य यह है कि यह सही हो।"[9] फ्रेजर एंड हैनसन 1995 में प्रतिगमन परीक्षण पर एक संक्षिप्त खंड है; स्रोत कोड उपलब्ध है।[10] बेली एंड डेविडसन 2003 प्रक्रिया कॉल के परीक्षण को कवर करता है[11] कई लेख इस बात की पुष्टि करते हैं कि जारी किए गए कई कंपाइलरों में महत्वपूर्ण कोड-शुद्धता बग हैं।[12] शेरिडन 2007 शायद सामान्य संकलक परीक्षण पर सबसे हालिया जर्नल लेख है।[13] अधिकांश उद्देश्यों के लिए, संकलक परीक्षण पर उपलब्ध सूचना का सबसे बड़ा निकाय फोरट्रान है[14] और कोबोल[15] सत्यापन सूट।

कम्पाइलर का परीक्षण करते समय आगे की सामान्य तकनीकें फज़िंग होती हैं[16] (जो एक कंपाइलर में बग खोजने की कोशिश करने के लिए यादृच्छिक प्रोग्राम उत्पन्न करता है) और टेस्ट केस में कमी (जो इसे समझने में आसान बनाने के लिए पाए गए टेस्ट केस को कम करने की कोशिश करता है)।[17]


यह भी देखें

संदर्भ

  1. ↑ De Millo, R. A.; Lipton, R. J.; Perlis, A. J. (1979). "Social processes and proofs of theorems and programs". Communications of the ACM. 22 (5): 271–280. doi:10.1145/359104.359106. S2CID 6794058.
  2. ↑ Leroy, X. (2006). "Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant". ACM SIGPLAN Notices. 41: 42–54. doi:10.1145/1111320.1111042.
  3. ↑ Leroy, Xavier (2009-12-01). "A Formally Verified Compiler Back-end". Journal of Automated Reasoning. 43 (4): 363–446. arXiv:0902.2137. doi:10.1007/s10817-009-9155-4. ISSN 0168-7433. S2CID 87730.
  4. ↑ "CompCert - The CompCert C compiler". compcert.inria.fr. Retrieved 2017-07-21.
  5. ↑ "CakeML: A Verified Implementation of ML".
  6. ↑ Stephan Diehl, Natural Semantics Directed Generation of Compilers and Abstract Machines,Formal Aspects of Computing, Vol. 12 (2), Springer Verlag, 2000. doi:10.1007/PL00003929
  7. ↑ Pnueli, Amir; Siegel, Michael; Singerman, Eli. Translation Validation. Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS '98.
  8. ↑ Compilers: Principles, Techniques and Tools, infra 1986, p. 731.
  9. ↑ ibid, 2006, p. 16.
  10. ↑ Christopher Fraser; David Hanson (1995). A Retargetable C compiler: Design and Implementation. Benjamin/Cummings Publishing. ISBN 978-0-8053-1670-4., pp. 531–3.
  11. ↑ Mark W. Bailey; Jack W. Davidson (2003). "Automatic Detection and Diagnosis of Faults in Generated Code for Procedure Calls" (PDF). IEEE Transactions on Software Engineering. 29 (11): 1031–1042. CiteSeerX 10.1.1.15.4829. doi:10.1109/tse.2003.1245304. Archived from the original (PDF) on 2003-04-28. Retrieved 2009-03-24., p. 1040.
  12. ↑ E.g., Christian Lindig (2005). "Random testing of C calling conventions" (PDF). Proceedings of the Sixth International Workshop on Automated Debugging. ACM. ISBN 1-59593-050-7. Archived from the original (PDF) on 2011-07-11. Retrieved 2009-03-24., and Eric Eide; John Regehr (2008). "Volatiles are miscompiled, and what to do about it" (PDF). Proceedings of the 7th ACM international conference on Embedded software. ACM. ISBN 978-1-60558-468-3. Retrieved 2009-03-24.
  13. ↑ Flash Sheridan (2007). "Practical Testing of a C99 Compiler Using Output Comparison" (PDF). Software: Practice and Experience. 37 (14): 1475–1488. arXiv:2202.07390. doi:10.1002/spe.812. S2CID 9752084. Retrieved 2009-03-24. Bibliography at "Compiler Testing Bibliography". Retrieved 2009-03-13..
  14. ↑ "Source of Fortran validation suite". Retrieved 2011-09-01.
  15. ↑ "Source of Cobol validation suite". Retrieved 2011-09-01.
  16. ↑ Chen, Yang; Groce, Alex; Zhang, Chaoqiang; Wong, Weng-Keen; Fern, Xiaoli; Eide, Eric; Regehr, John (2013). Taming Compiler Fuzzers. Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '13. New York, NY, USA: ACM. pp. 197–208. CiteSeerX 10.1.1.308.5541. doi:10.1145/2491956.2462173. ISBN 9781450320146. S2CID 207205614.
  17. ↑ Regehr, John; Chen, Yang; Cuoq, Pascal; Eide, Eric; Ellison, Chucky; Yang, Xuejun (2012). Test-case Reduction for C Compiler Bugs. Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '12. New York, NY, USA: ACM. pp. 335–346. doi:10.1145/2254064.2254104. ISBN 9781450312059. S2CID 1025409.
Retrieved from "https://alpha.indicwiki.in/index.php?title=संकलक_शुद्धता&oldid=120902"