CMU 15-671  Models of Software Systems  Fall 1995

Seq Satisfies Set

Garlan & Wing  Handout 11  9 October 1995

The motivation for this example is show you that when you do “object-oriented” programming, you are really identifying certain abstract objects (better known an data abstractions or abstract data types) like sets, stacks, queues, symbol tables, etc.. You eventually have to realize (i.e., implement) these objects in a real programming language in terms of either other abstract objects or the language’s built-in data objects like sequences, arrays, records, linked lists, etc. After you write your (concrete) implementation you are then faced with proving it correct with respect to the (abstract) specification.

Not surprisingly, these data objects (abstract or built-in) can themselves be viewed as little state machines. So, to show the correctness of an implementation of an abstract object is very much like showing that one state machine (the concrete one) satisfies another (the abstract one).

There are other proof techniques used to prove the correctness of the implementations of abstract data types. You may see them in the Methods Course (when you learn about object-oriented programming) and/or the Analysis course (when you learn about program verification).

1 Abstract Machine: Set

My Set abstract machine has the following interface:

Set = (

{s : {t} → set[int]},

{s : {t} → set[int] | s(t) = �},

{insert(i : int)/ok(),… see above …, pick()/ok(int)}, δ_{A} = … see next page … ).

Here are specifications of the actions, insert, delete, card, member, and pick. insert(i: int)/ok()

\begin{matrix}c \\ ◯ \end{matrix}1995 Jeannette M. Wing

pre true post t′ = t ∪ {i}

delete(i: int)/ok()

pre true post t′ = t \ {i}

card()/ok(int)

pre true post t′ = t ∧ result = #t

member(i: int)/ok(bool) pre true post t′ = t ∧ result = (i ∈ t)

pick()/ok(int)

pre t ≠ � post t′ = t ∧ result ∈ t

2 Concrete Machine: Seq

I’ve decided that I want to implement the Set machine in terms of a Seq machine with the following interface:

I’m going to define the actions such that the state where q = ⟨3, 5, 5⟩ is unreachable. You’ll see why soon.

Seq = ( {s : {q} → seq[int]}, {s : {q} → seq[int] | s(q) = ⟨⟩}, {addh(i : int)/ok(),… see above …, fetch(i : int)/ok(int)}, δ_{C} = … see next page … ).

Seq’s actions have the following specification: addh(i: int)/ok()

pre i ∉ ran q post q′ = q � ⟨i⟩

remh()/ok(int)

pre q ≠ ⟨⟩ post q = q′ � ⟨result⟩

size()/ok(int)

pre true post q′ = q ∧ result = #q

isin(i: int)/ok(bool) pre true post q′ = q ∧ result = (i ∈ ran q)

fetch(i: int)/ok(int) pre q ≠ ⟨⟩ ∧ i ∈ dom q post q′ = q ∧ result = q i

3 Proof of Correctness

Formally, RI and AF are defined over Seq’s set of states, but it’s going to be notationally convenient (and I hope more understandable) if I denote each of these states by the sequence value to which Seq’s state variable, q, maps. In other words, I should write something like:

RI (s(q) = ⟨3, 5, −1⟩) = …

but instead I’m going to write:

RI (⟨3, 5, −1⟩) = …

3.1 Step 1

I first need to define an abstraction function and a representation invariant.

1. Abstraction Function.

Informally AF takes an (ordered) sequence of elements and turns it into an (unordered) set of the sequence’s elements. Formally,

AF : seq[int] � set[int] AF (⟨⟩) = � AF (q � ⟨e⟩) = AF (q) ∪ {e}

It is common for abstraction functions to be defined recursively like this.

Notice that this AF is many-to-one. There are many sequence values that map to the same set value because we don’t care what the order of elements is in a set. In fact, the orderedness property of sequences is exactly the “irrelevant” property from which we abstract. For example,

AF (⟨3, 5, −1⟩) = {3, 5, −1} AF (⟨5, 3, −1⟩) = {3, 5, −1} AF (⟨−1, 5, 3⟩) = {3, 5, −1} These three different sequence values map to the same set value.

2. Representation Invariant.

Notice that the addh action has a pre-condition that checks whether the element to be inserted is already in the sequence. Thus, only sequence values that have no duplicate elements serve to represent set values. We have the following representation invariant, which characterizes the domain of AF :

RI : seq[int] → bool

RI (q) = ∀ 1 ≤ i, j ≤ #q • i ≠ j ⇒ q i ≠ q j

Informally I’ll call this representation invariant, NoDups. Thus we have,

RI (⟨3, 5, 5, −1⟩) = false 5 appears twice.

RI (⟨3, 5, −1⟩) = true NoDups

RI (⟨⟩) = true The empty sequence is ok.

All those sequence values that RI maps to true are legal representations of set values.

IMPORTANT: Remember that there’s a side proof that we need to do here. We need to show that the representation invariant is indeed an invariant. That is, along the lines of the proof technique described in the handout on Reasoning About State Machines, we need to show that the invariant is established in the initial states and preserved by each action. I’ll leave this part of the proof as an exercise to the reader.

Here’s a picture illustrating that AF is partial and many-to-one:

3.2 Step 2

Armed with RI and AF , I can now show the concrete machine satisfies the abstract one.

1. Initial condition.

We need to show that each initial state of Seq maps to some initial state of Set. More formally, we need to show that AF (⟨⟩) = �. This is obviously true by the definition of AF .

2. Commuting diagram for each Seq action.

I need to show this diagram:

There are five cases, one for each Seq action. I’ll just do three actions, addh, remh, and size.

Case: addh satisfies insert.

We’ll first consider the case where i is not in the sequence and then the case for when it is.

Case 1: i ∉ ran q

According to the post-condition for Set’s insert action we need to show that the set value for t′ obtained after doing an insert with argument i is t ∪ {i}. Seq’s addh action has the effect of adding to the high end of the sequence only if its argument i is not already stored in the sequence. Thus if q is the value of the sequence before, then q � ⟨i⟩ is the value after. In other words, we have:

AF (δ_{C} (q, addh(i)/ok()))

. = AF (q) � ⟨i⟩) post-condition of addh = AF (q) ∪ {i} def’n of AF = t ∪ {i} since t = AF (q) = t′ post-condition of insert

Case 2: i ∈ ran q

If i is already in the sequence then no state transition occurs and q stays the same.

Case: remh satisfies delete.

According to the post-condition of Set’s delete action the set value for t′ obtained after doing the delete is the set with i removed. Seq’s remh action has the effect of removing and returning the high end of the original sequence q. Informally speaking, it’s this element result, which we would “pass to” delete as an argument. In other words, given a particular state transition involving remh, I am choosing a particular state transition involving delete—the one for which result is passed as an argument. We have:

δ_{A}(AF (q), delete(result)/ok())

= δ_{A}(AF (q′ � ⟨result⟩), delete(result)/ok()) post-condition of remh

= δ_{A}(AF (q′) ∪ {result}, delete(result)/ok()) def’n of AF

= (AF (q′) ∪ {result}) \ {result} post-condition of delete (and def’n of δ_{A}) = AF (q′) properties about set union and set difference = t′ t′ = AF (q′)

Case: size satisfies card Looking at the post-condition for Set’s card action, there are two things to show. First, we need to show that the value returned by the Seq’s size action is the size of the corresponding

set (under AF ). Because of NoDups (the RI ), we know that the size of the sequence representing a set is the size of the set it represents. More formally, you would need to prove a lemma like:

Lemma 1 ∀ q : seq[int] • (#q = #AF (q))

Second, we need to show that size does not change the abstract value of the set that q represents. More formally,

q′= q

⇒ post-condition of size AF (q′) = AF (q) ⇒ AF is a function. t′ = t

IMPORTANT: Notice that we rely on the abstraction function AF on being a function here. In the second step above, we apply AF to two equal things; since AF is a function (and not a relation), we know the result of applying AF to two equal things will result in two equal things.

For your homework, it’s okay to give informal proofs like the ones I give here.