This chapter presents a first application of programming language semantics: proving compiler correctness. To this end, we will define a small machine language based on a simple stack machine. Stack machines are common lowlevel intermediate languages; the Java Virtual Machine is one example. We then write a compiler from IMP to this language and prove that the compiled program has the same semantics as the source program. The compiler will perform a very simple standard optimization for boolean expressions, but is otherwise non-optimizing.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten