This is a revised draft of a paper to appear in “Millennial Perspectives in Computer Science”, the proceedings of the Oxford–Microsoft Symposium in Honour of Sir Tony Hoare, (held September 13–15, 1999), to be published by Palgrave. It supercedes the version (dated August 12, 1999) that was distributed at the meeting, which contained a serious error.

Intuitionistic Reasoning about Shared Mutable Data Structure^{∗}

John C. Reynolds Department of Computer Science Carnegie Mellon University

July 28, 2000

Abstract

Drawing upon early work by Burstall, we extend Hoare’s approach to proving the correctness of imperative programs, to deal with programs that perform destructive updates to data structures containing more than one pointer to the same location. The key concept is an “independent conjunction” P & Q that holds only when P and Q are both true and depend upon distinct areas of storage. To make this concept precise we use an intuitionistic logic of assertions, with a Kripke semantics whose possible worlds are heaps (mapping locations into tuples of values).

The dichotomy between functional and imperative programming has obscured a variety of programming techniques that fit comfortably in neither approach. In fact, between these two paradigms there is a no-man’s land inhabited by many useful and intuitively straightforward programs that have been poorly served by both type systems and program-proving methodologies.

∗This research was sponsored by National Science Foundation Grant CCR-9804014.

Particularly important are programs where the data structure may contain more than one pointer to the same location, and the program destructively updates the contents of such locations. This class of programs includes many interesting and practically important algorithms; it is far more than a hacker’s jungle. Yet there has been surprisingly little research on reasoning about such programs.

In 1972, Burstall [1] gave correctness proofs for imperative programs that alter data structures, by using a novel kind of assertion that he called a “distinct nonrepeating tree system”; this approach was extended by Kowaltowski [2]. In 1975, Cook and Oppen [3, 4] devised an more general approach by extending Hoare logic with extremely complicated inference rules. Then, in 1981, J. M. Morris [5] extended weakest-precondition logic by generalizing the notion of substitution.

In the late 80’s Mason and Talcott [6, 7, 8] investigated reasoning about program equivalence for LISP-like functional languages where expression evaluation can alter data structures as a side effect; more recently they and others [9, 10] have extended this approach to a logic for reasoning about programs.

Also recently, Pitts and Stark [11] have studied operational reasoning about an ML-like language with data-altering expressions. (In this work, however, only simple values can be stored at locations; not structured values that themselves contain locations.) This research builds upon earlier work by Stark [12, 13, 14] on languages that create local names.

The present paper builds upon Burstall’s ideas, which fit nicely into the framework for reasoning about imperative programs that was devised about the same time by Hoare [15, 16], as well as earlier work by Floyd [17] and Naur [18]. Burstall’s “distinct nonrepeating tree system” was a sequence of assertions, written P_{1} & ⋯ & P_{n} in the notation of this paper, where each P_{i} described a distinct region of storage, so that an assignment to a single location could change only one of the P_{i}. I believe that this idea of organizing assertions to localize the effect of a mutation may be the key to scalability in reasoning about shared mutable data structure.

The goal of this paper is to overcome two limitations of Burstall’s work. In his formalism, each P_{i}, which he called a “triple”, described a fragment of data structure with no internal sharing. (Technically, the triples were morphisms in categories called “free theories” by Lawvere [19].) Sharing only occurred among pointers from variables into fragments, or from one fragment to another, so that a particular assertion could describe only structures with a fixed finite bound on the number of shared locations.

A subtler limitation was the specific notion of composition of triples. Roughly speaking, one composed P with Q by identifying the pointers coming out of P with those going into Q.

In this paper we will use the doubly-linked list as a simple example that violates both limitations. In this structure, every location is shared, so that a description of a fragment representing an arbitrary sequence must permit unbounded internal sharing. Moreover, the natural way of composing fragments P and Q is to identify both a pointer coming out of P with one going into Q, and a pointer coming out of Q with one going into P.

The preliminary version of this paper was flawed by a serious error: The inference rule for the cons operation was unsound. In the present version (as discussed at the end of Section 3), we have repaired this flaw, and substantially simplified our development, by interpreting assertions intuitionistically, using a Kripke semantics [20] with heaps as possible worlds. A similar intuitionistic semantics has been discovered independently by Ishtiaq and O’Hearn [21], using the logic of bunched implications [22].

1 Syntax

The programming language we will use is the simple imperative language originally axiomatized by Hoare, with additional commands for the manipulation of list structures. These structures will be similar to those of LISP, restricted by the elimination of property lists for atoms, and extended by permitting any positive number of values to be “cons-ed” together. Specifically, the LISP constructor cons will be generalized to cons_{1}, cons_{2}, cons_{3}, etc., and the selectors car(E) and cdr(E) to E.1, E.2, etc.

In contrast to LISP, however, these constructors and selectors will be permitted only in commands, not in expressions. The reason for this restriction is that the power of the kind of proof system advocated by Hoare (or Floyd or Dijkstra) depends on the ability to use any expression of the programming language in an assertion. In particular, substituting any expressions for the variables of a tautology should give a valid assertion.

Constructors cannot be expressions since they have side effects. For instance, if we could substitute cons_{2}(1, 2) for x in the tautology x = x, we would obtain cons_{2}(1, 2) = cons_{2}(1, 2), which must not hold if we are going to distinguish different locations with the same contents.

Selectors cannot be expressions because of their interaction with the “independent conjunction” operator &. For instance, if we could substitute z.2 for both x and y in the tautology x = x & y = y, we would obtain z.2 = z.2 & z.2 = z.2, which is false since the two operands of & do not depend upon distinct regions of storage.

Instead of permitting constructors and selectors in expressions, we introduce three novel forms of commands, which use constructors to create new list structures, and selectors to evaluate and mutate such structures:

\begin{aligned}x & := & cons_{n}(E_{1}, …, E_{n}) \\ x & := & E.i \\ E.i & := & E′ \end{aligned}

(where the various E’s denote expressions). We have used the assignment symbol := to give these commands a familiar appearance that should make their informal meaning obvious. Formally, however, they are not assignment commands; in particular they will not obey Hoare’s axiom of assignment.

As in Hoare’s work, assertions include boolean expressions, enriched with quantifiers. In addition, we introduce the form

E → E_{1}, …, E_{n},

which holds if the value of E is a location at which is stored an n-tuple containing the values of E_{1}, … E_{n}. Finally, we add the independent conjunction operator, so that an assertion can have the form

P & P′

(where P and P′ denote assertions). Roughly speaking, this form is true when P and P′ are both true and depend upon distinct regions of storage.

We will define two forms of specification: the original partial-correctness triple introduced by Hoare, which we will write {P } C {Q}, and an analogous total-correctness specification, which we will write [ P ] C [ Q].

2 Semantics

To make the meaning of our language and its specifications precise, we define a value to be an integer, an atom, or a location, where integers, atoms, and locations comprise disjoint, countably infinite sets, and nil is a particular atom:

Values = Integers ∪ Atoms ∪ Locations
nil ^{∈} Atoms.

To formalize mutable list structures, we must complicate the usual notion of the state of a computation, which now consists of two parts: the store, which maps some finite set of variables into values, and the heap, which maps some finite set of locations into nonempty tuples of values. Thus

Stores_{V} = (V → Values) where V is a finite set of variables
Heaps_{L} = (L → Values^{+}) where L is a finite set of locations
Heaps = ⋃_{L⊆^{fin}Locations} Heaps_{L}
States_{V} = Stores_{V} × Heaps.

A state ⟨η, σ⟩ is said to be complete if the domain of its heap component includes all locations that occur anywhere within the state, i.e., if

∀x ^{∈} dom η. η x ^{∈} Integers ∪ Atoms ∪ dom σ
∀ℓ ^{∈} dom σ. σ ℓ ^{∈} (Integers ∪ Atoms ∪ dom σ)^{+}.

We define the set

CmplStates_{V} = { ⟨η, σ⟩ | ⟨η, σ⟩ ^{∈} States_{V} and ⟨η, σ⟩ is complete }.

For each of the five classes of phrases used in programs or their specifications, there is a semantic function giving a different kind of meaning. Each of these semantic functions is indexed by a finite set of variables that must include the free variables of the argument of the semantic function. (We write OrdExp_{V} for the set of ordinary expressions whose free variables belong to V, and similarly for the other phrase classes.)

• Ordinary Expressions

[[−]]_{V}^{ordexp} ^{∈} OrdExp_{V} → Stores_{V} → Values,

• Boolean Expressions

[[−]]_{V}^{boolexp} ^{∈} BoolExp_{V} → Stores_{V} → {true, false},

• Commands

[[−]]_{V}^{comm} ^{∈} Comm_{V} → CmplStates_{V} → (CmplStates_{V} ∪ {⊥}),

• Assertions

[[−]]_{V}^{assert} ^{∈} Assert_{V} → Stores_{V} → Heaps → {true, false},

• Specifications

[[−]]_{V}^{spec} ^{∈} Spec_{V} → {true, false}.

Notice that ordinary and boolean expressions do not depend upon the heap. (This reflects our decision not to permit constructors and selectors in expressions.) Assertions that do not depend upon the heap are called pure, as are commands that neither depend upon nor change the heap. (As usual in denotational semantics, ⊥ is used to denote the nonterminating execution of a command.)

The meaning of expressions, commands, and specifications is standard. Note, however, that the implicit quantification of specifications extends over both the store and heap components of complete states:

[[{P } C {P′}]]_{V}^{spec} = ∀⟨η, σ⟩ ^{∈} CmplStates_{V} . [[P]]ησ and [[C]]⟨η, σ⟩ ≠ ⊥

implies [[P′]]η′σ′ where ⟨η′, σ′⟩ = [[C]]⟨η, σ⟩

[[[ P ] C [ P′ ]]]_{V}^{spec} = ∀⟨η, σ⟩ ^{∈} CmplStates_{V} . [[P]]ησ

implies [[C]]⟨η, σ⟩ ≠ ⊥ and [[P′]]η′σ′ where ⟨η′, σ′⟩ = [[C]]⟨η, σ⟩.

What is not standard is the meaning of assertions, which is defined for incomplete as well as complete states, by a Kripke semantics [20] in which the possible worlds are heaps, ordered by extension. Thus the logic of assertions is intuitionistic rather than classical.

When a boolean expression is used as an assertion, it is pure, i.e., its meaning is independent of the heap:

[[B]]_{V}^{assert}ησ iff [[B]]_{V}^{boolexp}η.

The simplest impure assertion is E → E_{1}, …, E_{n}, which describes the value of the heap for a single location:

[[E → E_{1}, …, E_{n}]]_{V}^{assert}ησ iff

[[E]]_{V}^{ordexp}η ^{∈} dom σ and σ([[E]]_{V}^{ordexp}η) = ⟨[[E_{1}]]_{V}^{ordexp}η, …, [[E_{n}]]_{V}^{ordexp}η⟩.

The operations of conjunction, disjunction, and quantification are defined conventionally, with the heap being treated pointwise:

[[P_{1} ∧ P_{2}]]_{V}^{assert}ησ iff [[P_{1}]]_{V}^{assert}ησ and [[P_{2}]]_{V}^{assert}ησ
[[P_{1} ∨ P_{2}]]_{V}^{assert}ησ iff [[P_{1}]]_{V}^{assert}ησ or [[P_{2}]]_{V}^{assert}ησ
[[∀x. P]]_{V}^{assert}ησ iff ∀v ^{∈} Values. [[P]]_{V}^{assert}[ η | x: v]σ
[[∃x. P]]_{V}^{assert}ησ iff ∃v ^{∈} Values. [[P]]_{V}^{assert}[ η | x: v]σ.

Here [ η | x: v] denotes the store, with domain dom η ∪ {x}, that maps x into v and maps all other variables x′ into η x′. (Analogous quantifiers that range over integers, atoms, or locations are left to the reader.)

On the other hand, the definitions of implication and negation involve an implicit universal quantification over extensions of the heap:

[[P_{1} ⇒ P_{2}]]_{V}^{assert}ησ iff ∀σ′ ⊇ σ. [[P_{1}]]_{V}^{assert}ησ′ implies [[P_{2}]]_{V}^{assert}ησ′
[[¬ P]]_{V}^{assert}ησ iff ∀σ′ ⊇ σ. not [[P]]_{V}^{assert}ησ′.

Finally, we must define the independent conjunction operation &. The idea that P_{1} and P_{2} must depend upon distinct regions of the heap is captured by requiring them to hold for restrictions of the heap with disjoint domains:

[[P_{1} & P_{2}]]_{V}^{assert}ησ iff ∃σ_{1}, σ_{2}.
σ_{1} ⊆ σ and σ_{2} ⊆ σ and dom σ_{1} ∩ dom σ_{2} empty
and [[P_{1}]]_{V}^{assert}ησ_{1} and [[P_{2}]]_{V}^{assert}ησ_{2}.

We are able to define independent conjunction so simply because we have given meaning to assertions in all states, not just complete states, and because this meaning obeys a monotonicity law that is characteristic of Kripke semantics:

If [[P]]_{V}^{assert}ησ and σ ⊆ σ′, then [[P]]_{V}^{assert}ησ′.

To obtain this property, however, we have sacrificed the law of the excluded middle. For instance, if the store η maps the variable x into a location that does not belong to the domain of the heap σ, then

[[x → 7]]_{V}^{assert}ησ,  [[¬ x → 7]]_{V}^{assert}ησ,  [[x → 7 ∨ ¬ x → 7]]_{V}^{assert}ησ

are all false.

As one expects in an intuitionistic logic, one has axiom schemata such as

\begin{aligned}∀x. ¬ P & ⇔ & ¬(∃x. P) \\ ∃x. ¬ P & ⇒ & ¬(∀x. P) \\ P & ⇒ & ¬(¬ P), \end{aligned}

but not the converses of the second and third lines. (Pure assertions, however, which are those that do not contain →, behave classically.)

Insight into the operation of independent conjunction is provided by a simple example: Suppose η is a store that maps x and y into distinct locations, and consider the heaps

σ_{1} = {⟨η x, 1⟩} and σ_{2} = {⟨η y, 2⟩},

which have disjoint domains. Then

If P is:  then [[P]]ησ is:
x → 1  σ_{1} ⊆ σ
y → 2  σ_{2} ⊆ σ
x → 1 & y → 2  σ_{1} ∪ σ_{2} ⊆ σ
x → 1 & (x → 1 ∨ y → 2)  σ_{1} ∪ σ_{2} ⊆ σ
(x → 1 ∨ y → 2) & (x → 1 ∨ y → 2)  σ_{1} ∪ σ_{2} ⊆ σ
x → 1 & y → 2 & (x → 1 ∨ y → 2)  false.

In general, independent conjunction is described by the axiom schemata

P_{1} & P_{2} ⇒ P_{1} ∧ P_{2}
P_{1} ∧ P_{2} ⇒ P_{1} & P_{2} when P_{2} is pure
P_{1} & P_{2} ⇔ P_{2} & P_{1}
(P_{1} & P_{2}) & P_{3} ⇔ P_{1} & (P_{2} & P_{3})
(P_{1} & P_{3}) ∨ (P_{2} & P_{3}) ⇔ (P_{1} ∨ P_{2}) & P_{3}
(P_{1} ∨ P_{3}) & (P_{2} ∨ P_{3}) ⇒ (P_{1} & P_{2}) ∨ P_{3}
(∃x. P_{1}) & P_{2} ⇔ ∃x. (P_{1} & P_{2}) when x not free in P_{2},

and the inference rule

P_{1} ⇒ P_{2}
P_{1} & P_{3} ⇒ P_{2} & P_{3}.

Note, however, that the analogous schemata (P_{1} ⇒ P_{2}) ⇒ (P_{1} & P_{3} ⇒ P_{2} & P_{3}) is not valid.

3 Inference Rules for Specifications

By prohibiting expressions from depending upon the heap, we insure that both the partial-correctness rules given by Hoare and the analogous totalcorrectness rules (see, for example, [23, Chapter 3]) remain valid, even for assertions containing &. Thus we need to introduce additional rules only for the new commands that depend upon or affect the heap. Since the new commands always terminate, these rules are identical for partial and total correctness.

First, we have the command x:= E.i, which examines the tuple stored in the heap at the location that is the value of E, and makes the ith component of this tuple the value of x. This operation is similar enough to assignment that one might hope to extend Hoare’s assignment axiom to describe it. But that axiom involves a substitution that would insert E.i into expressions, violating their purity. (If such substitutions were allowed, they would not preserve &.) Instead, we must mimic the effect of such a substitution by using existential quantifiers:

Suppose that x_{1}, …, x_{n} are distinct variables that do not occur free in E, that 1 ≤ i ≤ n, and that x_{i} does not occur free in P. Let P^{(i)} denote the result of substituting x_{i} for x in P. Then

{∃x_{i}. (P^{(i)} ∧ ∃x_{1}, …, x_{i−1}, x_{i+1}, …, x_{n}. E → x_{1}, …, x_{n})}
x:= E.i
{P }.

Next, we have the command x:= cons_{n}(E_{1}, …, E_{n}), which extends the heap with a new location mapped into the n-tuple of values of E_{1}, …, E_{n}, and then makes the new location the value of x. Again, we cannot use Hoare’s assignment axiom; instead we introduce an existential quantifier in the postcondition, in the style of Floyd [17]. The & operation is used to assert that the new location plays no role in any part of the postcondition that is inherited from the precondition:

Suppose that the variables x and x′ are distinct, and that x′ does not occur free in E_{1}, … E_{n}, or P. Let X′ denote the result of substituting x′ for x in the expression or assertion X. Then

{P }
x:= cons_{n}(E_{1}, …, E_{n})
{∃x′. (P′ & x → E′_{1}, …, E′_{n})}.

Happily, this rule can be simplified when the variable x does not occur in the precondition or the right side of the command being specified:

Suppose that the variables x does not occur free in E_{1}, …, E_{n} or P. Then

{P }
x:= cons_{n}(E_{1}, …, E_{n})
{P & x → E_{1}, …, E_{n}}.

Finally, we have a rule for the command E.i:=E′, which alters the heap at the location that is the value of E by changing the ith component of the tuple at that location to the value of E′. Here the & operator in the precondition separates an assertion about the heap at the value of E from assertions about other parts of the heap, which are not affected by the command:

Suppose that the variables x_{1}, …, x_{m} do not occur free in the expression E or E′, and that 1 ≤ i ≤ n. Then

{∃x_{1}, …, x_{m}. (E → E_{1}, …, E_{i}, …, E_{n} & P)}
E.i:= E′
{∃x_{1}, …, x_{m}. (E → E_{1}, …, E′, …, E_{n} & P)}.

The importance of using an intuitionistic logic is illustrated by the following instance of the simplified cons-rule:

{¬(∃x. x → 1, 2)}
y := cons_{2}(1, 2)
{(¬(∃x. x → 1, 2)) & y → 1, 2}.

Although its postcondition is always false, this instance is not unsound, because the precondition is always false in our intuitionistic logic — since it must hold for all extensions of the heap that was current immediately before execution of the cons operation, including the extension that is current immediately afterwards.

(This instance was unsound, however, in the classical logic used in the preliminary version of this paper.)

4 Inductive Definition of Predicates

To deal with real programs (even small ones), we must permit predicates to be defined by induction over sets of abstract data.

For instance, to prove the correctness of a program that uses some list representation, it is not enough to be able to assert that something is a list representation; one must say that it represents a particular sequence of values. Thus one must define “is representation of” as a function from the abstract data set “sequence of values” to predicates.

Specifically (though without being as formal as in previous sections), we will allow variables that occur in assertions but not in programs (often called logical or ghost variables) to range over inductively defined sets, and we will allow functions from such sets to predicates to be defined by induction (i.e., by primitive recursion).

As a first example, consider the representation of sequences by singlylinked lists. (This example is essentially similar to one of Burstall’s.) We write ϵ to denote the empty sequence, use other Greek letters as variables ranging over sequences, write · to indicate concatenation, and assume that a value is a sequence of length one. Then

list ϵ (i, j) ≡ i = j
list a·α (i, k) ≡ ∃j. i → a, j & list α (j, k)

is an inductive definition of a function list, from sequences to predicates, such that list α (i, j) asserts that the sequence α is represented by the list fragment from location i to j. More precisely, it asserts that there is a succession of cons_{2}-cells beginning at location i, containing the successive elements of α as their first components, and linked together by their second components, with a final link containing j:

[figure: α_{1}; i; ⋯; ^{j α_{n}}]

From this definition, it is obvious that

list a (i, j) ⇔ i → a, j.

Less trivially, one can show by induction on the length of α that

list α·β (i, k) ⇔ ∃j. list α (i, j) & list β (j, k),

and from this result one can obtain

list α·b (i, k) ⇔ ∃j. list α (i, j) & j → b, k.

Because of the use of & in the definition of list, the assertion list α (i, j) implies that the list fragment from i to j contains a distinct cons_{2}-cell for each element of α. Nevertheless, j can be the location of one of these cells, in which case a cyclic structure is being described. For instance, when α is nonempty, list α (i, i) describes a cycle whose length is the length of α.

However, when i = nil, the assertion i → a, j cannot hold, so that list a·α (i, k) cannot hold. In fact,

list α (i, j) ⇒ ( \begin{matrix}& (i = nil & ⇒ & (α = ϵ ∧ j = nil)) \\ ∧ & (i ≠ j & ⇒ & α ≠ ϵ). \end{matrix} )

A more complex example, which goes beyond Burstall’s framework, is the representation of sequences by doubly-linked lists. We write dlist α (i, i′, j, j′) to assert the existence of a a collection of cons_{3}-cells whose first components give the elements of α, whose second components are the links of a forward list beginning at i with a final link containing j, and whose third components are the links of a backward list beginning at j′ with a final link containing i′:

[figure: i′; α_{1}; i; ⋯; ⋯; j; α_{n}; j′]

This function can be defined inductively by

dlist ϵ (i, i′, j, j′) ≡ i = j & i′ = j′
dlist a·α (i, i′, k, k′) ≡ ∃j. i → a, j, i′ & dlist α (j, i, k, k′).

From this definition, it is obvious that

dlist a (i, i′, j, j′) ⇔ i → a, j, i′ & i = j′.

Less trivially, one can show by induction on the length of α that

dlist α·β (i, i′, k, k′) ⇔ ∃j, j′. dlist α (i, i′, j, j′) & dlist β (j, j′, k, k′),

and from this result one can obtain

dlist α·b (i, i′, k, k′) ⇔ ∃j′. dlist α (i, i′, k′, j′) & k′ → b, k, j′.

Much as in the singly-linked case, the assertion dlist α (i, i′, j, j′) describes a list fragment containing a distinct cons_{3}-cell for each element of α. The existence of unique back-links prevents a list from having a cyclic tail, but one can still have an isolated cyclic list, which would be described by dlist α (i, i′, i, i′) when α is nonempty.

Finally, to distinguish empty from nonempty lists, one can derive

dlist α (i, i′, j, j′) ⇒ ( \begin{matrix}& (i = nil & ⇒ & (α = ϵ ∧ j = nil ∧ i′ = j′)) \\ ∧ & (j′ = nil & ⇒ & (α = ϵ ∧ i′ = nil ∧ i = j)) \\ ∧ & (i ≠ j & ⇒ & α ≠ ϵ) \\ ∧ & (i′ ≠ j′ & ⇒ & α ≠ ϵ) \end{matrix} )

5 Annotated Specifications

For even a small program, a formal proof of its specification, in the sense of a sequence (or tree) of instances of inference rules, is usually too large to be readable. Fortunately, one can annotate a specification with intermediate assertions in such a way that its proof can be mechanically and straightforwardly derived from the annotations.

In the next section, we will give an illustrative proof in the form of an annotated specification. Before doing so, however, it is useful — independently of the main subject of this paper — to define the notion precisely (for the partial-correctness case).

The basic idea goes back at least to the “proof outlines” of concurrent computations by Owicki and Gries [24], which have been formalized by Schneider [25, Chapter 4]. Our formulation for sequential programs, however, permits the omission of many intermediate assertions that can be derived straightforwardly from their context.

We will call a specification annotated if it can be derived from the inference rules to be given below. All of these rules are easily derivable from Hoare’s rules and the rules given in Section 3, except that intermediate assertions occur in the conclusions of certain rules. Because of the presence of these intermediate assertions, the rules are determinate, i.e., every specification can be the conclusion of an instance of at most one rule, and the premisses of this instance are determined by its conclusion. Thus it is straightforward to derive a proof of an annotated specification from the specification itself, and a Hoare-style proof (albeit using derived rules) can then be obtained by erasing the intermediate assertions. (Of course, this proof will contain verification conditions, i.e., unproved implications between assertions, that must be verified independently. Pragmatically, one must supply enough intermediate assertions to make this verification tractable.)

The first two rules deal with assignment. Their determinacy stems from the fact that, in Hoare’s assignment axiom, the precondition P/x → E is determined by the postcondition P and the assignment command x:= E:

\frac{P_{0} ⇒ P/x → E}{\{P_{0}\} x:= E \{P \}}  \frac{\{P_{0}\} C \{P/x → E\}}{\{P_{0}\} C ; x:= E \{P \}.}

A similar situation holds for the rule for the select-and-assign command x := E.i, where again the precondition is determined by the postcondition and the command:

\frac{P_{0} ⇒ ∃x_{i}. (P^{(i)} ∧ ∃x_{1}, …, x_{i−1}, x_{i+1}, …, x_{n}. E → x_{1}, …, x_{n})}{\{P_{0}\} x:= E.i \{P \}} ; \frac{\{P_{0}\} C \{∃x_{i}. (P^{(i)} ∧ ∃x_{1}, …, x_{i−1}, x_{i+1}, …, x_{n}. E → x_{1}, …, x_{n})\}}{\{P_{0}\} C ; x:= E.i \{P \}.}

In contrast, the remaining axioms for heap-dependent commands given in Section 3 have the property that their postcondition is determined by their precondition and the heap-dependent command. This insures the determinacy of:

Suppose that the variables x and x′ are distinct, and that x′ does not occur free in E_{1}, … E_{n}, or P. Let X′ denote the result of substituting x′ for x in the expression or assertion X. Then

\frac{(∃x′. (P′ & x → E′_{1}, …, E′_{n})) ⇒ P′′}{\{P \} x:= cons_{n}(E_{1}, …, E_{n}) \{P′′\}}

{∃x′. (P′ & x → E′_{1}, …, E′_{n})} C {P′′}

{P } x:= cons_{n}(E_{1}, …, E_{n}) ; C {P′′}.

Suppose that the variables x_{1}, …, x_{m} do not occur free in the expression E or E′, and that 1 ≤ i ≤ n. Then

\frac{(∃x_{1}, …, x_{m}. (E → E_{1}, …, E′, …, E_{n} & P)) ⇒ P′′}{\{∃x_{1}, …, x_{m}. (E → E_{1}, …, E_{i}, …, E_{n} & P)\} E.i:= E′ \{P′′\}} ; \frac{\{∃x_{1}, …, x_{m}. (E → E_{1}, …, E′, …, E_{n} & P)\} C \{P′′\}}{\{∃x_{1}, …, x_{m}. (E → E_{1}, …, E_{i}, …, E_{n} & P)\} E.i:= E′ ; C \{P′′\}.}

Next, we have rules for skip, if, and while commands:

\frac{P ⇒ P′}{\{P \} skip \{P′\}}  \frac{\{P ∧ B\} C_{1} \{P′\} \{P ∧ ¬ B\} C_{2} \{P′\}}{\{P \} if B then C_{1} else C_{2} fi \{P′\}}

\frac{\{P ∧ B\} C \{P \} (P ∧ ¬ B) ⇒ P′}{\{P \} while B do C od \{P′\}.}

Finally, there are rules corresponding to Hoare’s rules for sequencing, strengthening preconditions, and weakening postconditions. It is in the conclusions of these rules that the intermediate assertions appear:

\frac{\{P \} C \{P′\} \{P′\} C′ \{P′′\}}{\{P \} C ; \{P′\} C′ \{P′′\}} ; \frac{P ⇒ P′ \{P′\} C \{P′′\}}{\{P \} \{P′\} C \{P′′\}} \frac{\{P \} C \{P′\} P′ ⇒ P′′}{\{P \} C \{P′\} \{P′′\}.}

6 An Example

In conclusion, we illustrate our formalism with an example: an annotated partial-correctness specification of a program for deleting zero-valued elements from a doubly-linked list.

Throughout execution of the program, the forward linkage of the list begins at location i and the backward linkage begins at location m. There is a single loop which moves forward through the list. Within this loop, the deletion operation is symmetric about the cell to be deleted.

Just before the test b = 0, the variable k points to the cell to be tested and perhaps removed, the preceding list fragment has a forward linkage from i to k and a backward linkage from j to nil, and the following list fragment has a forward linkage from l to nil and a backward linkage from m to k:

[figure: nil; α̂_{1}; i; ⋯; ⋯; α̂_{m}; j; b; k; β_{1}; l; ⋯; ⋯; nil; β_{n}; m]

If the current cell is to be removed, the program tests whether the preceding list fragment is empty, and resets either i or the last forward link to point to the following list fragment. Then it performs a symmetric operation on the following list fragment.

The notation α − 0 denotes the sequence obtained from α by deleting all occurrences of zero.

{dlist γ (i, nil, nil, m)} {∃α, β, α̂. dlist α̂ (i, nil, i, nil) & dlist β (i, nil, nil, m)

& α·β = γ & α − 0 = α̂} k := i ; j := nil ; {∃α, β, α̂. dlist α̂ (i, nil, k, j) & dlist β (k, j, nil, m)

& α·β = γ & α − 0 = α̂} while k ≠ nil do

{∃α, β, α̂, b, l. dlist α̂ (i, nil, k, j) & k → b, l, j & dlist β (l, k, nil, m)

& α·b·β = γ & α − 0 = α̂} b := k.1 ; l := k.2 ; {∃α, β, α̂. dlist α̂ (i, nil, k, j) & k → b, l, j & dlist β (l, k, nil, m)

& α·b·β = γ & α − 0 = α̂} if b = 0 then

{∃α, β, α̂. dlist α̂ (i, nil, k, j) & dlist β (l, k, nil, m)

& α·0·β = γ & (α·0) − 0 = α̂} {∃α, β, α̂. dlist α̂ (i, nil, k, j) & dlist β (l, k, nil, m)

& α·β = γ & α − 0 = α̂} if j = nil then

{∃α, β, α̂. α̂ = ϵ & i = k & nil = j & dlist β (l, k, nil, m)

& α·β = γ & α − 0 = α̂} i := l {∃α, β, α̂. α̂ = ϵ & i = l & nil = j & dlist β (l, k, nil, m)

& α·β = γ & α − 0 = α̂} else

{∃α, β, α̂, a, n. dlist α̂ (i, nil, j, n) & j → a, k, n & dlist β (l, k, nil, m)

& α·β = γ & α − 0 = α̂·a} j.2 := l {∃α, β, α̂, a, n. dlist α̂ (i, nil, j, n) & j → a, l, n & dlist β (l, k, nil, m)

& α·β = γ & α − 0 = α̂·a}

fi ;

{∃α, β, α̂. dlist α̂ (i, nil, l, j) & dlist β (l, k, nil, m)

& α·β = γ & α − 0 = α̂} if l = nil then

{∃α, β, α̂. dlist α̂ (i, nil, l, j) & β = ϵ & l = nil & k = m

& α·β = γ & α − 0 = α̂} m := j {∃α, β, α̂. dlist α̂ (i, nil, l, j) & β = ϵ & l = nil & j = m

& α·β = γ & α − 0 = α̂} else

{∃α, β, α̂, a, n. dlist α̂ (i, nil, l, j) & l → a, n, k & dlist β (n, l, nil, m)

& α·a·β = γ & α − 0 = α̂} l.3 := j {∃α, β, α̂, a, n. dlist α̂ (i, nil, l, j) & l → a, n, j & dlist β (n, l, nil, m)

& α·a·β = γ & α − 0 = α̂} fi

else

{∃α, β, α̂. dlist α̂·b (i, nil, l, k) & dlist β (l, k, nil, m)

& α·b·β = γ & (α·b) − 0 = α̂·b} {∃α, β, α̂. dlist α̂ (i, nil, l, k) & dlist β (l, k, nil, m)

& α·β = γ & α − 0 = α̂} j := k

fi ;

{∃α, β, α̂. dlist α̂ (i, nil, l, j) & dlist β (l, j, nil, m)

& α·β = γ & α − 0 = α̂} k := l

od {dlist (γ − 0) (i, nil, nil, m)}

7 Future Directions

The work described here is very preliminary, so that the most immediate need is to explore more examples. In particular, it is not clear that every abstract structure represented by mutable data structures can be defined inductively; for example, mutable data structures are often used to represent cyclic graphs.

It may be possible to extend our approach to dynamic logic [26], where commands can occur as modal operators within assertions. This would necessitate giving meaning to the execution of commands in incomplete states. When a command tries to examine a heap outside of its domain, it would raise a “heap fault” that would make the immediately enclosing assertion false.

It is easy to prove {true} x := cons_{2}(1, 2) ; {x → 1, 2} x := 3 {(∃x. x → 1, 2) ∧ x = 3}.

Here the existentially quantified location is disconnected from the data structures accessible to the computation, and can be eliminated by garbage collection. Of course, one can view garbage collection as a program optimization with no effect on observable computations, so that this example is sound. Nevertheless the fact that ∃x. x → 1, 2 is an “unobservable assertion” is worrisome.

It should be straightforward to impose upon the present development a type system based upon recursive data type declarations (similar to those in Standard ML but without the reference concept). More refined type systems might permit the specification of which fields are mutable or where pointers are required to be unique.

Finally, there is a need to move towards some form of higher-order formalism, akin to object-oriented programming, where the mutable shared data structures can contain closures. An obvious question is whether there is a connection with syntactic control of interference [27, 28, 29] or specification logic [30, 31, 32], both of which deal with interference in a higher-order but heap-free setting. Superficially this work seems quite different, but the recurring use of possible-world semantics is suggestive.

Acknowledgements

The author would like to thank Peter O’Hearn for his insights and helpful suggestions.

References

[1] Rodney M. Burstall. Some techniques for proving correctness of programs which alter data structures. In Bernard Meltzer and Donald Michie, editors, Machine Intelligence 7, pages 23–50. Edinburgh University Press, Edinburgh, Scotland, 1972.

[2] T. Kowaltowski. Correctness of programs manipulating data structures. Memorandum ERL-M404, University of California, Berkeley, California, September 1973.

[3] Stephen A. Cook and Derek C. Oppen. An assertion language for data structures. In Conference Record of the Second ACM Symposium on Principles of Programming Languages, pages 160–166, New York, 1975. ACM.

[4] Derek C. Oppen and Stephen A. Cook. Proving assertions about programs that manipulate data structures. In Proceedings of Seventh Annual ACM Symposium on Theory of Computing, pages 107–116, New York, 1975. ACM.

[5] Joseph M. Morris. A general axiom of assignment; assignment and linked data structures; a proof of the Schorr-Waite algorithm. In Manfried Broy and Gunther Schmidt, editors, Theoretical Foundations of Programming Methodology, pages 25–51. D. Reidel, Dordrecht, Holland, 1982.

[6] Ian A. Mason. The Semantics of Destructive Lisp. CSLI Lecture Notes Number 5. Center for the Study of Language and Information, Menlo Park, CA, 1986.

[7] Ian A. Mason. Verification of programs that destructively manipulate data. Science of Computer Programming, 10(2):177–210, April 1988.

[8] Ian A. Mason and Carolyn Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(3):287–327, July 1991.

[9] Furio Honsell, Ian A. Mason, Scott Smith, and Carolyn Talcott. A variable typed logic of effects. Information and Computation, 119(1):55– 90, May 15, 1995.

[10] Ian A. Mason. A first order logic of effects. Theoretical Computer Science, 185(2):277–318, October 20, 1997.

[11] Andrew M. Pitts and Ian D. B. Stark. Operational reasoning for functions with local state. In Andrew D. Gordon and Andrew M. Pitts, editors, Higher Order Operational Techniques in Semantics, pages 227– 273. Cambridge University Press, 1998.

[12] Ian D. B. Stark. Names and Higher-Order Functions. Ph. D. dissertation, University of Cambridge, Cambridge, England, December 1994.

[13] Ian D. B. Stark. Categorical models for local names. Lisp and Symbolic Computation, 9(1):77–107, February 1996.

[14] Ian D. B. Stark. Names, equations, relations: Practical ways to reason about new. Fundamenta Informaticae, 33:369–396, 1998.

[15] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580 and 583, October 1969. Reprinted in [33, pages 89–100].

[16] C. A. R. Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39–45, January 1971. Reprinted in [33, pages 101–115].

[17] Robert W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19–32, Providence, Rhode Island, 1967. American Mathematical Society.

[18] Peter Naur. Proof of algorithms by general snapshots. BIT, 6:310–316, 1966.

[19] F. William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America, 50(1):869–872, July 1963.

[20] Saul A. Kripke. Semantical analysis of intuitionistic logic i. In John N. Crossley and Michael A. E. Dummett, editors, Formal Systems and Recursive Functions, Studies in Logic and the Foundations of Mathematics, pages 92–130, Amsterdam, 1965. North-Holland.

[21] Peter W. O’Hearn. Private communication. dated January 17, 2000.

[22] Peter W. O’Hearn and David J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–244, June 1999.

[23] John C. Reynolds. Theories of Programming Languages. Cambridge University Press, Cambridge, England, 1998.

[24] Susan Speer Owicki and David Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6(4):319–340, 1976. Reprinted in [33, pages 130–152].

[25] Fred B. Schneider. On Concurrent Programming. Springer-Verlag, New York, 1997.

[26] Vaughan R. Pratt. Semantical considerations on Floyd-Hoare logic. In 17th Annual Symposium on Foundations of Computer Science, pages 109–121, Long Beach, California, 1976. IEEE Computer Society.

[27] John C. Reynolds. Syntactic control of interference. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 39–46, New York, 1978. ACM. Reprinted in [34, vol. 1, pages 273–286].

[28] Peter W. O’Hearn, A. John Power, Makoto Takeyama, and Robert D. Tennent. Syntactic control of interference revisited. Electronic Notes in Theoretical Computer Science, 1, 1995. Reprinted in [34, vol. 2, pages 189–225].

[29] Uday S. Reddy. Global state considered unnecessary: An introduction to object-based semantics. Lisp and Symbolic Computation, 9(1):7–76, February 1996. Reprinted in [34, vol. 2, pages 227–295].

[30] John C. Reynolds. Idealized Algol and its specification logic. In Danielle Néel, editor, Tools and Notions for Program Construction, pages 121– 161, Cambridge, England, 1982. Cambridge University Press. Reprinted in [34, vol. 1, pages 125–156].

[31] Robert D. Tennent. Semantical analysis of specification logic. Information and Computation, 85(2):135–162, April 1990. Reprinted in [34, vol. 2, pages 41–64].

[32] Peter W. O’Hearn and Robert D. Tennent. Semantical analysis of specification logic, 2. Information and Computation, 107(1):25–57, November 1993. Reprinted in [34, vol. 2, pages 65–93].

[33] David Gries, editor. Programming Methodology. Springer-Verlag, New York, 1978.

[34] Peter W. O’Hearn and Robert D. Tennent, editors. ALGOL-like Languages. Birkhäuser, Boston, Massachusetts, 1997. Two volumes.