Re: Generic Package

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

On Tue, 01 May 2007 23:41:31 +0200, Georg Bauhaus wrote:

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

But I did! (:-))

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

In what sense? 

[ I doubt that you were able to bind objects of a higher level language to
"non-abstract memory" in a more or less formal way. It is yet another
discussion, we probably should not go into. The states of the memory are
associated with some computational states and those with some objects
"having" some values. It is a tick Napoleon pastry of abstractions layered
over abstractions which you would not be able to flatten. As a practical
example consider

for I in ... loop
   -- what is I'Address here?

can you specify the transistors I has? ]

> The abstraction of the implementation implies the existence
> of a possible internal private ordering.

No, that is of course wrong. An abstraction of unordered set does not imply
anything beyond itself.

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

So, the precondition is not constant true, it is Count_Var = 0? Then either

1. N = 1

or

2. The program is incorrect, because for any N > 1  your precondition gets
violated on the second call to Add_One.

Here you are. You cannot specify the precondition of Add_One without
referring to the iteration state. You are caught in a circle of
tautologies.

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

No, first = [whatever] order. It is same.

> Nothing I could determine beforehand.

"Beforehand" means what? I hope it does not that you present one set while
dealing with another. Ordering is determined by sole existence of the
librarian who can give you a [first] book and continue to do so.

> The order(s), if any, isn't/aren't publicly known.

It is, if you don't cheat. The procedure was described by me in other post.

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

One of the set theory. You choose the language and a set of axioms, and
likely "in" will be somewhere there. So "in" is in a different position
than ordering. In ZF ordered pairs are not fundamental, they are
constructed. So we could talk about the contracts of on "ZF hardware."

Of course it depends on the hardware. Nobody would construct, say, integers
as they are constructed in ZF, because there is the ALU, which we could use
instead. So "+" becomes per magic. Same is with foreach, you could have a
hardware (axioms) for it. In that case it would have no contract.

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