From: David Crocker (dcrocker(at)eschertech.com)
Date: Fri 23 Jan 2004 - 19:52:27 GMT
Brian, >> Interesting. What is the difference between "automatic code generation" and compiling? << *If* the model from which code is generated completely describes the required behaviours and is written in a notation with well-defined semantics, then it seems to me that there is no fundamental difference between this form of code generation and a compiler. This is one of the points I intend to make in the paper. Indeed, it can be argued that formal specification languages are the natural successor to programming languages (which in turn replaced assembly languages - even in the safety-critical community!). >> Much of the data from compilers suggests that regression testing works. In other words, immature compilers cannot be trusted! How do the providers of "automatic code generators" assure their users that their products are suitable for safety applications? << Good point. For any compiler or code generator, the more similarity there is between the semantics of the input model and the semantics of the output model, the fewer rules are needed and the easier it is to get them right. The semantics of the underlying execution models of programming languages such as Ada or C++ are very different from the machine architectures on which they execute, so it is not trivial to get the rules right (and even harder if "optimisations" are attempted). Ensuring the correctness of code generated from formal specifications can (at least in some cases) be much easier. Formal specification notations tend to be much simpler than many programming languages. Generators of code from formal specifications can also appeal to refinement rules and/or proof during the code generation process. Depending on the source and target languages, there may be many concepts (such as variables and parameters) that map very easily from one to the other, rather than having to be simulated as in a compiler. David Crocker Escher Technologies Ltd. www.eschertech.com Tel. +44(0)1252 336565 Fax +44(0)1252 320954