High Integrity Compilation : a case study
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.
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.
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.
Specify a denotational semantics for the target language.
Specify an operational semantics of the source language as code
templates in the target language. This specification is an algorithm for
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.
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
The high level source language must have a target-independent
. 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.
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.
The target language must also have a mathematically defined
. The denotational semantics definition of Aida is a
The compiler ... must be correct
. Each Aida template has been
proved to have the same meaning as the corresponding Tosca statement.
[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
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.
The semantics ... must be made available for peer review and
. 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