Open AccessAn Investigation into Different Semantic Approaches
Author(s) -
Kurt Villads Jensen
Publication year - 1976
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v5i61.6480
Subject(s) - predicate transformer semantics , computer science , programming language , denotational semantics , normalisation by evaluation , logical equivalence , denotational semantics of the actor model , principle of compositionality , equivalence (formal languages) , dijkstra's algorithm , domain theory , semantics (computer science) , semantic theory of truth , continuation , theoretical computer science , operational semantics , algebra over a field , artificial intelligence , mathematics , discrete mathematics , pure mathematics , linguistics , graph , philosophy , shortest path problem
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.