Re: Compiler Correctness

Pramod,


Here is a quotation with regard to the discussion on compiler correctness
taken out of my dissertation:
"Systematic Test of Code Generation Tools - A Test Suite-oriented Approach
for Safeguarding Model-based Code Generation"


See: http://www.ichmaschine.de/dissertation.html


Disussion on Formal Compiler Correctness (Chapter 5.1)


"The main problem is how to create a fully correct compiler such that not
only the translation function, but above all the implementation down to
binary machine code is correct with mathematical certainty. Literature has
neglected the latter problem as stated in [Gle03]. However, under realistic
conditions, the industrial benefit of the correct-by-construction approach
could not yet be shown: actually, there is no formally proven compiler in
use that has reached industrial maturity. Goos and Zimmermann [GZ00], for
instance, are stating that nobody succeeded in producing a correct compiler
for a realistic programming language for two main reasons:


- The range and precision limitations on computers were ignored.


- The formal methods chosen for describing the source and the target
language and of the intermediate languages in the compiler made the
treatment of realistic programming languages too difficult. As a
consequence, attention was restricted to relatively small programming
languages disregarding the complexities and pitfalls of realistic languages.


Further, [GZ00] also state, that the assumptions made within the translation
validation approach [PSS98a] are only sufficient for (reactive) source
programs consisting of single loops; the loop body must implement a function
from inputs to outputs; only the loop body is checked.


..."




Hope this helps...


Best regards,
Ingo Stuermer


Literature:


[Gle03]Glesner, S.: Using Program Checking to Ensure The Correctness of
Compiler Implementations, Journal of Universal Computer Science, Vol. 9 (3),
pp. 191-222, 2003.


[GZ00] Goos, G. and Zimmermann, W.: Verifying Compilers ans ASMs, Abstract
State Maschines, Lecture Notes in Computer Science, 1912:177-202, Springer,
2000


[PSS98b] Pnueli, A., Shtrichman, O. and Siegel, M.: The Code Validation Tool
(CVT): Automatic verification of a compilation process. Int. Journal on
Software Tools for Technology Transfer (STTT), Vol. 2(1), pp. 192-201, 1998.

Return to the comp.compilers page.
Search the comp.compilers archives again.