Re: Generic Package

[Georg Bauhaus <bauhaus@futureapps.de>]

On Tue, 2007-05-01 at 19:16 +0200, Dmitry A. Kazakov wrote:

> Apart from obvious uselessness of contracts referencing to the memory
> layout,

I didn't say that.

> the above is self-contradictory. Memory layout defines an order. It
> also is a part of the contract.

Memory is not abstract, addresses aren't abstract, but what I
have described as a formal model is abstract.

>  Hence the interface is ordered.

The abstraction of the implementation implies the existence
of a possible internal private ordering. The order can be completely
controlled by an implementation and it won't be "reachable"
through the public Set interface.

Randy has explained much more about possible internal orderings.


> >     -- 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?

The proof mentions that Count_Var is initially zero and that
it is only changed by Add_One. Together with the fact that these
are (1) a local variable and (2) a local procedure
closely tied this should imply that pre: Count_Var = 0.

> 2. because pred (Add_One) = true, that also includes Count_Val = N + 1.

This is not a possible interpretation of the program as given
(because Count_Var := 0 immediately before Foreach is called),
but you are right that the precondition is not explicitly stated.



> > 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.

?
The first book might be determined by whatever order the librarian
thinks he should choose this time. Nothing I could determine beforehand.
The order(s), if any, isn't/aren't publicly known.


> >>>> 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.

What's the contract of "in"?