By the same authors

High integrity compilation - a case study

Research output: Book/ReportBook



Publication details

DatePublished - 1993
PublisherPrentice Hall
Original languageUndefined/Unknown
ISBN (Print)978-0-13-381039-4


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.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations