On denotational versus predicative semantics

摘要

Two definitions of a language of communicating programs are offered: one by denotational semantics, and one by predicative specifications. The equivalence of both definitions is established. Both partial and total correctness semantics are considered. Nondeterminism and its interaction with recursion is studied. The main contribution is a comparative study of the descriptive and the prescriptive viewpoint of program semantics.