While-programs with nondeterministic assignments and the logic ALNA (Q1082808)

In this paper, unbounded countable nondeterminism, allowed by adding nondeterministic assignments to while-programs, is studied. First, their semantical properties that are expressible in the language of ALNA (Algorithmic Logic for while-programs with Nondeterministic Assignments) are considered. Wellfoundedness as well as bounded and unbounded nondeterminism for the considered class of programs are shown to be expressible in the language of ALNA. A characterization of the wellfounded while computation trees is obtained via a notion of approximation by computation trees of suitable if-then-else-programs. No use of ordinals has been necessary to that aim. The logic ALNA is proved to be sound and complete.