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 .
-- Professor Gordon A. Rose
Please note that the copyright of this work is not in the public domain. However, permission is granted to make copies of the whole work for any purpose except direct commercial gain. The copyright holder retains all other rights, including but not limited to the right to make translations and derivative works, and the right to make extracts and copies of parts of the work. Fair quotation is permitted according to usual scholarly conventions.
I have provided the text as a PDF (1435K) . This has slightly different pagination from the printed version, and has a few minor typos corrected, but is otherwise identical.
@book(SS-HIC, author = "Susan Stepney", title = "High Integrity Compilation : a case study", publisher = "Prentice-Hall", year = 1993 )