Re: Generic Package

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Tue, 01 May 2007 15:42:21 +0200, Georg Bauhaus wrote:

> On Tue, 2007-05-01 at 12:19 +0200, Dmitry A. Kazakov wrote:
>> On Tue, 01 May 2007 11:02:22 +0200, Georg Bauhaus wrote:
>> 
>>> On Mon, 2007-04-30 at 22:04 +0200, Dmitry A. Kazakov wrote:
>>>> It was that if foreach were a primitive operation
>>>> defined on an unordered set, then its contract could not be stated.
>>> 
>>> Every specific Set object (collection of elements) inside a computer has
>>> a memory layout.
>> 
>> So the memory layout is a part of the contract?
> 
> Yes, in the sense that the specifics of memory layout and such are
> unknown and irrelevant to the client; in particular, no order needs
> to be specified.

Apart from obvious uselessness of contracts referencing to the memory
layout, the above is self-contradictory. Memory layout defines an order. It
also is a part of the contract. Hence the interface is ordered.

>     -- Proof. Foreach calls Add_One exactly once for each node
>     -- in s. Add_One unconditionally increments Count_Var by 1.
>     -- No other operation changes the value of Count_Var.
>     -- Hence, Count_Var (initially zero) is incremented by 1 for
>     -- each node in s, so Foreach counts the elements of s. ∎

So the precondition of Add_One is true? Then your proof is wrong. Here is a
counterexample:

1. let S'Length = N

2. because pred (Add_One) = true, that also includes Count_Val = N + 1. So
let's take it.

3. observe that for whatever number of calls to Add_One might then happen,
the result Count_Val is not N.

i.e. Count_Val = N does not follow from S'Length = N /\  pred (Add_One) =
true.

q.e.d.

(You cannot use true as the precondition. If you should to narrow it, for
this you need the invariant of the implicit loop behind "foreach," and that
would require ordering of S.)

> As you can see, there is some order again but I don't have to know
> the order. (Finding a first book (and then the next book) is the
> job of the librarian, not mine.)

Librarian is the interface. If it finds first book then that is a publicly
ordered set = you _can_ know the order without breaking the abstraction.

>>>> To be able to pick a random member <=>
>>>> to have an order.
>>> 
>>> Can you determine whether one of your sets is empty?
>> 
>> Sure. I can compare an empty set with the given set. This does not require
>> picking elements.
> 
> Uhm, not require the client to pick or the implementation to pick?
> When two sets A and B are equal iff the same elements
> belong to both A and B, won't you need at least references to the
> elements for "=" to be called for the elements?

No. You have to show that whatever element you took (no matter how) it is
either in both sets or else in neither:

   forall x in S, x in Q

This does not force you to present any method of getting elements from any
of the sets.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de