An Investigation into Different Semantic Approaches

Abstract

This paper relates several different semantic description-methods. It uses a common example-language, called SNAIL, which includes assignment, conditional command, guarded commands, WHlLE-command, INPUT/OUTPUT-commands and block-oriented declaration. First two models and two theories (taken from Hoare and Lauer) are used on SNAIL. The two models are proved equivalent and it is moreover proved that the two theories (under specified interpretations) are satisfied by the models. Secondly it is shown that these 4 semantic approaches in a very straightforward manner can be reformulated using denotational semantics as developed in Oxford by Scott and Strachey. A weakest predicate-transformer theory due to Dijkstra is introduced together with command-continuations and it is shown that there is a very strong equivalence between Dijkstra's theory and denotational continuation- semantics. Finally a machine language, called ASSLA, is defined. A compilation from SNAIL to ASSLA is given and proved correct. Then Dijkstra's theory is interpreted using SNAIL and the given compilation.