|
|
|
| | |
| Technischer Bericht| [1] | Gerhard Goos, Wolf Zimmermann, ASMs for uniform description of multistep transformations, ETH ZĂĽrich, Feb 2000.
|
Zusammenfassung A verifying compiler ensures that the compiled code is
always correct but the compiler may also terminate with an
error mesage and then fails to generate code. We argue
that with respect to compiler correctness this is the best
possible result which can be achieved in practice. Such a
compiler may even include unverified code provided the
results of such code can be proven correct independently
from how they are generated. We then show how abstract
state machines (ASMs) can be used to uniformly describe
the dynamic semantics of the programs being compiled
across the various intermediate transformation steps
occurring within a compiler. Besides being a convenient
tool for describing dynamic semantics the fact that we do
not have to switch between different descriptional methods
is found to be extremely useful.
Autoren
| | | |
