This book presents the verified design of a code generator translating a prototypic real-time programming language to an actual microprocessor, the Inmos Transputer. Unlike most other work on compiler verification, and with particular emphasis on modularity, it systematically covers correctness of translation down to actual machine code, a necessity in the area of safety-critical systems. The formal framework provided as well as the novel proof-engineering ideas incorporated in the verified code generator are also of relevance for software design in general.
Author(s): Markus Müller-Olm (auth.)
Series: Lecture Notes in Computer Science 1283
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1997
Language: English
Pages: 260
Tags: Programming Languages, Compilers, Interpreters; Software Engineering; Logics and Meanings of Programs; Special Purpose and Application-Based Systems
Introduction....Pages 1-7
Complete Boolean lattices....Pages 9-14
Galois connections....Pages 15-22
States, valuation functions and predicates....Pages 23-38
The algebra of commands....Pages 39-83
Communication and time....Pages 85-104
Data refinement....Pages 105-111
Transputer base model....Pages 113-125
A small hard real-time programming language....Pages 127-134
A hierarchy of views....Pages 135-178
Compiling-correctness relations....Pages 179-187
Translation theorems....Pages 189-214
A functional implementation....Pages 215-231
Conclusion....Pages 233-237
