Re: Generic Package

[Georg Bauhaus <bauhaus@futureapps.de>]

On Wed, 2007-05-02 at 12:29 +0200, Dmitry A. Kazakov wrote:

> > Memory is not abstract, addresses aren't abstract,
> 
> In what sense? 

When you write a Set implementation for a PC, you can specifying
addresses and refer to addresses in a consistent way.

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

irrelevant without computational model. (I didn't say that the
mentioned abstract addressable node is good for everything.
But even so, it should not be too difficult to come up with an
AS-IF model of how I "work"; otherwise, Ada would have an
insurmountable teaching problem, besides other exegetic trouble.)


> can you specify the transistors I has? ]

no need.


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

I didn't say anything about unordered sets here. I have given
a description of an implementation model.

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

The program is correct; the assumption that Count_Var = 0 is
false and not the precondition of Add_One at each time. My fault
being sloppy.
("Count_Var is initially zero and ... is only changed
by 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.

Ok, Ok. There is a reason I didn't specify that as a precondition
for Add_One. Add_One adds 1 to whatever initial value Count_Var has.
It has the value 0 before the defined procedure Foreach starts
operating using Add_One, as described. So there is a well defined
operation going on and I can argue about this operation using the
formally defined abstraction "Iterator".


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

How is "whatever order" defined, exactly, and how can I say whatever
first book will come given a library?


> > Nothing I could determine beforehand.
> 
> "Beforehand" means what?

It means that it is impossible to predict an order because
nothing is known about any order by any client.


> Ordering is determined by sole existence of the
> librarian who can give you a [first] book and continue to do so.

That is, ordering is an outcome of the librarians operation,
not of the books.


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

OK

> Of course it depends on the hardware.

OK. Glad to hear someone recognizes the inversion that
mathematics brings in. Normative ontology at its best, though :-)