A continuous semantics for unbounded nondeterminism

AbstractNondeterminism is introduced into an ordinary iterative programming language by treating procedure calls as nondeterministic assignment statements. The effect of such assignment statements is assumed to be determined solely by the entry-exit specifications of the corresponding procedures. The nondeterminism which this approach yields is not necessarily bounded. The paper discusses the problem of defining a denotational semantic for programming languages with this kind of, possibly unbounded, nondeterminism. As an additional constraint, the semantics is required to be continuous, in the sense that the underlying semantic algebra is continuous. It is shown how such a continuous semantics for unbounded nondeterminism can be derived from a simple operational semantics based on program execution trees