Preface

Historical background of the DeCCo project

In 1990 we performed a study for RSRE (now QinetiQ) into how to develop a compiler for high integrity applications that is itself of high integrity. In that study, the source language was Spark, a subset of Ada designed for safety critical applications, and the target was Viper, a high integrity processor. We developed a mathematical technique for specifying a compiler and proving it correct, and developed a small proof of concept prototype. The study is described in [Stepney 1991], and the small case study is worked up in full, including all the proofs, in [Stepney 1993]. Experience of using the PVS tool to prove the small case study is reported in [Stringer-Calvert et al. 1997]. Futher developments to the method to allow separate compilation are described in [Stepney 1998].

Engineers at AWE read about the study and realised the technique could be used to implement a compiler for their own high integrity processor, called the ASP (Arming System Processor). They contacted us, and between 1992 and 2001 we used these techniques to deliver a high integrity compiler, integrated in a development and test environment, for progressively larger subsets of Pascal.

The full specifications of the final version of the DeCCo compiler are reproduced in these technical reports. These are written in the Z specification language. The variant of Z used is that supported by the Z Specific Formaliser tool [Formaliser], which was used to prepare and type-check all the DeCCo specifications. This variant is essentially the Z described in the Z Reference Manual [Spivey 1992] augmented with a few new constructs from ISO Standard Z [ISO-Z]. Additions to ZRM are noted as they occur in the text.

The Reports

The DeCCo Project case study is detailed in the following technical reports (this preface is common to all the reports)

1. Z Specification of Pasp
   The denotational semantics of the high level source language, Pasp. The definition is split into several static semantics (such as type checking) and a dynamic semantics (the meaningof executing a program). Later smeantics are not defined for those programs where the result of earlier semantics is error.
2. Z Specification of Asp, AspAL and XAspAL
   The denotational semantics of the low level target assembly languages. XAspAL is the target of compilation of an individual Pasp module; it is AspAL extended with some cross-module instructions that are resolved at link time. The meaning of these extra instructions is given implicitly by the specification of the linker and hexer. AspAL is the target of linking a set of XAspAL modules, and also the target of compilation of a complete Pasp program. Asp is the non-relocatable assembly language of the chip, with AspAL's labels replaced by absolute program addresses. The semantics of programs with errors is not defined, because these defintions will only ever be used to define the meaning of correct, compiled programs.
3. Z Specification of Compiler Templates
   The operational semantics of the Pasp source language, in the form of a set of XAspAL target language templates.
4. Z Specification of Linker and Hexer
   The linker combines compiled XAspAL modules into a single compiled AspAL program. The hexer converts a relocatable AspAL program into an Asp program located at a fixed place in memory.
5. Compiler Correctness Proofs
   The compiler's operational semantics are demonstrated to be equivalent to the source language's denotational semantics, by calculating the meaning of each Pasp construct, and the corresponding meaning of the AspAL template, and showing them to be equivalent. Thus the compiler transformation is meaning preserving, and hence the compiler is correct.
6. Z to Prolog DCTG translation guidelines
   The Z specifications of the Pasp semantics and compiler templates are translated into an executable Prolog DCTG implementation of a Pasp interpreter and Pasp-to-Asp compiler. The translation is done manually, following the stated guidelines.

Acknowledgements

We would like to thank the client team at AWE -- Dave Thomas, Wilson Ifill, Alun Lewis, Tracy Bourne -- for providing such an interesting development project to work on. We would like to thank the rest of the development team: Tim Wentford, John Taylor, Roger Eatwell, Kwasi Ametewee.

@techreport(SS-YCS-358,
  author = "Susan Stepney and Ian T. Nabney",
  title = "The {DeCCo} Project Papers I:
           {Z} Specification of {Pasp}",
  institution = "Department of Computer Science, University of York",
  number = "YCS-2002-358",
  month = jun,
  year = 2003
)

@techreport(SS-YCS-359,
  author = "Susan Stepney and Ian T. Nabney",
  title = "The {DeCCo} Project Papers II:
           {Z} Specification of {Asp}",
  institution = "Department of Computer Science, University of York",
  number = "YCS-2002-359",
  month = jun,
  year = 2003
)

@techreport(SS-YCS-360,
  author = "Susan Stepney and Ian T. Nabney",
  title = "The {DeCCo} Project Papers III:
           {Z} Specification of Compiler Templates",
  institution = "Department of Computer Science, University of York",
  number = "YCS-2002-360",
  month = jun,
  year = 2003
)

@techreport(SS-YCS-361,
  author = "Susan Stepney",
  title = "The {DeCCo} Project Papers IV:
           {Z} Specification of Linker and Hexer",
  institution = "Department of Computer Science, University of York",
  number = "YCS-2002-361",
  month = jun,
  year = 2003
)

@techreport(SS-YCS-362,
  author = "Susan Stepney",
  title = "The {DeCCo} Project Papers V:
           Compiler Correctness Proofs",
  institution = "Department of Computer Science, University of York",
  number = "YCS-2002-362",
  month = jun,
  year = 2003
)

@techreport(SS-YCS-363,
  author = "Susan Stepney",
  title = "The {DeCCo} Project Papers VI:
               {Z} to {Prolog DCTG} translation guidelines",
  institution = "Department of Computer Science, University of York",
  number = "YCS-2002-363",
  month = jun,
  year = 2003
)