Relational semantics for locally nondeterministic programs

Introducing nondeterministic operators in a conventional deterministic language gives rise to various semantic difficulties. One of the problems is that there has been no semantic domain that is wholly satisfactory for denoting nondeterministic programs. In this paper, we propose an approach based on relational algebra. We divide the semantics of a nondeterministic program into two parts. The first part concerns the angelic aspect of programs and the second part concerns the demonic aspect of programs. Because each semantic function used in these parts is monotonic with respect to an ordering on relations, the existence of the fixed points of recursively defined nondeterministic programs is ensured.