صحت کامپایلر

در رایانش، صحت کامپایلر شاخه ای از علوم کامپیوتر است که سعی دارد نشان دهد که یک کامپایلر طبق مشخصات زبان آن رفتار می کند. این تکنیک‌ها شامل توسعه کامپایلر با استفاده از روش‌های صوری و استفاده از تست دقیق (که اغلب به آن اعتبارسنجی کامپایلر گفته می شود) روی کامپایلر موجود می‌باشد.
 روش‌های صوری 
اعتبارسنجی کامپایلر با روشهای رسمی شامل زنجیره ای طولانی از منطق رسمی و استنتاجی است.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 اما از آنجا که ابزار یافتن اثبات (اثبات قضیه خودکار) در نرم‌افزار پیاده‌سازی شده و پیچیده است، احتمال بسیار بالایی وجود دارد که شامل خطا بشود. یک رویکرد استفاده از ابزاری برای اعتبارسنجی اثبات است که به دلیل اینکه خیلی ساده‌تر از یک اثبات‌کننده است، با احتمال کمتری با خطا روبرو خواهد شد.

کاملترین نمونه این رویکرد CompCert است که کامپایلر بهینه سازی شده‌ایست که به طور صوری اعتبارسنجی شده و برای یک زیر مجموعه بزرگ از C99 می‌باشد.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.1111042Leroy, Xavier (2009-12-01). "A Formally Verified Compiler Back-end". Journal of Automated Reasoning. 43 (4): 363–446. arXiv:0902.2137"CompCert - The CompCert C compiler". compcert.inria.fr. Retrieved 2017-07-21.

این روشها شامل وارسی مدل، اعتبارسنجی صوری و تولید کامپایلر معناشناخته می‌باشد.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
 آزمایش 
آزمایش بخش قابل توجهی از توسعه کامپایلر می‌باشد، که با این حال در نوشته‌ها و کتاب‌ها پوشش کمی روی آن داده می‌شود. نسخه ۱۹۸۶ کتاب Aho, Sethi & Ullman تنها یک بخش از یک صفحه به آزمایش کامپایلر اختصاص داده شده که آن هم بدون هیچ نمونه نامگذاری شده می‌باشد.Compilers: Principles, Techniques and Tools, infra 1986, p. 731.

نسخه ۲۰۰۶ این کتاب بخشی مربوط به آزمایشن دارد، اما اهمیت آن را تأکید می کند: "بهینه سازی کامپایلرها آنقدر سخت است که به جرئت می توان گفت که هیچ کامپایلر بهینه سازی شده کاملاً عاری از خطا نیست
بنابراین ، مهمترین هدف در نوشتن کامپایلر صحیح بودن آن است."ibid, 2006, p. 16.

نسخه ۱۹۹۵ کتاب Fraser & Hanson بخش مختصری از آزمون رگرسیون دارد. کد آن نیز موجود است.Christopher Fraser; David Hanson (1995). A Retargetable C compiler: Design and Implementation. Benjamin/Cummings Publishing. ISBN 978-0-8053-1670-4., pp. 531–3.

نسخه ۲۰۰۳ کتاب Bailey & Davidson تست فراخوانی رویه‌ها را پوشش میدهد.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.
تعدادی از مقالات تأیید می کنند که بسیاری از کامپایلرهای منتشر شده اشکالات قابل توجهی در صحتشان دارند.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.

نسخه ۲۰۰۷ کتاب Sheridan احتمالاً جدیدترین مقاله ژورنال در مورد آزمایش کامپایلرهای عمومی می باشد.Flash Sheridan (2007). "Practical Testing of a C99 Compiler Using Output Comparison" (PDF). Software: Practice and Experience. 37 (14): 1475–1488. doi:10.1002/spe.812. Retrieved 2009-03-24. Bibliography at "http://pobox.com/~flash/compiler_testing_bibliography.html%22 .

کامپایلرهای تجاری منطبق بر اعتبارسنجی از  "peren.com/pages/products_set.htm". Retrieved 2009-03-13.
 Solid Sands "www.solidsands.nl". Retrieved 2011-01-15. ،Perennial و Plum-Hall در دسترس هستند. برای اکثر اهداف، بزرگترین اطلاعات موجود در مورد آزمایش کامپایلرها از مجموعه های اعتبار سنجی Fortran  و Cobol در دسترس هستند.

برخی تکنیک‌های معمول دیگر برای آزمایش کامپایلرها عبارتند از فازینگ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. (که برنامه‌های تصادفی ایجاد می‌کند تا اشکالات کامپایلر را بیابد) و کاهش مورد آزمایشی (که سعی می کند یک مورد آزمایشی پیدا شده را کوچکتر کند تا فهم مشکل و آن مورد آزمایشی راحت تر باشد).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.
 جستارهای وابسته 
 کامپایلر
 اعتبار و درستی‌سنجی نرم‌افزار
 صحت (علوم کامپیوتر)
 CompCert -کامپایلر رسمی زبان C
 در پشتی در کامپایلرها
 منابع 

رده:کامپایلرسازی
رده:مقاله‌های ایجادشده توسط ایجادگر