| Summary: | A programming language ALEPH and its compilar have been designed under the constraint of being able to derive a functional description Of the semantics of the language from the implementation. The way in which this approach developed is described, particularly the reason why it is considered as a design tool rather than a method of proving the equivalence of implementation and description. As a design tool, the approach proves to be very critical of irrational language and implementation features. The language is described informally and then an implementation for a hypothetical computin device is given, by means of a simple translator. The translator associates with each source phrase, a sequence of commands in the machine language of the hypothetical computing device. A symbolic model of this device is described and the semantics of each command in the machine language is defined as a mapping of the internal states of this model. By compounding the effect of sequences of such mappings, the effect of a translated source phrase can be obtained. The recursive nature of the syntax of ALEPH necessitates an inductive approach to this analysis, where it is proved that a phrase has a certain property whenever its component phrases have. This property guarantees the integrity of the states of the model. The derived functional description is used to answer some simple questions about ALEPH, to demonstrate its usefulness . The main problems and limitations of the approach and its possible extension are considered briefly. Appendices provide documentation of the author's experimental implementation.
|
|---|
