![[High Integrity Compilation]](hic2.jpg "[High Integrity Compilation]")
Susan
Stepney.
Tosca is very similar to the classic tutorial language of 'while' programs, but here much more emphasis has been placed on static semantics. Although languages almost as small as Tosca are actually used in developing some high integrity applications, the reason is not that they are particularly appropriate, but simply that larger languages are not considered safe, for the reasons outlined in Chapter 1 . Tosca is merely a first small step away from assembly language.
There are a variety of concerns that need to be addressed for developing a compiler for a 'full' language. These range from theoretical concerns about what language features should be supported, to pragmatic ones of how to manage the development process in practice. Some of these are discussed below.
Tosca lacks some of the language features needed to support good software engineering practice, and treats others in a less than satisfactory manner. Some of these are discussed below.
Note that as more sophisticated features are added, the approach of sets and partial functions taken in this book becomes inadequate. The full power of domain theory is required. However, the approach described here (separate static semantics, proof by structural induction, and implementation as a DCTG) is just as applicable in the more powerful mathematical formalism.
Data structures appropriate to the application, not to the hardware, are one of the first features that need to be supplied. More than integers and booleans are needed. Statically bounded arrays and non-recursive record structures (exactly the kind of restrictions usually required of a high integrity language) are relatively straightforward to specify and prove.
The introduction of arrays begs for the introduction of a for loop, too, to iterate over them. This is also quite straightforward: simpler than a while loop in many respects.
A good, careful, specification of the type checking semantics of record types is needed to curtail those interminable traditional discussions of whether foo and baz have the same type or not in a declaration such as
foo : record( x:int ; y:int ) ;
baz : record( x:int ; y:int ) ;
Tosca's main disadvantage is the lack of an abstraction mechanism. Procedures or functions are essential for modularizing large programs.
Most traditional books on compiler writing give informal descriptions of algorithms for compiling procedures and functions. The challenge for a high integrity compiler specifier is not only to formalize such an algorithm, but to formalize it in such a way that it is possible to prove it correct against the dynamic semantics specification.
Recursion (both in procedure calls and data structures) is usually forbidden in high integrity languages, because of the danger that an embedded processor could run out of memory during program execution. For a non-recursive language such as Tosca, it is possible to work out at compile time how much memory a program requires, and so to check that the proposed target machine has enough memory to run it.
But there are critical applications that are not embedded, and where it is perfectly allowable for them to stop and complain that they have run out of memory, provided they do not produce any partial, incorrect output. An example of such an application is a compiler for a high integrity language! Recursion is allowable (and in fact highly desirable) in a high integrity development language.
Once procedures and functions have been added to the language, separate compilation becomes a possibility. As much care needs to be taken over specifying the meaning of separate modules as on any other language feature. On the dynamic side, the initial environment can be taken as non-empty, but rather containing the relevant procedures. On the static side, careful definitions are needed to provide safe separate compilation.
From the high integrity perspective, there is an extra potential for errors introduced by separate compilation. The configuration system needs to ensure that the correct versions of modules are provided for linking. The newly needed linker needs to be proved correct, too, which can be done using the same techniques as described here for the compiler.
Tosca is small enough that the specification, proof and translation work can feasibly be done by hand. As the language grows, tool support at all stages of the process becomes imperative.
There are tools to support writing and checking Z specification. But set-based Z is not appropriate for larger languages, and so tool support for domain theory based specifications is necessary. Both the correctness proofs and the translation into executable form are highly stylized, so tool support for these should also be feasible.
Optimization can be dangerous. It can produce obscure code, and it can introduce bugs. Hence the traditional motto runs: First law of optimization: don't do it. Second law of optimization (for experts only): don't do it yet.
It is highly inadvisable to optimize the performance of the compiler. One of the requirements of the method advocated in this book is that there be a clear, visibly correct, translation from the mathematical definition of the semantics to the Prolog DCTG implementation. Optimization could only compromise this visibility.
One of the requirements for a high integrity compiler is that there be a clear mapping between each fragment of target code and its corresponding source code. This would seem to rule out optimization, which tends to obscure any such correspondence. However, the reason for this requirement is that the compiler is not trusted, and so this correspondence is required to enable an extra validation step to be performed. When the compiler can be trusted, this validation will not be required, and optimization becomes possible. All optimizations must be performed with the same care and proof work as the compiler development, to ensure that no bugs are introduced. The semantics of the language should be used to prove that any proposed optimization is a meaning preserving transform.
As stated in Chapter 1 , one issue not addressed here is the problem of how one would go about proving that a high integrity application written in the source language is itself correct. In fact, denotational semantics is not the most appropriate formalism for reasoning about the properties of a program; axiomatic semantics is a better approach.
The axiomatic semantics of a language should, however, be proved sound against the denotational semantics: that everything provable using the axiomatic semantics is in fact true. The logic for Z itself has been proved sound against its denotational semantics in such a manner.
The process of proving the compiler correct is a process of greatly increasing assurance in its correctness, not a process of providing absolute certainty. Just because the operational semantics templates have been proved correct, and the translation performed in a clear and visible manner, does not mean that the resulting compiler is infallible. There are many possible sources of bugs still around. Some of these are discussed below.
There could be an error in the proof. If a proof is done by hand, certain 'obvious' steps tend to be left out, for brevity. This could introduce an error, as could a simple mistake in copying from one line to the next. Cutting out the human step, and using a machine-based proof assistant, removes one class of errors and introduces another: there might be a bug in the proof tool. Since machine-produced proofs tend to be exceedingly long and dull (no steps are left out, and the steps tend to be smaller) there is less chance that a human reviewer might catch the error. Assurance can be increased by checking the proof produced by one tool with a separately developed tool, the hope being that if the second tool also has bugs, they might be different bugs.
There could be an error in the translation from Z to Prolog. Again, this could be due to a transcription error if done by hand, or a programming error in an automated translator. Some of the more trivial typographical errors are detected as syntax errors by the Prolog system when the compiler is run. But some errors might slip through.
There could be an error in the development environment. This includes the possibility of errors in the DCTG implementation, in the Prolog system itself, in the underlying operating system, and in the underlying hardware.
There could be an error in the formal semantics of the target microprocessor because the action of its instructions has been misunderstood, and formalized incorrectly.
The moral of this tale is that, no matter how much mathematical specification and proof is carried out, good old-fashioned testing still has a role to play. It provides yet another degree of increased assurance. But remember Dijkstra's famous aphorism: Program testing can be used to show the presence of errors, but never to show their absence!
Yet another potential source of bugs is that there could be an error in the target microprocessor so that it does not implement its specified semantics. There is a subtle difference from the last point made in the previous section, and arises from the difference between verification and validation.
Verification is the process of proving some property of a piece of mathematics, for example, that one specification is a correct refinement of another, or that a specification exhibits certain properties expressed in a theorem. Verification is a formal, mathematical process.
Validation is the process of demonstrating that a model (here assumed to be a mathematical model) has the desired properties, for example, that it suitably captures the system requirements, or adequately models the operation of a physical device. Validation is inherently informal, and cannot even in principle be a mathematical process, because it is attempting to demonstrate some correspondence between a piece of mathematics and the physical real world. It is impossible to prove a mathematical model faithfully reflects the physical system it is modelling, that is, to prove that everything that needs to be modelled has been modelled, and that what has been modelled has been done so accurately. So, to return to the example that started this discussion, it is impossible ever to prove, in the mathematical sense of the word, that a given microprocessor implements its mathematical semantics. This argument holds for any applications that interact with or control aspects of the real world. No less a person than Einstein said: As far as the laws of mathematics refer to reality, they are not certain, and as far as they are certain, they do not refer to reality. There is always a need to validate the formal mathematical specification against informal requirements or behaviour of a physical device. Validation is a fancy name for testing.
This point is laboured because there is frequently misunderstanding about what a formal specification provides. It provides greatly increased assurance, but it does not provide certainty. This is not a failing peculiar to mathematics, however. Nothing provides certainty.
A catalogue of the various tools currently available for supporting Z can be found in [Parker 1991] .
[Tennent 1991] describes how to prove the soundness of an axiomatic semantics against the denotational semantics of a programming language. [Woodcock and Brien 1992] describe a logic for Z, and discuss its soundness proofs.
For a thought-provoking argument on what constitutes a valid proof, and how much assurance the existence of a proof actually gives, see [De Millo et al . 1979] .