16. Concluding Remarks

16.1 Summary of the approach

In summary, the approach to building a high assurance compiler described in this book has the following steps.

1. Specify a denotational semantics for the source language. Many problems and ambiguities arising in the language definition can be resolved at this stage. This specification should include both dynamic and static semantics.
2. Write each semantics as a Prolog DCTG. Each static semantics provides the relevant checker (for example, type checker, declaration checker). The dynamic semantics provides an interpreter that can be used to provided further validation for the proposed semantics.
3. Specify a denotational semantics for the target language.
4. Specify an operational semantics of the source language as code templates in the target language. This specification is an algorithm for the compiler.
5. Calculate the meaning of these templates, using the target language semantics, to prove that they have the same meaning as the corresponding source language constructs. This proves that the proposed compiler performs a correct (meaning preserving) translation.
6. Write the operational semantics as a DCTG. This provides a compiler.

16.2 The criteria for high assurance compilation

How does this approach fit the criteria laid out for a high assurance compiler in Chapter 1 ?

1. The high level source language must have a target-independent meaning . The denotational semantics definition provides this meaning. The calculation of the meaning of a program can proceed manually from the semantics, as shown in the 'square' example of Chapter 9, or mechanically by using the target-independent interpreter.
2. The source language must have a mathematically defined semantics . The denotational semantics definition of Tosca is a mathematical definition, and hence, can be reasoned about.
3. The target language must also have a mathematically defined semantics . The denotational semantics definition of Aida is a mathematical definition.
4. The compiler ... must be correct . Each Aida template has been proved to have the same meaning as the corresponding Tosca statement.
5. [The compiler] must be written clearly, and must be clearly related to the semantics . The Prolog DCTG approach allows a clear one-to-one mapping between the mathematical definition and its implementation.
6. The target code produced by the compiler must be clear, and easily related to the source code . The template style and lack of optimization allows a clear mapping from target code to the corresponding source code. If a clearer correspondence is needed, it is a simple job to make the compiler annotate the target code.
7. The semantics ... must be made available for peer review and criticism . See the descriptions in sections 8.2--8.6 and Chapter 10.

The small languages and the compiler described in this book were developed as a prototype demonstration, and it would not be surprising if mistakes are found in either the semantics or the compiler. Indeed, since one of the aims of the approach described here is to produce a specification and implementation of sufficient clarity to facilitate the discovery of such errors, it would be disappointing if they were not discovered!