Referential Opacity In Nondeterministic Data Refinement^{∗}

Xiaolei Qian and Allen Goldberg^{†} Kestrel Institute

August 3, 1992

Abstract

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 well-defined 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 Refinement, Nondeterminism, Program Transformation, Referential Transparency, Theory Morphism

∗ This work was supported in part by Rome Laboratories under contract F30602-86-C-0026, and in part by DARPA and Rome Laboratories under contract F30602-91-C-0092.

† Xiaolei Qian is with Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025; Allen Goldberg is with Kestrel Institute, 3260 Hillview Avenue, Palo Alto, CA 94304.

1 Introduction

Data refinement is the transformation in a program of one data type to another. Data refinement has been approached by formalizing the semantics of abstract data types by initial algebras[6], data type specifications by algebraic theories in equational logic[1], and (correct) data refinements by theory morphisms[5, 10]. Such formalization has the nice property that, assuming abstract data type A is refined to abstract data type B, replacing A by B in program P preserves the correctness of P [4].

Nondeterminism provides a convenient vehicle to avoid specifying all details of an implementation prematurely. The stepwise refinement of a specification to an implementation can be viewed as a process in which nondeterminism is gradually removed by making design decisions[12]. The semantics of nondeterministic data types has been formalized as multi-algebras[7, 9], which essentially avoids nondeterminism by encapsulating it through the medium of set construction. However, the straightforward formulation of nondeterministic data type specifications as algebraic theories in equational logic makes many desirable data refinements impossible to prove correct.

Consider for example the refinement of set to sequence[3]. It is desirable to refine equality of set not to equality of sequence but to an equivalence relation of sequence, in which sequences that are permutations of the same set are equivalent. Meanwhile, it is also desirable to refine the nondeterministic choose operator of set, which chooses an element from a nonempty set, to the head operator of sequence, which takes the first element of a nonempty sequence. Obviously these two data refinements cannot coexist in the presence of referential transparency: x = y → choose(x) = choose(y).

Data refinements are often specified as refinement rules, which are formalized as equations in data type specifications. For example, we would like to have a conditional refinement rule in our specification of set: x ≠ {}: choose(x∪y) ⟹ choose(x). Assuming both S and S′ are nonempty, we would have choose(S ∪ S′) ⟹ choose(S) and choose(S′ ∪ S) ⟹ choose(S′). Because of referential transparency, they lead to choose(S) = choose(S′), which is clearly undesirable.

Referential transparency and related issues were studied in detail in [11]. It was recognized in [2] that one might have to give up referential transparency in order to adequately deal with nondeterminism. There it was also suggested that a well-defined notion of refinement should be reΩexive, transitive, and such that all constructs are monotonic with respect to it. Meseguer observed in [8] that term rewriting should not be formalized in equational logic for applications such as nondeterministic data types, concurrent systems, and object-oriented computation.

The rest of the paper is organized as follows. In Section 2, we propose an alternative formalization of nondeterministic data types in which referential transparency applies only to deterministic operators. We show in Section 3 how various desirable data refinements can be proved correct with our approach, and in Section 4 how a well-defined notion of refinement can be incorporated into the formalism. Section 5 concludes the paper.

2 Nondeterministic Data Types

A signature Σ is a pair ⟨S, Ω⟩, where S is a set of sort symbols and Ω is a family of finite disjoint sets {Ω_{v,s}}_{v∈S^{∗},s∈S} of operator symbols. Ω is divided into two disjoint families Ω^{d} and Ω^{n}. Operator symbols in Ω^{d} are deterministic, while operator symbols in Ω^{n} are nondeterministic. We write f: v → s to denote v ∈ S^{∗}, s ∈ S, and f ∈ Ω_{v,s}. Let bool be the sort symbol for truth values, Ω_{v,bool} is a set of predicate symbols for v ∈ S^{∗}. For every sort s ∈ S we assume that there is an (infix) predicate symbol =_{s}∈ Ω_{s,s,bool}. The logical connectives ∨, ∧, ¬, →, ↔ are treated as boolean operator symbols.

For signature Σ = ⟨S, Ω⟩, the Σ-terms are defined inductively as the well-sorted composition of variables and operator symbols in Ω. A Σ-term t is deterministic if all operator symbols in t are from Ω^{d}. Otherwise t is nondeterministic. A Σ-formula is a formula built from Σ-terms and quantifiers ∀ and ∃. A Σ-sentence is a closed Σ-formula.

Let Σ = ⟨S, Ω⟩ be a signature. A Σ-algebra A is an S-indexed family of carrier sets A = {A_{s}}_{s∈S}, a function f_{A}: A_{v_{1}} × ⋯ × A_{v_{n}} → A_{s} for every f ∈ Ω_{v,s}^{d}, and a function f_{A}: A_{v_{1}} × ⋯ × A_{v_{n}} → P(A_{s}) for every f ∈ Ω_{v,s}^{n}, where v = ⟨v_{�}, …, v_{n}⟩ and P(A_{s}) denotes the set of nonempty subsets of A_{s}.

A nondeterministic data type T is a pair ⟨Σ, Φ⟩, where Σ = ⟨S, Ω⟩ is a signature and Φ is a set of Σ-sentences called axioms. For every sort s ∈ S we assume that the following equality axioms are in Φ:

1. ReΩexivity (∀x)(x =_{s} x)

2. Symmetry (∀x, y)(x =_{s} y → y =_{s} x)

3. Transitivity (∀x, y, z)(x =_{s} y ∧ y =_{s} z → x =_{s} z)

4. Monotonicity For f ∈ Ω_{v,s}^{d} where v = ⟨v_{�}, …, v_{i}, …, v_{n}⟩,

(∀x, y, z_{�}, …, z_{i−�}, z_{i��}, …, z_{n}) (x =_{v_{i}} y → f(z_{�}, …, z_{i−�}, x, z_{i��}, …, z_{n}) =_{s} f(z_{�}, …, z_{i−�}, y, z_{i��}, …, z_{n}))

The monotonicity axiom schemata applies only to deterministic operators, meaning that we do not enforce referential transparency on nondeterministic operators. A T -model is a Σalgebra that satisfies the axioms of T. A Σ-sentence p is a T -theorem, denoted as T ⊧ p, if p is a logical consequence of the axioms of T. T -theory is the set of T -theorems. As examples, the following are the specifications of two nondeterministic data types: set and seq, both of which take atom as a parameter data type with sort atom and operator f( ): atom → atom. set(atom) =^{���}(sorts set

deterministic operators {}: → set ∘ : atom, set → set ∈ : atom, set → bool apply^{f}( ): set → set

nondeterministic operators choose( ): set → atom axioms ¬(a ∘ S = {})

a ∘ (b ∘ S) = b ∘ (a ∘ S)
a ∘ (a ∘ S) = a ∘ S
¬(a ∈ {})
a ∈ (b ∘ S) ↔ a = b ∨ a ∈ S
apply^{f}({}) = {}
apply^{f}(a ∘ S) = f(a) ∘ apply^{f}(S)
¬(S = {}) → choose(S) ∈ S)

seq(atom) =^{���}(sorts seq

deterministic operators [ ]: → seq ∘ : atom, seq → seq head( ): seq → atom ∈ : atom, seq → bool apply^{f}( ): seq → seq

axioms ¬(a ∘ Q = [ ]) a ∘ Q = b ∘ Q′ → a = b ∧ Q = Q′ head(a ∘ Q) = a ¬(a ∈ [ ]) a ∈ (b ∘ Q) ↔ a = b ∨ a ∈ Q apply^{f}([ ]) = [ ] apply^{f}(a ∘ Q) = f(a) ∘ apply^{f}(Q))

The intuition behind the nondeterministic choose operator of set is that it can be referentially opaque. We do not expect that choose(S) computes a specific element of S, nor that choose(S) always computes the same element of S. All we require about choose is given by the last axiom of set.

3 Data Refinement

A signature morphism σ: Σ → Σ′, where Σ = ⟨S, Ω⟩ and Σ′ = ⟨S′, Ω′⟩, is a pair ⟨δ, θ⟩ where δ: S → S′ is a map and θ is a family of maps {θ_{v,s}: Ω_{v,s} → Ω′_{δ^{∗}�v�,δ�s�} }_{v∈S^{∗},s∈S} where δ^{∗}(⟨v_{�}, …, v_{n}⟩) denotes ⟨δ(v_{�}), …, δ(v_{n})⟩ for v_{�}, …, v_{n} ∈ S. We write σ(s) for δ(s), σ(v) for δ^{∗}(v), and σ(f) for θ_{v,s}(f) where f ∈ Ω_{v,s}. Given a Σ-formula p, σ(p) denotes the Σ′- formula resulted from replacing every operator symbol f in p by σ(f). An obvious signature morphism from set to seq is:

{set ↦ seq, {} ↦ [ ], ∘_{set} ↦ ∘_{seq}, ∈_{set}↦∈_{seq}, apply_{set}^{f} ↦ apply_{seq}^{f}, =_{set}↦=_{seq}, choose ↦ head}

Let T = ⟨Σ, Φ⟩ and T′ = ⟨Σ′, Φ′⟩ be two nondeterministic data types, and σ: Σ → Σ′ be a signature morphism. We say that σ is a data refinement from T to T′ if T′ ⊧ σ(A) for every axiom A ∈ Φ. Apparently the above signature morphism from set to seq is not a data refinement, because seq |̸= a ∘ (a ∘ Q) = a ∘ Q.

Suppose T_{�}, T_{�} are two nondeterministic data types with equality predicates =_{�}, =_{�} respectively. In refining T_{�} to T_{�}, a critical decision is how to refine equality. There are two possible ways that =_{�} can be refined through signature morphism σ.

1. If σ(=_{�}) is =_{�}, then we are often forced to require more knowledge from T_{�}. Moreover, it might add too much detail that prohibits certain efficient implementations. For example, if σ(=_{set}) is =_{seq}, then σ(∘_{set}) cannot be ∘_{seq}. We might require that there is a total ordering ≤ on atom, and build into seq an (ordered) insert operator ⋄ : atom, seq → seq defined by:

a ⋄ [ ] = a ∘ [ ]
a ⋄ (a ∘ Q) = a ∘ Q
a < b → a ⋄ (b ∘ Q) = a ∘ (b ∘ Q)
b < a → a ⋄ (b ∘ Q) = b ∘ (a ⋄ Q)

Now σ(∘_{set}) can be ⋄. This implementation represents every set as an ordered sequence with no duplicate atoms. It is more efficient when =_{set} is used more frequently than ∘_{set}.

2. If σ(=_{�}) is ≈ different from =_{�}, then ≈ must be logically weaker than =_{�}, namely for all x, y we have x =_{�} y implies x ≈ y, because ≈ must satisfy all the equality axioms. The refinement of =_{�} is underspecified: every object of T_{�} is refined to a group of objects of T_{�} not distinguishable under ≈. This delay of implementation decisions is essential in keeping more implementation options available. For example, we might build into seq a range containment predicate ⊑ : seq, seq → bool and a range equality predicate =_{r} : seq, seq → bool defined by:

[ ] ⊑ Q
a ∘ Q ⊑ Q′ ↔ a ∈ Q′ ∧ Q ⊑ Q′
Q =_{r} Q′ ↔ Q ⊑ Q′ ∧ Q′ ⊑ Q

Now σ(=_{set}) can be =_{r}, and σ(∘_{set}) can be ∘_{seq}. This implementation represents every set by a group of sequences not distinguishable under =_{r}: these sequences all contain the same set of atoms. It is more efficient when ∘_{set} is used more frequently than =_{set}.

Suppose T_{�} has a nondeterministic operator f: v → s. Another critical decision is how to refine f such that the right amount of nondeterminism is removed from T_{�}.

1. We might refine f to a nondeterministic operator. For example, we might build into seq a nondeterministic operator choose_{seq}( ): seq → atom defined by

¬(Q = [ ]) → choose(Q) ∈ Q

and refine choose_{set} to it. Since data refinement can be viewed as the gradual removal of nondeterminism, this refinement causes unnecessary delay of implementation decisions.

2. We might refine f to a deterministic operator. For example, if there is a min operator on atom, we might build into seq a select (minimum) operator select( ): seq → atom defined by

select(a ∘ [ ]) = a
select(a ∘ (b ∘ Q)) = min(a, select(b ∘ Q))

and refine choose_{set} to it. This implementation represents arbitrary selection in a set by the selection of the minimal element of a sequence, which is linear in the size of the sequence. It destroys the Ωexibility about choose in set by having the implementation of choose(S) computes a definite and specific element of S. Alternatively, we might refine choose to head, which is a constant-time operation that preserves the Ωexibility about choose in set.

If referential transparency is enforced on nondeterministic operators however, certain desirable refinement combinations of equality and nondeterministic operators become incorrect. In general, if σ(=_{v}) is ≈ weaker than =_{σ�v�}, f: v → s, and σ(f) is deterministic, then σ(f) has to satisfy the additional requirement that x ≈ y → σ(f)(x) =_{σ�s�}σ(f)(y). For example, with referential transparency enforced on choose_{set}, the following signature morphism from set to seq is not a data refinement, since seq |̸= Q =_{r} Q′ → head(Q) = head(Q′).

{set ↦ seq, {} ↦ [ ], ∘_{set} ↦ ∘_{seq}, ∈_{set}↦∈_{seq}, apply_{set}^{f} ↦ apply_{seq}^{f}, =_{set}↦=_{r}, choose ↦ head}

Under our approach where nondeterministic operators are referentially opaque, it is easy to verify that the above signature morphism is indeed a data refinement. It does not require additional knowledge on atom such as a total ordering or a min operator, and it provides constant-time implementation for both ∘_{set} and choose_{set}. The combination of =_{r} and head operators in seq captures the essence of nondeterministic behavior exhibited by = and choose operators in set.

4 Refinement Predicate

To capture the notion of refinement rules in nondeterministic data type refinement, we introduce a refinement predicate. Given a nondeterministic data type T = ⟨Σ, Φ⟩ where Σ = ⟨S, Ω⟩, we extend T with a refinement predicate ⇒_{s}∈ Ω_{s,s,bool} for s ∈ S. For every sort s ∈ S we assume that the following refinement axioms are in Φ:

1. ReΩexivity (∀x)(x ⇒_{s} x)

2. Transitivity (∀x, y, z)(x ⇒_{s} y ∧ y ⇒_{s} z → x ⇒_{s} z)

3. Monotonicity For f ∈ Ω_{v,s} where v = ⟨v_{�}, …, v_{i}, …, v_{n}⟩,

(∀x, y, z_{�}, …, z_{i−�}, z_{i��}, …, z_{n}) (x ⇒_{v_{i}} y → f(z_{�}, …, z_{i−�}, x, z_{i��}, …, z_{n}) ⇒_{s} f(z_{�}, …, z_{i−�}, y, z_{i��}, …, z_{n}))

4. Equality For deterministic Σ-terms t, t′,

t ⇒_{s} t′ → t =_{s} t′

Compared with the equality axioms of Section 2, the monotonicity axiom schemata applies to nondeterministic as well as deterministic operators. The last axiom says that the refinement predicate is stronger than the equality predicate in nondeterministic data types: there are nondeterministic Σ-terms t, t′ such that t ⇒_{s} t′ but ¬(t =_{s} t′). In the special case of deterministic data types, the last axiom implies that the refinement predicate is equivalent to the equality predicate, which corresponds to rewriting in equational logic.

A conditional refinement rule ϕ: t ⟹ t′ in the refinement of nondeterministic data type T = ⟨Σ, Φ⟩, where ϕ is a Σ-formula and t, t′ are Σ-terms, is expressed by a (universally quantified) Σ-sentence p of the form ϕ → t ⇒ t′. The refinement of T by this rule is a nondeterministic data type T′ = ⟨Σ, Φ′⟩ where Φ′ = Φ ∪ {p}. Conditional refinement rules can be used both to reduce nondeterminism and to obtain optimal implementation of nondeterministic data types. As an example, we can refine set by the following conditional refinement rules:

¬(S = {}): choose(S ∪ S′) ⟹ choose(S)
¬(S = {}): choose(apply^{f}(S)) ⟹ f(choose(S))

The resulting nondeterministic data type set′ contains the following two axioms in addition to axioms of set:

¬(S = {}) → choose(S ∪ S′) ⇒ choose(S)
¬(S = {}) → choose(apply^{f}(S)) ⇒ f(choose(S))

Compared with set, set′ has a reduced degree of nondeterminism and is more efficient in computation. The refinement predicate is stronger than the equality predicate, because from S = S′ we cannot infer choose(S) = choose(S′) (choose is referentially opaque), but from S ⇒ S′ we can infer choose(S) ⇒ choose(S′). Notice that such a refinement is not semantically sound if nondeterministic operators are referentially transparent. As an example, suppose choose is referentially transparent, and we have in set a union operator ∪ : set, set → set such that

{} ∪ S′ = S′
(a ∘ S) ∪ S′ = a ∘ (S ∪ S′)

¿From S ∪ S′ = S′ ∪ S, we infer by the monotonicity axiom choose(S ∪ S′) = choose(S′ ∪ S). Applying the first conditional refinement rule we get ¬(S = {})∧¬(S′ = {}) → choose(S) = choose(S′), which leads to the collapse of the carrier set A_{atom} to a single element in any set′- model, since from ¬(a ∘ {} = {}) and ¬(b ∘ {} = {}), we infer choose(a ∘ {}) = choose(b ∘ {}) and hence a = b.

5 Conclusion

The refinement of nondeterministic data types is a process which gradually removes nondeterminism by making design decisions that lead to an efficient implementation. However, with the specification of nondeterministic data types formalized in equational logic, many desirable refinements become impossible to prove correct. Nondeterminism often has to be removed entirely in one refinement step, rather than gradually through many refinement steps. This problem is caused by the requirement of referential transparency imposed on nondeterministic operators.

We proposed an alternative formalization of nondeterministic data types, which imposes the requirement of referential transparency only on deterministic operators. With this approach, we can easily show the correctness of many desirable refinements. Moreover, a welldefined notion of refinement can be built into nondeterministic data types as a refinement operator. Using such an operator, the gradual removal of nondeterminism can be formulated as conditional refinement rules, whose stepwise application leads to efficient implementation.

Acknowledgement

We thank Lee Blaine for our collaboration on the DTRE program transformation system, which has been a source of inspiration for the ideas presented here. The first author also thanks Peter Ladkin and José Meseguer for helpful discussions.

References

[1] Bidoit, M., Kreowski, H.-J., Lescanne, P., Orejas, F., Sannella, D., “Algebraic System Specification and Development”; Lecture Notes in Computer Science 501, Springer-Verlag, 1991.

[2] Bird, R., Meetens, L., Wile, D., “A Common Basis for Algorithmic Specification and Development”; Technical Report CS-N8702, Center for Mathematics and Computer Science, Amsterdam, April 1987, 89-100.

[3] Blaine, L., Goldberg, A., “DTRE — A Semi-Automatic Transformation System”; Constructing Programs from Specifications, B. Möller (editor), North-Holland, 1991, 165-204.

[4] Broy, M., Möller, B., Pepper, P., “Algebraic Implementations Preserve Program Correctness”; Science of Computer Programming 7, 1986, 35-53.

[5] Goguen, J.A., Thatcher, J.W., Wagner, E.G., “An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types”; Current Trends in Programming Methodology, Vol.4: Data Structuring, R.T. Yeh (Editor), Prentice-Hall, 1978, 80-149.

[6] Guttag, J.V., Horning, J.J., “The Algebraic Specification of Abstract Data Types”; Acta Informatica 10, 1978, 27-52.

[7] Hesselink, W., “A Mathematical Approach to Nondeterminism in Data Types”; ACM Transactions on Programming Languages and Systems 10:1, January 1988, 87-117.

[8] Meseguer, J., “Conditional Rewriting Logic as a Unified Model of Concurrency”; Theoretical Computer Science 96, 1992, 73-155.

[9] Nipkow, T., “Non-deterministic Data Types: Models and Implementations”; Acta Informatica 22, 1986, 629-661.

[10] Sannella, D., Tarlecki, A., “Toward Formal Development of Programs from Algebraic Specifications: Implementations revisited”; Acta Informatica 25, 1988, 233-281.

[11] Søndergaard, H., Sestoft, P., “Referential Transparency, Definiteness and Unfoldability”; Acta Informatica 27, 1990, 505-517.

[12] Turski, W., Maibaum, T., The Specification of Computer Programs, Addison-Wesley, 1987.