[cover] Susan Stepney.
High Integrity Compilation : a case study .

Prentice-Hall, 1993.

ISBN 0-13-381039-9



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 .

The book is very well written and I thought the asides were particularly valuable as they give the reader guidance as to why certain paths are taken (or rejected).

-- Professor Gordon A. Rose

Table of Contents

  1. Introduction and Background
    1. Introduction
    2. Specifying a Language---by Example
    3. Using Prolog
  2. Tosca---the High Level Language
    1. Tosca---Syntax
    2. A Running Example---the 'Square' Program
    3. Partitioning the Specification
    4. Tosca---States and Environments
    5. Tosca---Semantics
    6. Calculating the Meanings of Programs
  3. The Correct Compiler
    1. Aida---the Target Language
    2. The Templates---Operational Semantics
    3. The 'Square' Example, Compiled
    4. The Proofs---Calculating the Meaning of the Templates
    5. The Prolog Implementation
  4. Winding Up
    1. Further Considerations
    2. 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
)