An Operational Semantics for Bonded Nondeterminism Equivalent to a Denotational One

摘要

Dyadic nondeterministic choice is added to the programming language with recursive procedures used in de Bakker's monograph on program correctness. This leads to considerable changes in the operational semantics. The possible result of the execution of a program is no longer given as a single state, but as a set of possible states. Furthermore, the execution of a program is no longer given as a computation sequence, but as a set of possible computation sequences with tree-like properties. A natural operational semantics 0, defined by a function Comp, where Comp yields for each program R and each state sigma a set of computation sequences, characterized by Cook equations, is presented. For this set of equations, in a topological setting, the existence of a unique solution and the equivalence of the operational semantics to the usual denotational one, defined by fixed point techniques, is proved.