Abstract
This book illustrates a route for mathematically specifying and rigorously implementing a high assurance compiler suitable for use in developing high integrity applications. It explains the various techniques used at each stage of the development: denotational semantics, to capture the meaning of the source and target languages: Z, to specify the meanings and perform the correctness proofs; Prolog, to implement directly from the specification. It is illustrated throughout by a fully worked case study developing a compiler for a small language.
Although the case study in the book covers only a small language, the techniques described have been used to develop a compiler for a full safety critical language, including functions, procedures, modules, and separate compilation.
Although the case study in the book covers only a small language, the techniques described have been used to develop a compiler for a full safety critical language, including functions, procedures, modules, and separate compilation.
| Original language | Undefined/Unknown |
|---|---|
| Publisher | Prentice Hall |
| ISBN (Print) | 978-0-13-381039-4 |
| Publication status | Published - 1993 |