Connection between Dijkstra's Predicate-Transformers and Denotational Continuation-Semantics

Abstract

It is important to define and relate different semantic methods. In particular it is interesting to compare semantics for program- verification with those aimed for program execution. In this paper the intuitive background for a number of different semantics is given. They are all reformulated to the notation of denotational semantics and compared. It is shown that Dijkstra's weakest predicate theory is satisfied by a denotational continuation-semantics. The present paper is an improved and shortened version of DAIMI PB-61.