Referential opacity in nondeterministic data refinement
Xiaolei Qian, Allen Goldberg · ACM Letters on Programming Languages and Systems · 1993
Data refinement is the transformation in a program of one data type to another. With the obvious formalization of nondeterministic data types in equational logic however, many desirable nondeterministic data refinements are impossible to prove correct. Furthermore, it is difficult to have a monotonic notion of refinement. We propose an alternative formalization of nondeterministic data types, in which the requirement of referential transparency applies only to deterministic operators. We show how the above-mentioned problems can be solved with our approach. Categories and Subject Descriptions: D.2.4[Software Engineering]: Program Verification --- Correctness proofs; D.3.3[Programming Languages]: Language Constructs and Features --- Abstract data types; F.3.2[Logics and Meanings of Programs]: Semantics of Programming Languages --- Algebraic approaches to semantics General Terms: Languages, Theory, Verification Additional Key Words and Phrases: Algebraic Specification, Data Refinemen...