Preface

Software is increasingly being used in applications where failure could result in injury or loss of life, significant damage to equipment, severe financial loss, or environmental damage. These applications continue to grow in size and complexity, increasing the risk of such failures.

High level languages are often not trusted for these critical applications: they can have complex features that are difficult to understand, and their compilers are not developed to the high degree of assurance required. Thus critical applications tend to be coded in assembly language. But as these applications grow in size using assembly language becomes infeasible; high level languages will have to be used.

To obtain an acceptable level of assurance for a high integrity compiler, it is necessary to have a mathematical specification of the source and target languages, and a formal development of the compiler that translates between them. In this book I illustrate a route for achieving a high integrity compiler by means of a small case study. Note that this is not a book about classical compiler development, and so some topics, perhaps surprisingly at first sight, are not covered. There is no treatment of parsing, nor of optimization, for example. The former is a well-understood and solved problem, adequately addressed elsewhere. The latter is not appropriate in high integrity applications, where a clear and traceable link between source code and target code is required for validation.

Part I introduces the problems posed by the requirement for high integrity compilation, and overviews a route to developing such a compiler. Part II specifies a small example language for which the case study compiler, and three static checkers, are developed. Part III specifies the target language and the compiler itself, proves that the compiler's specification correctly implements the high level language semantics, and describes a means of directly implementing the specification to produce an executable compiler. Part IV winds up the discussion by describing the extra components needed for producing a high integrity compiler for a full high level language, and evaluating the proposed approach.

The method for developing a high integrity compiler outlined in this book makes use of many concepts and notations from computer science, including denotational semantics, the Z formal specification language, and the Prolog programming language. Because of this, there is no way the discussion can be stand-alone: it would have to be the size of three tutorial books before I could start talking about high integrity compilers. There are many tutorials on these subjects available, however, and I provide appropriate references to them. Rather than scattering follow-up references throughout the text, I gather them together at the end of relevant chapters, in `further reading' sections. This book has evolved from a study originally carried out by Logica into implementation techniques that could be used to build a trustworthy Spark compiler for the formally developed Viper microprocessor. The study was commissioned by RSRE (the Royal Signals and Radar Establishment, which has lately metamorphosed into DRA Malvern), and I would like to thank the staff of RSRE for their input to that early work. In particular, detailed technical assistance was provided by John Kershaw, Clive Pygott and Ian Currie, and technical background was provided by Nic Peeling and Roger Smith. That early work was reported in [Stepney et al . 1991] .

I would like to thank David Brazier, Jon Brumfitt, David Cooper, Mike Flynn, Colin Grant, Tim Hoverd, Ian Nabney and Dave Whitley of Logica for helpful discussions, and for careful reading of various versions of this work. I would also like to thank the anonymous referees, whose detailed comments helped me to clarify and expand the exposition in places. Last but not least, my thanks also to Helen Martin of Prentice Hall for her encouragement and patience, and to Logica management for providing much of the support, both moral and financial, that enabled me to write this book.