Compiler correctness
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.[citation needed] Techniques include developing the compiler using formal methods and using rigorous testing (often called compiler validation) on an existing compiler.
Contents
Formal methods
Lua error in package.lua at line 80: module 'strict' not found. Compiler validation with formal methods involves a long chain of formal, deductive logic.[1] 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.
A language described as a subset of C has been formally verified (although no proof was given of its connection to the C Standard), and the proof has been machine checked.[2]
Methods include model checking, formal verification, and provably correct semantics-directed compiler generation.[3]
Testing
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.[4] 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.”[5] Fraser & Hanson 1995 has a brief section on regression testing; source code is available.[6] Bailey & Davidson 2003 cover testing of procedure calls[7] A number of articles confirm that many released compilers have significant code-correctness bugs.[8] Sheridan 2007 is probably the most recent journal article on general compiler testing.[9] Commercial compiler compliance validation suites are available from ACE,[10] Perennial,[11] and Plum-Hall.[12] For most purposes, the largest body of information available on compiler testing are the Fortran[13] and Cobol[14] validation suites.
See also
- Compiler
- Verification and validation (software)
- Correctness (computer science)
- CompCert C compiler—Formally verified C compiler
- Reflections on Trusting Trust
References
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ 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.
- ↑ Lua error in package.lua at line 80: module 'strict' not found., pp. 531–3.
- ↑ Lua error in package.lua at line 80: module 'strict' not found., p. 1040.
- ↑ E.g., Lua error in package.lua at line 80: module 'strict' not found., and Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found. Bibliography at Lua error in package.lua at line 80: module 'strict' not found..
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
<templatestyles src="Asbox/styles.css"></templatestyles>
 |
This programming-language-related article is a stub. You can help Wikipedia by expanding it. |
