next up previous
Next: Step 2 Up: Proof of Correctness Previous: Proof of Correctness

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,

tex2html_wrap_inline328
tex2html_wrap_inline330
tex2html_wrap_inline332

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,

tex2html_wrap_inline336
tex2html_wrap_inline338
tex2html_wrap_inline340

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:

tex2html_wrap_inline344
tex2html_wrap_inline346

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

  tex2html_wrap_inline348   tex2html_wrap_inline350   5 appears twice.

tex2html_wrap_inline352 = true NoDups

tex2html_wrap_inline356 = 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:

tex2html_wrap364


next up previous
Next: Step 2 Up: Proof of Correctness Previous: Proof of Correctness

Norman Papernick
Thu Mar 21 15:04:44 EST 1996