In computing, compiler correctness is the branch of software engineering that deals with trying to show that a compiler behaves according to its language specification. Techniques include developing the compiler using formal methods and using rigorous testing (often called compiler validation) on an existing compiler.
|This section requires expansion. (March 2009)|
Compiler validation with formal methods involves a long chain of formal, deductive logic. However, since the tool to find the proof (theorem prover) is implemented in software and is complex, there is a high probability it will contain errors. One approach has been to use a tool that verifies the proof (a proof checker) which because it is much simpler than a proof-finder is less likely to contain errors.
Testing represents a significant portion of the effort in shipping a compiler, but receives comparatively little coverage in the standard literature. The 1986 edition of Aho, Sethi, & Ullman has a single-page section on compiler testing, with no named examples. The 2006 edition omits the section on testing, but does emphasize its importance: “Optimizing compilers are so difficult to get right that we dare say that no optimizing compiler is completely error-free! Thus, the most important objective in writing a compiler is that it is correct.” Fraser & Hanson 1995 has a brief section on regression testing; source code is available. Bailey & Davidson 2003 cover testing of procedure calls A number of articles confirm that many released compilers have significant code-correctness bugs. Sheridan 2007 is probably the most recent journal article on general compiler testing. Commercial compiler compliance validation suites are available from ACE, Perennial, and Plum-Hall. For most purposes, the largest body of information available on compiler testing are the Fortran and Cobol validation suites.
- Verification and validation (software)
- Correctness (computer science)
- CompCert C compiler -- Formally verified C compiler
- Reflections on Trusting Trust
- 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. doi:10.1145/359104.359106.
- Leroy, X. (2006). "Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant". ACM SIGPLAN Notices 41: 42. doi:10.1145/1111320.1111042.
- 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
- Compilers: Principles, Techniques and Tools, infra 1986, p. 731.
- ibid, 2006, p. 16.
- Christopher Fraser; David Hanson (1995). A Retargetable C compiler: Design and Implementation. Benjamin/Cummings Publishing. ISBN 0-8053-1670-1., pp. 531–3.
- Mark W. Bailey; Jack W. Davidson (2003). "Automatic Detection and Diagnosis of Faults in Generated Code for Procedure Calls". IEEE Transactions on Software Engineering 29 (11). Retrieved 2009-03-24., p. 1040.
- E.g., Christian Lindig (2005). "Proceedings of the Sixth International Workshop on Automated Debugging". ACM. ISBN 1-59593-050-7. Retrieved 2009-03-24.
|chapter=ignored (help), and Eric Eide; John Regehr (2008). "Proceedings of the 7th ACM international conference on Embedded software". ACM. ISBN 978-1-60558-468-3. Retrieved 2009-03-24.
- Flash Sheridan (2007). "Practical Testing of a C99 Compiler Using Output Comparison". 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". Retrieved 2009-03-13..
- "http://www.ace.nl/compiler/supertest.html". Retrieved 2011-01-15.
- "http://peren.com/pages/products_set.htm". Retrieved 2009-03-13.
- "http://plumhall.com/suites.html". Retrieved 2009-03-13.
- "Source of Fortran validation suite". Retrieved 2011-09-01.
- "Source of Cobol validation suite". Retrieved 2011-09-01.
|This programming language–related article is a stub. You can help Wikipedia by expanding it.|