[Prev][Next][Index]
Re: A miscellany

To: horning

Subject: Re: A miscellany

From: davidg@oracorp.com

Date: Fri, 27 Aug 93 17:53:12 EDT
Jim,
It seems we agree about essentially everything except, possibly, the
implications of all the things we agree about.
> But for this to really specify perm properly, the operators on bags that
> are used have to be pinned down pretty precisely. I'd expect that
> regardless of the model chosen, all the terms that are used in the
> specification of perm are completely determined. (If they aren't, perm
> isn't guaranteed to test correctly for a permutation.) So within
> package integer_lists there isn't any difference between the E and
> Ainterpretations.
Yes. Something like this is no doubt true. The devil comes in
formulating precisely what it is that the user must do to persuade
himself that two Especifications can be combined.
I now have to run off to Washington for a few days and beg for money.
Here is one further consideration that might be of interest. What are
the different proof procedures associated with showing that an A or
E specification is satisfied? and what are the proof procedures
associated with being a client of an A or E specification? They go
like this (I'll do it for a procedure):
Note: For technical reasons, I'm going to assume that a basic
condition of "semantic wellformedness" for any 2tiered specification
is that the mathematical part be consistent. First of all I'll
distinguish between the visible spec of a procedure and its body.
Visible spec:
procedure Q;
Mathematical part: theory T1
Interface part: ... whatever ...
This defines the specification of Q from the point of view of a
client.
Body:
procedure Q is
begin ... end;
Mathematical part: theory T2
Interface part: ... for simplicity's sake, the same  although
it needn't be ...
By definition, T2 includes T1. T2 may also contain auxiliary notions
needed to define loop invariants, the theories associated with units
that the body of Q imports but which are not visible to the clients of
Q, etc.
Consider first the implementor of an A or E spec:
To prove that Q satisfies the Aspec we must guarantee that the theory
T2 is a conservative extension of T1. (This actually requires me to
liberalize the definition of Asatisfaction slightly: it comes to
saying that for every model of T1 has an elementary extension in which
the interface specifications are true. This liberalization makes no
difference to any observable effects of Q.)
To prove that Q satisfies the Espec we need only know that T2 is
consistent (which we're already assuming as part of "semantic
wellformedness").
Now consider the client of an A or E spec:
Visible spec:
with Q;
procedure R;
Mathematical part: theory X1
Interface part: ... whatever ...
By definition, X1 contains the mathematical part of the specification
of Q. Now the situations is dual to the preceding one.
If the spec of Q is an Espec, then we must know that X1 is a
conservative extension of the mathematical part of the specification
of Q. If the spec of Q is an Aspec, then we need only know that X1
is consistent.
Things get more complicated if R is "with" several units having
Especifications, because then X1 would have to be a conservative
extension of them individually (certainly)  actually, I think, a
conservative extension of the union of the mathematical parts of
subset of the imported units. (I forget because it's been a while
since I thought about this in detail.)
 David
davidg@oracorp.com