On semantics of nondeterministic recursive program schemes. (English) Zbl 0577.68032

Algebraic methods in semantics, Semin. Fontainebleau/France 1982, 1-33 (1985).
[For the entire collection see Zbl 0568.00021.]
In order to define the semantics of a non-deterministic recursive program scheme in the Herbrand universe considered as an ultrametric space, three different approaches are presented. The first one, called operational semantics, proceeds from Boudol’s notion of terminated computations. The second is the well-known denotational semantics, which, in this study, is defined as the greatest fixed point of a mapping. The last one is defined by delaying the interpretation of non-determinism, then computing the semantics of the deterministic scheme obtained in this way, and finally interpreting the non-deterministic choice as a union of sets of trees. These three semantics are proved to be equivalent under a natural notion of equivalence. Moreover the operational and denotational semantics are equal when the program scheme belongs to a class of programs which is larger than the class of Greibach schemes.


68Q60 Specification and verification (program logics, model checking, etc.)
68Q65 Abstract data types; algebraic specification
68Q45 Formal languages and automata
68Q55 Semantics in the theory of computing


Zbl 0568.00021