[Prev][Next][Index]

Re: A miscellany

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

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 E-specifications 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 well-formedness" for any 2-tiered 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 A-spec we must guarantee that the theory
T2 is a conservative extension of T1.  (This actually requires me to
liberalize the definition of A-satisfaction 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 E-spec we need only know that T2 is
consistent (which we're already assuming as part of "semantic
well-formedness").

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 E-spec, 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 A-spec, then we need only know that X1
is consistent.  

Things get more complicated if R is "with" several units having
E-specifications, 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