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 .

Table of Contents

• Preface

1. Introduction and Background
   1. Introduction
   2. Specifying a Language---by Example
   3. Using Prolog
2. Tosca---the High Level Language
   4. Tosca---Syntax
   5. A Running Example---the 'Square' Program
   6. Partitioning the Specification
   7. Tosca---States and Environments
   8. Tosca---Semantics
   9. Calculating the Meanings of Programs
3. The Correct Compiler
   10. Aida---the Target Language
   11. The Templates---Operational Semantics
   12. The 'Square' Example, Compiled
   13. The Proofs---Calculating the Meaning of the Templates
   14. The Prolog Implementation
4. Winding Up
   15. Further Considerations
   16. Concluding Remarks
5. Appendices
   1. Bibliography
   2. Recursive Definition of Loops
   3. Z's Free Type Construct
   4. Glossary of Notation

High Integrity Compilation 's publisher, Prentice Hall, have allowed it to go out of print, and have returned the publishing rights. So I have made the full text available here.

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
)