Re: Generic Package

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

On Wed, 02 May 2007 13:48:26 +0200, Georg Bauhaus wrote:

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

But I am not required to do so.

BTW 1, it is a quite common programming pattern to share some predefined
states of the container, usually empty ones, but not only. An
implementation of a container of integers could have a reserved
representation for contiguous ranges of integers. For these it would keep
only From and To. Now, let you have a container holding 1, 2, 3, can you
point me the address of 2 there?

Another typical pattern is some f applied to the actually kept values, so
"()" actually is a composition f o "()". So what is in the container?

BTW 2, it is sort of surprising to have such a discussion in c.l.a., for
Ada was one of the first languages introducing a clear distinction between
interface and implementation.

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

Huh, argumentation to Turing-completeness is a subject of Godwin's Law...

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

That still does not describe the precondition of. In particular, where it
follows that counts S and not something else? S have to appear there.

> So there is a well defined
> operation going on

It might be a well-defined operation, but its outcome is not.
 
>> 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?

Merely by saying/writing "first." That defines a book.
 
>> 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.

Come on, all orderings are ordered but some orderings are more ordered than
others? (:-)) _WHAT_ is the difference?  Let you asked somebody to bring
you books in their "proper" order. How can you determine if he does not
cheat, or just mistakenly used the issue date rather than the birth day of
the author written in Roman numerals and ordered according to Unicode
positions?

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