AbstractThe use of nondeterminism in specifications, as distinct from underspecification, is motivated by an example in the context of data refinement. A simple formalism for specifying nondeterministic data types is introduced. Its semantics is given in terms of the existing formalisms of relations, multialgebras, sets of functions and oracles by means of appropriate translation rules. Nondeterministic data refinement is studied from the syntactic and semantic perspective, and the correctness of the suggested proof obligations is proved. A more general implementation relation and parameterisation of nondeterministic data types are discussed and the standard theorems of vertical and horizontal composition are generalized to the nondeterministic case.
Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory; F.1.2 [Computation by Abstract Devices]: Modes of Computation; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages; I.1.3 [Algebraic Manipulation]: Languages and Systems
Additional Key Words and Phrases: algebraic specification, nondeterminism, data refinement, verification
Selected references
- Manfred Broy. Functional specification of time-sensitive communicating systems. ACM Transactions on Software Engineering and Methodology, 2(1):1-46, January 1993.
- Peter D. Mosses. Unified algebras and institutions. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, pages 304-312, Asilomar Conference Center, Pacific Grove, California, 5-8 June 1989. IEEE Computer Society Press.
- Michal Walicki and Sigurd Meldal. A complete calculus for the multialgebraic and functional semantics of nondeterminism. ACM Transactions on Programming Languages and Systems, 17(2):366-393, March 1995.