Re: Generic Package

[Georg Bauhaus <bauhaus@futureapps.de>]

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. However, it is then known that the elements of sets
in a computer have said properties. These properties will assign
meaning to the phrase
 "Procedure Foreach calls procedure P once for each element of S"
or, put differently but still with just logical references to
implementation details, "For each node of the set S, the node will
be used as the actual argument of P when P is invoked; this is
done once for each node of S in an unspecified order."
 There isn't much a client (programmer) needs to know about nodes.
He or she isn't concerned with implementation details.
But the abstract notions of what is implemented provide enough
formal information so that the operation of Foreach can be
described formally. (Just not in terms of its own inner workings
as a postcondition stating foreach in terms of foreach. So what?)

As a consequence of this formal description, ("nodes", "called once",
"each") I can call Foreach passing a procedure Add_One that increments
a count variable when called. Provided there is a query function
Length of Set (as is typically the case), then (remove quantifiers
if more apt)

 function Unnamed(S: Set) return Count_Type;
 -- post: (∀s) s in Set [ s.Length = Result ]

 function Unnamed(S: Set) return Count_Type is
    count_var: Count_Type;
    procedure Add_One(C: Cursor) is
    begin
       count_var := count_var + 1;
    end;
 begin
    count_var := 0;
    Foreach(S, Add_One'access);
    -- Claim (∀s) s in Set [ s.Length = count_var ]

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

    pragma assert(Length(S) = count_var);
    return count_var;
 end;

If there is no Length defined for Set, the above is still enough,
to me at least, to show that this computes the number of elements
in a Set using a computer representation even when there is no known
order of elements and without knowledge of the actual implementation.

I think it is possible to add even more contract clauses almost
like the ones you have mentioned:

function First(S: Set) return Cursor;
  -- post: let (Result then t0) = (First(S) then Clock),
  --           (Result' then t) = (First(S) then Clock) in
  --         (∀t) t > t0 [ Result /= Result' ]

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



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