Report Number: CSL-TR-95-664
Institution: Stanford University, Computer Systems Laboratory
Title: Nondeterministic Operators in Algebraic Frameworks
Author: Meldal, Sigurd
Author: Walicki, Michal Antonin
Date: March 1995
Abstract: A major motivating force behind research into abstract data types is the realization that software should be described in an abstract manner - on the one hand leaving open decisions regarding further refinement and on the other allowing for substitutivity of modules as long as they satisfy a particular specification. The use of nondeterministic operators is a useful abstraction tool: nondeterminism represents a natural abstraction whenever there is a hidden state or other components of a system description which are, methodologically, conceptually or technically, inaccessible at a particular level of specification granularity. In this report we explore the various approaches to dealing with nondeterminism within the framework of algebraic specifications. The basic concepts involved in the study of nondeterminism are introduced. The main alternatives for the interpretation of nondeterministic operations, homomorphisms between nondeterministic structures and equivalence of nondeterministic terms are sketched, and we discuss various proposals for initial and terminal semantics. We offer some comments on the continuous semantics of nondeterminism and the problem of solving recursive equations over signatures with binary nondeterministic choice. We also present the attempts at reducing reasoning about nondeterminism to reasoning in first order logic, and present a calculus dealing directly with nondeterministic terms. Finally, rewriting with nondeterminism is discussed: primarily as a means of reasoning, but also as a means of assigning operational semantics to nondeterministic specifications.
http://i.stanford.edu/pub/cstr/reports/csl/tr/95/664/CSL-TR-95-664.pdf