Applications of Summation and Product Operators in the Refinement Calculus

Ralph-Johan Back Michael Butler Dept. of Computer Science, Åbo Akademi, Finland

                   {backrj,mbutler}@abo.fi

30 November 1994

Abstract Product and summation operators for predicate transformers were introduced by Naumann [20] and by Martin [15] using category theoretic considerations. In this paper, we formalise these operators in the higher order logic approach to the refinement calculus of [6], look at various algebraic properties of these operators, and examine several of their applications. We look at how the product operator provides a model of simultaneous execution of statements, while the summation operator provides a simple model of late binding. We also generalise the product operator slightly to form an operator that corresponds to conjunction of specifications. We show how the product operator may be used to model extension and modification operators for programs, and how a combination of the product and summation operators may be used to model inheritance in an object-oriented programming language.

1 Introduction

Dijkstra introduced weakest-precondition predicate transformers as a means of verifying total correctness properties of sequential programs [9]. In the refinement calculus of Back, Morgan, and Morris [2, 16, 18], specifications and programs are regarded uniformly as predicate transformers, and refinement laws are derived from properties of predicate transformers.

The refinement calculus provides various choice and assignment operators that are generalisations of Dijkstra’s operators, and the applications of these operators are well-known. However, the applications of an operator representing simultaneous execution of program statements are less well developed in the refinement calculus. Such an operator was introduced by Naumann [20] and by Martin [15] using category theoretic considerations. This product operator combines predicate transformers by forming the cartesian product of their state spaces. In this paper, we examine the product operator using the higherorder logic formalisation of the refinement calculus of Back & von Wright [6]. We examine various distributivity and refinement preserving properties of the operator and show that it can be used to model simultaneous execution and to extend the state spaces of statements so they can be more easily matched with other statements. We also generalise the definition of the product operator slightly to form what we call a fusion operator and show that the product operator is a special case of the fusion operator. The fusion operator can also be applied to conjoining or amalgamating specification statements.

The summation (or co-product^{1}) operator, which is the categorical dual of the product operator and combines statements by forming the disjoint union of their state spaces, is also described in [20] and [15]. The summation operator is a form of choice operator and we show that it is a special case of the existing choice operators of the refinement calculus. We show that this operator provides a simple yet powerful model of late binding, and that when combined with the product operator, provides a model of inheritance in an object-oriented programming language.

The paper is organised as follows. First the refinement calculus basics are described. Then Section 3 examines properties of the summation operator, while Section 4 examines properties of the product and fusion operators. In Section 5 we look briefly at the categorical properties of the summation and product operators. Section 6 looks at various applications of the operators including simultaneous execution, extending state spaces, late binding, and inheritance. Note that proofs are omitted here, but may be found in [3].

2 Refinement Calculus Basics

A predicate over a set of states Σ is a boolean function p : Σ → Bool which assigns a truth value to each state. The set of predicates on Σ is denoted P Σ:

P Σ ˆ= Σ → Bool.

We define the entailment ordering on predicates by pointwise extension: for p, q : P Σ,

p ≤ q ˆ= (∀σ : Σ · p σ ⇒ q σ).

The identically false predicate is denoted ⊥, and the identically true predicate is denoted ⊤. Negation, conjunction, and disjunction of (similarly-typed) predicates are defined by pointwise extension, so that, e.g.,

(p ∧ q) σ ˆ= (p σ ∧ q σ).

Predicates form a complete lattice under the entailment ordering. Conjunction and disjunction represent meet and join respectively, while ⊤ and ⊥ represent top and bottom respectively.

A relation from Σ to Γ is a function P : Σ → P Γ that maps each state σ to a predicate on Γ. We write

Σ ↔ Γ ˆ= Σ → P Γ.

This view of relations is isomorphic to viewing them as predicates on the cartesian space Σ × Γ. The domain and range of relation P, are denoted dom P and ran P respectively. Conjunction and disjunction of relations is defined pointwise, so that, e.g., (P ∧ Q) σ γ = (P σ γ) ∧ (Q σ γ). We write P; Q for the relational composition of P : Σ ↔ Γ and Q : Γ ↔ Λ, and P^{−1} for the inverse relation. For function f : Σ → Γ, we write f^{−1} for the relation (λγ · (λσ · γ = fσ)) : Γ ↔ Σ. A partial function g : Σ →_{p} Γ is a relation from Σ to Γ such that g σ γ ∧ g σ γ′ ⇒ γ = γ′.

1The direction of arrows in [20] and [15] are the reverse of what we use, so our product operator corresponds to their co-product operator, and vice versa.

A predicate transformer is a function S : P Γ → P Σ from predicates to predicates. We write,

Σ ⟼ Γ ˆ= P Γ → P Σ.

Note the reversal of Γ and Σ: program statements in the refinement calculus are identified with weakest-precondition predicate transformers that map a postcondition q : P Γ to the weakest precondition p : P Σ such that the program is guaranteed to terminate in a final state satisfying q whenever the initial state satisfies p. For program statement S : Σ ⟼ Γ, we say that S has source Σ and target Γ. Programs need not have identical initial and final state spaces, though if they do, we write S : Δ(Σ) instead of S : Σ ⟼ Σ. Note that, in order to aid intuition, we sometimes discuss commands from an operational viewpoint, though our formal reasoning is always in terms of predicate transformers.

The refinement ordering on predicates is defined by pointwise extension: for S, T : Σ ⟼ Γ,

S ≤ T ˆ= (∀q : P Γ · S q ≤ T q).

The refinement ordering on predicates models the notion of total-correctness preserving program refinement. A total-correctness specification is typically given as a precondition-postcondition pair (pre, post), and program (i.e., predicate transformer) S satisfies (pre, post) if pre ≤ (S post). Now, for programs S and T, S ≤ T holds if and only if T satisfies any specification satisfied by S.

Predicate transformers form a complete lattice under the refinement ordering. The bottom element is the predicate transformer abort that maps each postcondition to ⊥, and the top element is the predicate transformer magic that maps each postcondition to ⊤. The abort statement is never guaranteed to terminate, while the magic statement is miraculous since it is always guaranteed to establish any postcondition. A miraculous statement cannot be implemented. For statement S, halt S ˆ= S ⊤ describes those initial states under which S is guaranteed to terminate, while gd S ˆ= ¬ (S ⊥) (called guard of S) describes those initial states under which S behaves non-miraculously.

Conjunction and disjunction of (similarly-typed) predicate transformers is defined pointwise, so that, e.g., (S ∧ T) q = (S q) ∧ (T q). Conjunction of statements models demonic nondeterministic choice between executing S and T (i.e., each alternative must establish the postcondition), whereas disjunction models angelic nondeterministic choice (i.e., some alternative must establish the postcondition). If halt S = ¬ halt T, then S ∨ T becomes a deterministic choice, while if gd S = ¬ gd T, then S ∧ T becomes a deterministic choice.

Sequential composition of program statements is modelled by functional composition of predicate transformers, i.e., for S : Σ ⟼ Γ, T : Γ ⟼ Λ, p : P Λ, S; T p ˆ= S (T p). The program statement skip_{Σ} is modelled by the identity predicate transformer on P Σ.

Given a relation P : Σ ↔ Γ, the angelic update statement {P } : Σ ⟼ Γ and demonic update statement [P] : Σ ⟼ Γ are defined by

{P } q σ ˆ= (∃γ : Γ · (P σ γ) ∧ (q γ))

[P] q σ ˆ= (∀γ : Γ · (P σ γ) ⇒ (q γ)).

When started in a state σ, {P } angelically chooses a new state γ such that P σγ holds, while [P] demonically chooses a new state γ such that P σγ holds. If no such new state exists then {P } aborts, while [P] behaves as magic.

For predicate p : P Σ, let \overline{p} : Σ ↔ Σ be the corresponding test relation for p, i.e., (λσ · λσ′ · p σ ∧ σ = σ′). Then we write \{p\} for \{\overline{p}\} and [p] for [\overline{p}]. {p} models the assert statement that behaves as skip if p holds, otherwise it aborts. [p] models the guard statement that behaves as skip if p holds, otherwise it behaves as magic.

Given a function f : Σ → Γ, the deterministic update statement ⟨f⟩ : Σ ⟼ Γ is defined by

⟨f⟩ q σ ˆ= q (f σ).

Let f̃ be the the deterministic relation corresponding to function f, i.e., (λσ · λγ · f σ = γ). Then we have {f̃} = ⟨f⟩ = [f̃].

Ordinary program constructs such conditionals, recursions, and assignments may be modelled using the basic operators presented above. For example, if g then S else T fi may be modelled by [g]; S ∧ [¬ g]; T or alternatively by {g}; S ∨ {¬ g}; T. Program variables may be modelled as cartesian components of the state space, and a multiple assignment x, y := e, f in a state space with three components, representing program variables (x, y, z), may be modelled by the deterministic update:

⟨λx, y, z · (e, f, z)⟩.

It is easy to show, for predicates pre and post, that {pre}; [post] is the least statement satisfying the specification pair (pre, post). Thus, implementing the specification (pre, post) involves constructing a statement S such that {pre}; [post] ≤ S. If post is a relation rather than a predicate, we can model postconditions on the before and after states in the manner of VDM [14] and Z [22]. Rules for the stepwise refinement of specification statements of the form {pre}; [post] into more familiar program constructs may be found in [2, 16, 18].

All predicate transformers S constructed using the operators described above will be monotonic, i.e., p ≤ q ⇒ S p ≤ S q. A predicate transformer S is bottom homomorphic if S ⊥=⊥, and top homomorphic if S ⊤ = ⊤. Conjunctive predicate transformers form a subset of the monotonic predicate transformers satisfying S (∀i ∈ I · q_{i}) = (∀i ∈ I · S q_{i}), for non-empty I. S is universally conjunctive if it is conjunctive and top homomorphic. Disjunctive and universally disjunctive predicate transformers are defined dually. A predicate transformer is continuous if it is disjunctive over non-empty chains of predicates. Demonic update statements are universally conjunctive, angelic update statements are universally disjunctive, and deterministic update statements are both. The operators ∧ and ; preserve the conjunctivity of their operands, while ∨ and ; preserve the disjunctivity of their operands. Also, each of ∧, ∨, and ; preserve refinement of monotonic predicate transformers, e.g., S ≤ S′ ⇒ S; T ≤ S′; T.

In Dijkstra’s original calculus, all statements were conjunctive and nonmiraculous. Also, for conjunctive statements, disjunctivity corresponds to determinism, while continuity corresponds to bounded nondeterminism [9].

3 Summation Operators

In this section, we describe two summation operators for predicate transformers: the first only sums the operand sources, while the second sums both the operand sources and the operand targets.

The sum (or disjoint union) of two state spaces Σ_{1} and Σ_{2} is written Σ_{1} + Σ_{2}. Associated with the summation are two injections ϕ_{1} and ϕ_{2} which map elements of the base type to elements of the summation (A →_{ι} B represents the set of injective functions from A to B):

ϕ_{1} : Σ_{1} →_{ι} Σ_{1} + Σ_{2}  (1)
ϕ_{2} : Σ_{2} →_{ι} Σ_{1} + Σ_{2}.  (2)

Since any element of Σ_{1} + Σ_{2} must either come from Σ_{1} or Σ_{2}, but not both, the injections also satisfy:

(ran ϕ_{1}, ran ϕ_{2}) partition Σ_{1} + Σ_{2}.  (3)

We shall assume that all injection pairs (ϕ_{1}, ϕ_{2}) associated with summations satisfy (1), (2), and (3).

Since ϕ_{1} and ϕ_{2} are injective, their inverses ϕ_{1}^{−1} and ϕ_{2}^{−1} are partial functions:

ϕ_{1}^{−1} : Σ_{1} + Σ_{2} →_{p} Σ_{1} ϕ_{2}^{−1} : Σ_{1} + Σ_{2} →_{p} Σ_{2}.

For σ ∈ Σ_{1} + Σ_{2}, (ϕ_{1}^{−1}σ) is only defined if σ ∈ (dom ϕ_{1}^{−1}).

Summation of predicates is given by: Definition 1 For p_{1} : P Σ_{1}, p_{2} : P Σ_{2}, p_{1} + p_{2} is of type P (Σ_{1} + Σ_{2}), where for σ : Σ_{1} + Σ_{2},

(p_{1} + p_{2}) σ ˆ= σ ∈ (dom ϕ_{1}^{−1}) ∧ p_{1}(ϕ_{1}^{−1}σ) ∨ σ ∈ (dom ϕ_{2}^{−1}) ∧ p_{2}(ϕ_{2}^{−1}σ).

Given an injection ϕ_{1} : Σ_{1} →_{ι} Σ_{1} + Σ_{2}, the deterministic update

⟨ϕ_{1}⟩ : Σ_{1} ⟼ Σ_{1} + Σ_{2} ( = P (Σ_{1} + Σ_{2}) → P Σ_{1})

maps predicates in the summation type to predicates in the first base type. The updates can be used to select the components of a summation of predicates: Theorem 1 For p_{1} : P Σ_{1}, p_{2} : P Σ_{2},

⟨ϕ_{1}⟩ (p_{1} + p_{2}) = p_{1} and ⟨ϕ_{2}⟩ (p_{1} + p_{2}) = p_{2}.

The following theorem shows that a predicate in the summation type can always be separated into a summation of predicates: Theorem 2 For p : P (Σ_{1} + Σ_{2}), p = ⟨ϕ_{1}⟩ p + ⟨ϕ_{2}⟩ p.

3.1 Summation of Predicate Transformers

The summation of predicate transformers S_{1} and S_{2} is written S_{1} ⊕ S_{2}, where S_{1} and S_{2} have the same target, but possibly distinct sources: Definition 2 For S_{1} : Σ_{1} ⟼ Γ, S_{2} : Σ_{2} ⟼ Γ, S_{1} ⊕ S_{2} is of type Σ_{1} + Σ_{2} ⟼ Γ, where for q : P Γ:

(S_{1} ⊕ S_{2}) q ˆ= (S_{1} q) + (S_{2} q).

The selection and separation properties of the summation operator follow directly from Theorems 1 and 2:

Theorem 3 For S_{1} : Σ_{1} ⟼ Γ, S_{2} : Σ_{2} ⟼ Γ, S : Σ_{1} + Σ_{2} ⟼ Γ,

⟨ϕ_{1}⟩; (S_{1} ⊕ S_{2}) = S_{1} and ⟨ϕ_{2}⟩; (S_{1} ⊕ S_{2}) = S_{2}

S = ⟨ϕ_{1}⟩; S ⊕ ⟨ϕ_{2}⟩; S.

Summation of predicate transformers is a form of choice operator since the effect of executing S_{1} ⊕ S_{2} in some initial state σ depends on the base type of σ: if it is of type Σ_{1}, then S_{1} is executed, while if it is of type Σ_{2}, then S_{2} is executed. This may be seen more clearly in the following theorem where the summation operator is characterised purely in terms of the existing choice operators. The theorem uses the following angelic and demonic updates formed from the inverse injections:

{ϕ_{1}^{−1}} : Σ_{1} + Σ_{2} ⟼ Σ_{1}  [ϕ_{1}^{−1}] : Σ_{1} + Σ_{2} ⟼ Σ_{1}.

Theorem 4 For S_{1} : Σ_{1} ⟼ Γ, S_{2} : Σ_{2} ⟼ Γ,

S_{1} ⊕ S_{2} = {ϕ_{1}^{−1}}; S_{1} ∨ {ϕ_{2}^{−1}}; S_{2} = [ϕ_{1}^{−1}]; S_{1} ∧ [ϕ_{2}^{−1}]; S_{2}. It is also clear from Theorem 4 that the choice between S_{1} and S_{2} is deterministic since ϕ_{1}^{−1} and ϕ_{2}^{−1} have disjoint domains, so that

halt {ϕ_{1}^{−1}} = ¬ halt {ϕ_{2}^{−1}} and gd [ϕ_{1}^{−1}] = ¬ gd [ϕ_{2}^{−1}].

3.2 Derived Summation Operator

Next we define a summation operator on predicate transformers with distinct sources and distinct targets. Let ψ_{1} and ψ_{2} be the injections for the summation Γ_{1} + Γ_{2} (thus, e.g., ⟨ψ_{1}⟩ has type Γ_{1} ⟼ Γ_{1} + Γ_{2}). Definition 3 For S_{1} : Σ_{1} ⟼ Γ_{1}, S_{2} : Σ_{2} ⟼ Γ_{2}, S_{1} + S_{2} is of type Σ_{1} + Σ_{2} ⟼ Γ_{1} + Γ_{2}, where

S_{1} + S_{2} ˆ= S_{1}; ⟨ψ_{1}⟩ ⊕ S_{2}; ⟨ψ_{2}⟩.

The components of S_{1} + S_{2} may be selected as follows: Theorem 5 For S_{1} : Σ_{1} ⟼ Γ_{1}, S_{2} : Σ_{2} ⟼ Γ_{2},

⟨ϕ_{1}⟩; (S_{1} + S_{2}); {ψ_{1}^{−1}} = ⟨ϕ_{1}⟩; (S_{1} + S_{2}); [ψ_{1}^{−1}] = S_{1}

⟨ϕ_{2}⟩; (S_{1} + S_{2}); {ψ_{2}^{−1}} = ⟨ϕ_{2}⟩; (S_{1} + S_{2}); [ψ_{2}^{−1}] = S_{2}.

Summation distributes through sequential composition as follows: Theorem 6

(i) (S_{1} + S_{2}) ; (T_{1} ⊕ T_{2}) = (S_{1}; T_{1}) ⊕(S_{2}; T_{2}).
(ii) (S_{1} + S_{2}) ; (T_{1} + T_{2}) = (S_{1}; T_{1}) +(S_{2}; T_{2}).

In order to consider the summation of angelic and demonic updates, we require the following definition of summation of relations: Definition 4 For P_{1} : Σ_{1} ↔ Γ_{1}, P_{2} : Σ_{2} ↔ Γ_{2}, σ : Σ_{1} + Σ_{2}, γ : Γ_{1} + Γ_{2},

(P_{1} + P_{2}) σ γ ˆ= σ ∈ (dom ϕ_{1}^{−1}) ∧ γ ∈ (dom ψ_{1}^{−1}) ∧ P_{1} (ϕ_{1}^{−1}σ) (ψ_{1}^{−1}γ) ∨

σ ∈ (dom ϕ_{2}^{−1}) ∧ γ ∈ (dom ψ_{2}^{−1}) ∧ P_{2} (ϕ_{2}^{−1}σ) (ψ_{2}^{−1}γ).

Summation distributes through updates, assert and guard statements as follows: Theorem 7 For P_{1} : Σ_{1} ↔ Γ_{1}, P_{2} : Σ_{2} ↔ Γ_{2}, p_{1} : P Σ_{1}, p_{2} : P Σ_{2},

{P_{1}} +{P_{2}} = {P_{1} + P_{2}} and [P_{1}] +[P_{2}] = [P_{1} + P_{2}]  (4)
{p_{1}} +{p_{2}} = {p_{1} + p_{2}} and [p_{1}] +[p_{2}] = [p_{1} + p_{2}].  (5)

Both the summation operators preserve refinement allowing us to refine summands separately: Theorem 8

S_{1} ≤ S′_{1} ∧ S_{2} ≤ S′_{2} ⇒ (S_{1} ⊕ S_{2}) ≤ (S′_{1} ⊕ S′_{2})
T_{1} ≤ T′_{1} ∧ T_{2} ≤ T′_{2} ⇒ (T_{1} + T_{2}) ≤ (T′_{1} + T′_{2}).

4 Product Operators

The cartesian product of state spaces Σ_{1} and Σ_{2} is denoted Σ_{1} ×Σ_{2}. Given two predicates q_{1} and q_{2} their product is denoted q_{1} × q_{2} and is defined as follows: Definition 5 For q_{1} : P Σ_{1}, q_{2} : P Σ_{2}, q_{1} × q_{2} is of type P (Σ_{1} × Σ_{2}) where for σ_{1} : Σ_{1}, σ_{2} : Σ_{2},

(q_{1} × q_{2}) (σ_{1}, σ_{2}) = (q_{1} σ_{1}) ∧ (q_{2} σ_{2}).

Note that, in contrast to summation of predicates where any predicate of type P (Σ_{1} + Σ_{2}) may be represented by the summation of two predicates of types P Σ_{1} and P Σ_{2} respectively, predicates of the form q_{1} × q_{2} only form rectangular subsets of P (Σ_{1} × Σ_{2}). Also, the components of a product of predicates cannot always be selected, e.g., p_{1} cannot be retrieved from p_{1}× ⊥. As we shall see, these facts mean that the product operators for predicate transformers do not satisfy as many properties as the summation operator.

Consider the following two predicate transformers which have a common source but distinct targets:

S_{1} : Σ ⟼ Γ_{1},  S_{2} : Σ ⟼ Γ_{2}.

The product operator combines these two commands to form a command with target Γ_{1} × Γ_{2} as follows: Definition 6 For S_{1} : Σ ⟼ Γ_{1}, S_{2} : Σ ⟼ Γ_{2}, S_{1} ⊗ S_{2} is of type Σ ⟼ Γ_{1} × Γ_{2}, where for q : P (Γ_{1} × Γ_{2}):

(S_{1} ⊗ S_{2}) q ˆ= (∃q_{1} : P Γ_{1}; q_{2} : P Γ_{2} | q_{1} × q_{2} ≤ q · S_{1}q_{1} ∧ S_{2}q_{2}).

We shall see later that execution of S_{1} ⊗ S_{2} has the same effect as simultaneous execution of S_{1} and S_{2}.

Before investigating properties of the product operator further, we first look at two related operators. The first is derived from the product operator. Let π_{1} and π_{2} be the projections from Σ_{1} × Σ_{2} to Σ_{1} and Σ_{2} respectively:

\begin{matrix}π_{1} : Σ_{1} × Σ_{2} → Σ_{1}, & π_{2} : Σ_{1} × Σ_{2} → Σ_{2}, \\ π_{1}(σ_{1}, σ_{2}) = σ_{1}, & π_{2}(σ_{1}, σ_{2}) = σ_{2}. \end{matrix}

The projections give the following deterministic updates:

⟨π_{1}⟩ : Σ_{1} × Σ_{2} ⟼ Σ_{1} and ⟨π_{2}⟩ : Σ_{1} × Σ_{2} ⟼ Σ_{2}.

The statement ⟨π_{1}⟩ starts in a state (σ_{1}, σ_{2}) and ends in the state σ_{1} simply discarding the second component. The derived product operator combines commands with distinct sources and distinct targets, and is defined as follows: Definition 7 For S_{1} : Σ_{1} ⟼ Γ_{1}, S_{2} : Σ_{2} ⟼ Γ_{2}, S_{1} × S_{2} is of type Σ_{1} × Σ_{2} ⟼ Γ_{1} × Γ_{2}, where

S_{1} × S_{2} ˆ= ⟨π_{1}⟩; S_{1} ⊗ ⟨π_{2}⟩; S_{2}.

We shall see later that the derived product operator models simultaneous execution of two commands with distinct initial states and distinct final states.

Definition 6 may be generalised to define what we term a fusion operator that combines commands with common sources and common targets as follows: Definition 8 For S_{1}, S_{2} : Σ ⟼ Γ, S_{1} ⊙ S_{2} is of type Σ ⟼ Γ, where for q : P Γ:

(S_{1} ⊙ S_{2}) q ˆ= (∃q_{1}, q_{2} : P Γ | q_{1} ∧ q_{2} ≤ q · S_{1}q_{1} ∧ S_{2}q_{2}).

Neither product operator is commutative, since Σ_{1}×Σ_{2} is different to Σ_{2}×Σ_{1} when Σ_{1} and Σ_{2} are different. However, it is clear from Definition 8 that the fusion operator is commutative. We proceed by investigating further properties of the fusion operator and showing that the product operators are special cases of the fusion operator.

4.1 Properties of Fusion Operator

The fusion operator preserves refinement: Theorem 9 S_{1} ≤ S′_{1} ∧ S_{2} ≤ S′_{2} ⇒ (S_{1} ⊙ S_{2}) ≤ (S′_{1} ⊙ S′_{2}) .

A program specification takes the form {p}; [P], where p is a state predicate and P is a state relation. The following theorem provides a simple way of calculating the fusion of two such specifications: Theorem 10 For relations P, Q : Σ ↔ Γ, and predicates p, q : P Σ,

{p}; [P] ⊙ {q}; [Q] = {p ∧ q}; [P ∧ Q].

The theorem illustrates that the effect of the fusion operator is to reduce the (demonic) nondeterminism of the terminating behaviour of both commands. The theorem also illustrates that the fusion operator can be used as a (refinement preserving) way of combining program specifications.

Given a predicate transformer S : Σ ⟼ Γ, we derive a relation, called rel S, of type Σ ↔ Γ as follows:

(rel S) σ γ ˆ= ¬ S(λγ′ · γ ≠ γ′) σ.

This definition is from [10]. It can be shown that any conjunctive predicate transformer may be characterised as a specification involving halt S and rel S: Lemma 1 For conjunctive predicate transformer S, S = {halt S}; [rel S]. Using this lemma and Theorem 10, we arrive at the following theorem: Theorem 11 For conjunctive predicate transformers S and T,

S ⊙ T = { (halt S) ∧ (halt T) } ; [ (rel S) ∧ (rel T) ].

Abrial [1] describes a parallel operator for statements whose definition is similar to the right-hand side of Theorem 11. Thus our fusion of statements is similar to Abrial’s parallel composition, for conjunctive statements.

We say that two specifications {p}; [P] and {q}; [Q] are contradictory in some initial state σ if σ has a successful outcome in each specification, but does not have a successful outcome in their fusion, i.e., σ holds in p, q, dom P, and dom Q, but not in dom (P ∧ Q). For those contradictory initial states, the fusion of both specifications behaves miraculously. Ward [25] has defined a slight variant of Abrial’s parallel combinator where the combination behaves as abort when both specifications are contradictory. Thus, in Ward’s case, a contradictory combination may be refined by any statement whereas, in our case, it is unimplementable. Furthermore, Ward’s combinator is not refinement preserving.

4.2 Properties of Product Operator

Now we show that the product operator is a special case of the fusion operator. Let ϖ_{1} and ϖ_{2} be the projections from Γ_{1} × Γ_{2} to Γ_{1} and Γ_{2} respectively:

ϖ_{1} : Γ_{1} × Γ_{2} → Γ_{1},  ϖ_{2} : Γ_{1} × Γ_{2} → Γ_{2}.

The inverses of ϖ_{1} and ϖ_{2} are relations:

ϖ_{1}^{−1} : Γ_{1} ↔ Γ_{1} × Γ_{2},  ϖ_{2}^{−1} : Γ_{2} ↔ Γ_{1} × Γ_{2},

so that the demonic update [ϖ_{1}^{−1}] transforms predicates in Γ_{1}×Γ_{2} to predicates in Γ_{1}:

[ϖ_{1}^{−1}] : Γ_{1} ⟼ Γ_{1} × Γ_{2},  (= P (Γ_{1} × Γ_{2}) → P Γ_{1}),

and similarly for [ϖ_{2}^{−1}]. The command [ϖ_{1}^{−1}] starts in a state γ_{1} : Γ_{1} and ends in a state (γ′_{1}, γ′_{2}) : Γ_{1}×Γ_{2} such that γ_{1} = γ′_{1} and γ′_{2} is chosen nondeterministically. Given S_{1} : Σ ⟼ Γ_{1}, the predicate transformer S_{1}; [ϖ_{1}^{−1}] : Σ ⟼ Γ_{1} × Γ_{2} is a ‘lifted’ version of S_{1} that behaves as S_{1} on the first component of the final state, and nondeterministically writes any value to the second component. Similarly for S_{2}; [ϖ_{2}^{−1}]. Now we have: Theorem 12 For S_{1} : Σ ⟼ Γ_{1}, S_{2} : Σ ⟼ Γ_{2},

S_{1} ⊗ S_{2} = S_{1}; [ϖ_{1}^{−1}] ⊙ S_{2}; [ϖ_{2}^{−1}].

Preservation of refinement follows from Theorems 9 and 12. The product operator does not, in general, satisfy selection and separation properties, though it does satisfying the following: Theorem 13 For monotonic S_{1} : Σ ⟼ Γ_{1}, S_{2} : Σ ⟼ Γ_{2}, q : P Γ_{1},

(S_{1} ⊗ S_{2}); ⟨ϖ_{1}⟩ q = (S_{1}q ∧ S_{2}⊤) ∨ (S_{1}⊤ ∧ S_{2} ⊥).

The separation property does not hold for the product operator, though we do have the following inequality for conjunctive S: Theorem 14 For conjunctive S : Σ ⟼ Γ_{1} × Γ_{2}, S; ⟨ϖ_{1}⟩ ⊗ S; ⟨ϖ_{2}⟩ ≤ S.

Assume that for functions f_{1} : Σ → Γ_{1}, f_{2} : Σ → Γ_{2} and relations P_{1} : Σ ↔ Γ_{1}, P_{2} : Σ ↔ Γ_{2} we have:

f_{1} ⊗ f_{2} σ ˆ= (f_{1} σ, f_{2} σ)
P_{1} ⊗ P_{2} σ (γ_{1}, γ_{2}) ˆ= P_{1} σ γ_{1} ∧ P_{2} σ γ_{2}.

The product operator then combines with specification statements and deterministic updates in the following manner: Theorem 15 For p_{1}, p_{2} : P Σ, and P_{1} : Σ ↔ Γ_{1}, P_{2} : Σ ↔ Γ_{2},

{p_{1}}; [P_{1}] ⊗ {p_{2}}; [P_{2}] = {p_{1} ∧ p_{2}}; [P_{1} ⊗ P_{2}].

Theorem 16 For f_{1} : Σ → Γ_{1}, f_{2} : Σ → Γ_{2}, ⟨f_{1}⟩ ⊗ ⟨f_{2}⟩ = ⟨f_{1} ⊗ f_{2}⟩.

4.3 Properties of the Derived Product Operator

Theorem 12 shows that the derived product operator is also a special case of the fusion operator:

Theorem 17 For S_{1} : Σ_{1} ⟼ Γ_{1}, S_{2} : Σ_{2} ⟼ Γ_{2},

S_{1} × S_{2} = ⟨π_{1}⟩; S_{1}; [ϖ_{1}^{−1}] ⊙ ⟨π_{2}⟩; S_{2}; [ϖ_{2}^{−1}].

Here, the command ⟨π_{1}⟩ starts in a state (σ_{1}, σ_{2}) : Σ_{1} × Σ_{2} and ends simply in the state σ_{1}. Given S_{1} : Σ_{1} ⟼ Γ_{1}, the predicate transformer ⟨π_{1}⟩; S_{1}; [ϖ_{1}^{−1}] : Σ_{1} × Σ_{2} ⟼ Γ_{1} × Γ_{2} is a ‘lifted’ version of S_{1} that behaves as S_{1} on the first components of the before and after state, and behaves nondeterministically on the second components. Similarly for ⟨π_{2}⟩; S_{1}; [ϖ_{1}^{−1}].

The derived product operator preserves refinement and it is easy to show that it combines with specification statements and deterministic updates in a similar manner to the product operator.

5 Applications

In Section 4.1 (c.f. Theorem 10), we saw that the fusion operator corresponds to a form of conjunction operator for specifications. Here we look more closely at applications of the other operators.

5.1 Simultaneous Assignment

As mentioned in Section 2, variables may be modelled as cartesian components of the state space. We take the view that the predicate transformer S_{1} : Σ_{1} × Σ_{2} ⟼ Σ_{1} models a statement that reads from program variables x and y, and assigns a value to program variable x, while S_{2} : Σ_{1} × Σ_{2} ⟼ Σ_{2} reads from the same variables and assigns a value to y. The product S_{1} ⊗ S_{2} has type Δ(Σ_{1} × Σ_{2}) and models simultaneous assignment to x and y. For example, we have

x := f(x, y) ⊗ y := g(x, y) = ⟨λx, y · f(x, y)⟩ ⊗ ⟨λx, y · g(x, y)⟩
=  {Theorem 16}
⟨λx, y · f(x, y), g(x, y)⟩
= x, y := f(x, y), g(x, y).

If S_{1} and S_{2} read from distinct state components, i.e., S_{1} has type Δ(Σ_{1}) and S_{2} has type Δ(Σ_{2}), then their simultaneous execution is modelled by the derived product S_{1} × S_{2}. With both product operators we know that if either assignment is nonterminating, then the combined assignment is nonterminating, e.g., S_{1} ⊗ abort = abort.

The action system formalism of Back & Kurki-Suonio [4] uses predicate transformers to model parallel programs. An action system consists of an initialisation predicate transformer and a set of action predicate transformers. Execution of an action system proceeds by firstly executing the initialisation, then, repeatedly, executing an enabled action (an action A is enabled when gd A holds). Two action systems are composed in parallel by composing their initialisations such that they are executed simultaneously and forming the union of their actions. Conventionally, the initialisations are demonic updates [I_{1}], [I_{2}], and their composition is simply [I_{1} ∧ I_{2}]. The product operator provides a way of composing more general initialisations achieving the same effect.

In [8], the actions of an action system are given labels and a correspondence with Hoare’s CSP is established. A version of parallel composition of action systems is described in which commonly labelled actions from the respective action systems are composed such that they are executed simultaneously. This composition is defined by the properties that it should satisfy. One such property is that the composition should only be enabled when both actions are enabled. The product operator almost satisfies all the required properties: it fails if one of the actions can abort. However, by guarding the product of the actions as follows, we get an operator that satisfies the required properties:

A_{1}∥A_{2} ˆ= [(gd A_{1}) × (gd A_{2})] ; (A_{1} × A_{2}).

5.2 Superposition

Consider the following two predicate transformers:

S_{1} : Δ(Σ_{1}),  S_{2} : Σ_{1} × Σ_{2} ⟼ Σ_{2}.

S_{1} only operates on Σ_{1}, while S_{2} reads from Σ_{1} × Σ_{2} and writes to Σ_{2}. Superposition of S_{2} on to S_{1} allows S_{2} to add extra program variables which it writes to, as well as allowing S_{2} to read the program variables of S_{1}. Such an operation may be defined as a special case of the product operator: Definition 9 S_{1} sup S_{2} ˆ= ⟨π_{1}⟩; S_{1} ⊗ S_{2}. Here, ⟨π_{1}⟩ reads from Σ_{1} × Σ_{2} though it discards the Σ_{2} component. For example, we have:

x := f(x) sup y := g(x, y) = x, y := f(x), g(x, y).

Superposition refinement of action systems is described in [5], where superposition on individual actions is described in terms of sequential composition. Our superposition operator could be used instead.

5.3 Modification

Consider the following two predicate transformers:

S_{1} : Δ(Σ_{1} × Σ_{2}),  S_{2} : Σ_{1} × Σ_{2} ⟼ Σ_{2}.

S_{1} operates on Σ_{1} × Σ_{2}, while S_{2} reads from Σ_{1} × Σ_{2} and writes to Σ_{2}. For example, we could have

S_{1} = x, y := f(x, y), g(x, y),  S_{2} = y := h(x, y).

We wish to modify S_{1} with S_{2} so that S_{1} writes to Σ_{1} as before, but the value written to Σ_{2} is determined instead by S_{2}. Again, such an operation may be defined as a special case of the product operator: Definition 10 S_{1} mod S_{2} ˆ= S_{1}; ⟨π_{1}⟩ ⊗ S_{2}. Here, ⟨π_{1}⟩ discards the Σ_{2} component written to by S_{1} preserving only the Σ_{1} component. For example,

x, y := f(x, y), g(x, y) mod y := h(x, y) = x, y := f(x, y), h(x, y).

5.4 Rearranging and Extending State Components

Sometimes when combining statements, their state components may not match in the required way. For example, the statements S_{1} : Δ(Σ_{1} × Σ_{2} × Σ_{3}) and S_{2} : Δ(Σ_{2} × Σ_{3} × Σ_{1}) may not be combined directly as S_{1}; S_{2}, (even if Σ_{1}, Σ_{2}, and Σ_{3} are the same sets, constructing S_{1}; S_{2} directly will result in the state components being mismatched). Instead, the state components may be rearranged using an update statement before combining the statements:

S_{1}; ⟨δ⟩; S_{2},

where δ(σ_{1}, σ_{2}, σ_{3}) = (σ_{2}, σ_{3}, σ_{1}).

The same technique can be used to match statements modulo associativity. For example, although

(S_{1} × S_{2}) × S_{3} ≠ S_{1} × (S_{2} × S_{3}),

we do have (let κ((σ_{1}, σ_{2}), σ_{2}) = (σ_{1}, (σ_{2}, σ_{2})) ):

(S_{1} × S_{2}) × S_{3} = ⟨κ⟩; (S_{1} × (S_{2} × S_{3})); ⟨κ^{−1}⟩.

Sometimes the state components of a statement need to be extended in order to combine it with another statement. For example, suppose we wish to combine S_{1} : Δ(Σ_{1} × Σ_{2}) and S_{2} : Δ(Σ_{2}). Here, S_{2} is independent of Σ_{1}, so when combining it with S_{1} we would most likely expect it to leave the Σ_{1} component unchanged. To achieve this, we first combine S_{2} with skip:

S_{1}; (skip_{Σ_{1}} × S_{2}).

Extension of the state space is required, for example, when composing action systems: the state space of all actions must be extended to the state space of the combined action system.

5.5 Shared Variable Assignment

The fusion operator may be viewed as a way of combining statements such as that they both assign a value that they agree on to the same state component. In the case that two statements have only partially overlapping state components, then they need to be extended firstly with the havoc statement, before being combined using the fusion operator. For example, S_{1} : Δ(Σ_{1} × Σ_{2}) and S_{2} : Δ(Σ_{2} × Σ_{3}) may be combined as follows:

(S_{1} × havoc_{Σ_{3}}) ⊙ (havoc_{Σ_{1}} × S_{2}).

Since havoc acts as a unit for the fusion operator, the effect of this statement on the Σ_{1} component will be determined purely by S_{1}, and the effect on the Σ_{3} component will be determined by Σ_{3}. The effect on the Σ_{2} component will be the intersection of the nondeterministic possibilities allowed by S_{1} and S_{2}. If that intersection is empty, then, provided S_{1} and S_{2} terminate, the combination behaves as magic.

Note that the above operands of the fusion operator, do not match exactly: the first is of type Δ((Σ_{1} × Σ_{2}) × Σ_{3}), while the second is of type Δ(Σ_{1} × (Σ_{2} × Σ_{3})). However, these can easily be made to match using the function (λ((σ_{1}, σ_{2}), σ_{3}) · (σ_{1}, (σ_{2}, σ_{3}))) as described in Subsection 5.4.

5.6 Late Binding of Procedures

We model a procedure by simply associating a statement with a procedure name. Calling a procedure then involves executing the statement associated with the procedure name. The following example shows the concrete syntax used to describe procedures:

proc Increment
var x : Int
x := x + 1

The concept of late binding of procedures is important in object-oriented programming. Late binding means that the effect of executing a procedure depends on the value of the state on which it is to be executed. For example, Utting & Robinson [23] model late binding in the refinement calculus by regarding a procedure as being a function from values to statements:

proc : Σ → Δ(Σ).

The effect of executing procedure proc in state σ is then determined by the statement (proc σ). This is sometimes referred to as instance-centered late binding [12].^{2}

A simpler notion of late binding uses types rather than values to determine which statement is selected when a procedure is called (so-called class-centered late binding [12]). Here we show how the summation operator may be used to model this form of late binding.

Firstly, the following operator lifts predicate transformers in either base type of a summation to the summation type: Definition 11 Let S_{1} : Σ_{1} ⟼ Γ_{1} and S_{2} : Σ_{2} ⟼ Γ_{2} be predicate transformers. Then,

S_{1}^{+} ˆ= S_{1} + abort  S_{2}^{+} ˆ= abort + S_{2}.

Now, given predicate transformers

S_{1} : Σ_{1} ⟼ Γ_{1}  S_{2} : Σ_{2} ⟼ Γ_{2}
T_{1} : Γ_{1} ⟼ Λ_{1}  T_{2} : Γ_{2} ⟼ Λ_{2},

we have the following result: Theorem 18

S_{1}^{+}; (T_{1} + T_{2}) = (S_{1}; T_{1})^{+}  S_{2}^{+}; (T_{1} + T_{2}) = (S_{2}; T_{2})^{+}.

That is, the effect of (T_{1} + T_{2}) depends on whether S_{1} or S_{2} is executed beforehand.

Consider the following two procedures:

proc Invert_{1} ; var x : Int ; x := −x  proc Invert_{2} ; var x : Bool ; x := ¬ x

Let Invert ˆ= Invert_{1} + Invert_{2}. Then

(x := 10)^{+}; Invert = (x := 10)^{+}; (Invert_{1} + Invert_{2})
= (x := 10; Invert_{1})^{+}

2Sometimes the terms “late binding” and “dynamic binding” are used interchangeably in the literature. We prefer to reserve the term “dynamic binding” for the case where the procedure associated with an instance/class may change during execution. Such an effect may be achieved, for example, by using stored procedures as provided in Oberon [19] where procedures are themselves values. A predicate transformer model of stored procedures may be found in [21].

= (x := −10)^{+},

while

(x := true)^{+}; Invert = (x := true)^{+}; (Invert_{1} + Invert_{2})
= (x := true; Invert_{2})^{+}
= (x := false)^{+}.

Thus the effect of Invert depends on whether an integer or boolean value has been assigned to x beforehand.

5.7 Inheritance

Consider the following object-oriented definition of a procedure:

proc R inherits S extended by E modified by M

Here, R inherits the behaviour of S, extends the behaviour of S by E and modifies the behaviour of S by M.

Suppose S, E and M have the following types:

S : Δ(Σ_{1} × Σ_{2})

E : Σ_{1} × Σ_{2} × Σ_{3} ⟼ Σ_{3}
M : Σ_{1} × Σ_{2} × Σ_{3} ⟼ Σ_{2}.

That is, E introduces a new component of type Σ_{3}, while M modifies how S behaves on the Σ_{2} component. One way to define R would be as follows:

R ˆ= (S sup E) mod M.

However, in object-oriented programming, as well as performing the extended and modified behaviour on the extended type of R, we would expect R to behave as S on values of the type of S. But some of the behaviour of S has been discarded in (S sup E) mod M. So instead we define R as follows:

R ˆ= S + ((S sup E) mod M).

Now, R uses late binding when choosing whether to perform the inherited behaviour or the extended/modified behaviour.

This form of inheritance preserves refinement: Theorem 19

S ≤ S′ ∧ M ≤ M′ ∧ E ≤ E′ ⇒
S +((S sup E) mod M) ≤ S′ +((S′ sup E′) mod M′).

It should also be possible to define multiple inheritance in a similar way, with the fusion operator being used in the case where two inherited procedures act on the same state component.

6 Conclusions

We have investigated summation and product operators for predicate transformers and shown that they satisfy a rich set of algebraic laws. These are mostly distributivity laws and refinement preservation laws that experience with other operators in the refinement calculus has shown to be useful.

We examined possible applications of these operators such as simultaneous execution, conjunction of specifications, late binding and inheritance. Simultaneous execution is important, for example, for various forms of action system parallel composition. The fusion operator provides a refinement-preserving way of composing requirements (specifications) which could also be viewed as a form of multiple inheritance. Late binding and inheritance are important features of object-oriented programming languages, and although our approach is limited in that we only model class-centered late binding, we believe it to be sufficiently powerful and find the rich set of associated laws encouraging.

Acknowledgements

The work reported here was carried out within the IRENE-project supported by the Academy of Finland. We are grateful to David Naumann and Xu Qiwen for useful comments.

References

[1] J.R. Abrial. B-Technology Technical Overview. B-Core(UK) Ltd., 1993.

[2] R.J.R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications. Tract 131, Mathematisch Centrum, Amsterdam, 1980.

[3] R.J.R. Back and M.J. Butler. Exploring Summation and Product Operators in the Refinement Calculus. Åbo Akademi reports on Computer Science and Mathematics, Series A, No.152, 1994.

[4] R.J.R. Back and R. Kurki-Suonio. Decentralisation of process nets with centralised control. In 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pages 131–142, 1983.

[5] R.J.R. Back and K. Sere. Superposition refinement of parallel algorithms. In K.A. Parker and G.A. Rose, editors, FORTE’91. North–Holland, 1992.

[6] R.J.R. Back and J. von Wright. Refinement concepts formalised in higher order logic. Formal Aspects of Computing, 5:247–272, 1990.

[7] R.J.R. Back and J. von Wright. Refinement Calculus. Book in preparation, Åbo Akademi, 1994.

[8] M.J. Butler. Refinement and Decomposition of Value-Passing Action Systems. In E. Best, editor, CONCUR’93, volume LNCS 715. Springer–Verlag, 1993.

[9] E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

[10] E.W. Dijkstra. From Predicate Transformers to Predicates. Manuscript EWD821, April 1982.

[11] P.H.B. Gardiner and C.C. Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87:143–162, 1991.

[12] J. Gutknecht. Object-Oriented Programming with Oberon. Lecture Notes from Eastern Finland Universities International Summer School on Novel Computing, Lapeenranta University of Technology, Finland, 1994.

[13] J. He, C.A.R. Hoare, and J.W. Sanders. Data refinement refined. In European Symposium on Programming, volume LNCS 213. Springer–Verlag, 1986.

[14] C.B. Jones. Systematic Software Development using VDM – Second Edition. Prentice–Hall, 1990.

[15] C.E. Martin. Preordered Categories and Predicate Transformers. D.Phil. Thesis, Programming Research Group, Oxford University, 1991.

[16] C.C. Morgan. Programming from Specifications. Prentice–Hall, 1990.

[17] C.C. Morgan. The cuppest capjunctive capping, and Galois. In A.W. Roscoe, editor, A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice–Hall, 1994.

[18] J.M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Sci. Comp. Prog., 9(3):298–306, 1987.

[19] H.P. Mossenboeck. Object-Oriented Programming in Oberon-2. Springer-Verlag, 1994.

[20] D.A. Naumann. Two-Categories and Program Structure: Data Types, Refinement Calculi, and Predicate Transformers. Ph.D. Thesis, University of Texas at Austin, 1992.

[21] D.A. Naumann. On the Essence of Oberon. Southwestern University, Georgetown, Texas, 1993.

[22] J.M. Spivey. The Z Notation - A Reference Manual. Prentice–Hall, 1989.

[23] B.M. Utting and K. Robinson. Modular reasoning in an object-oriented refinement calculus. In Mathematics of Program Construction, 1992, volume LNCS 669. Springer–Verlag, 1993.

[24] J. von Wright. The lattice of data refinement. Acta Informatica, 31(2):105– 135, 1994.

[25] N. Ward. Adding specification constructs to the refinement calculus. In FME’93, volume LNCS 670. Springer–Verlag, 1993.