[Prev][Next][Index]
A miscellany

To: larchinterest

Subject: A miscellany

From: davidg@oracorp.com

Date: Thu, 26 Aug 93 13:00:28 EDT
Some miscellaneous questions about LSL and about 2tiered
specifications:
1. Some time ago I asked why the LSL didn't contain a notion of
"freely generated by". This precipitated a discussion of whether it
wouldn't be better to introduce a more general notion of "free"  in
terms of which "freely generated by" would become a definable special
case. That discussion ended inconclusively. Here is a report from
the (pragmatic) front: We've built "freely generated by" into our
homegrown LSL editor; we use it all the time; and we have not yet
felt the lack of a more general "free" construct.
2. I don't want to be always beating the drum for "features," but ...
we have found it very convenient to have a direct way to express
induction principles other than structural induction. So, for
experimental purposes, our homegrown editor includes a new assertion
of the form
wellfounded R
where R must be an operator whose signature has the form S,S > Bool
for some sort symbol S. This provides the schema of complete
induction over R. Whenever the user is required to prove this
assertion he discharges the obligation by doing the obvious thing:
namely, for some fresh predicate symbol of signature P:S>Bool, prove
the corresponding instance of complete induction.
So, for example, we have things like
WF: trait
introduces
R: Domain, Domain > Bool
asserts
wellfounded R
implies
forall [d:Domain]
(not R(d, d))
where the implication is proven by induction on R, and
InducedWF: trait
assumes WF
introduces
f: Element > Domain
Rf: Element, Element > Bool
asserts
forall [e1, e2:Element]
(Rf(e1, e2) = R(f(e1), f(e2)))
implies
wellfounded Rf
where the well foundedness of Rf with respect to an arbitrary
predicate Element>Bool is proven by induction over R, and
Lists: trait
includes ...
includes InducedWF(
Int for Domain, < for R,
length for f, less_than for Rf
)
introduces
...
length_less: list,list > Bool
asserts
forall l1,l2:list
...
length_less(l1,l2) = length(l1) < length(l2)
implies
wellfounded length_less  This is free from InducedWF
When you really want to do a proof by induction on the length of
sequences it's much nicer, and clearer, to do so directly than to
translate that argument into a structural induction over the
construction of the natural numbers.
3. A question about the official ideology of 2tiered semantics: In
places like Jeanette Wing's thesis the semantics of a specification
like
use trait Blah
module stack is
procedure push ...
... entryexit annotations ...
end;
is this: There exists *some* algebra satisfying the axioms of Blah
with respect to which the annotations of the module are true. I now
think that was a mistake, and it would be better to adopt the dual
interpretation, according to which the annotations are true for
*every* algebra modeling Blah. It's possible to formulate proof
obligations corresponding to either of these interpretations. Here
are what seem to me the central considerations. (For the rest of this
chat I'll call the official interpretation the Einterpretation and my
proposed revision the Ainterpretation.)
a. What's lost: With the Ainterpretation you lose the ability to
express a specification such as: "Implement an arbitrary group, I
don't care which one." Not being able to express this particular
specification seems to me no loss at all. How about: "Implement a
bounded stack of fixed size c, for some c that's at least 100." This
is more reasonable, and to me it's only barely plausible that somebody
might want to say this. I think it's more likely that that spec is a
muddled way of saying something like: "Implement a generic bounded
stack parameterized by its maximum size" and then instantiating that
generic with a parameter known to be at least 100. (It's possible to
formulate proof obligations that will do generics correctly. [And see
c, below.])
b. What's gained: With the Ainterpretation you gain compositionality
as a practical possibility. Composing two Especifications is, in
general, a mess. Consider:
Blah1: trait
includes Set(Intset,Int)
...
Blah2: trait
includes Set(Intset,Int)
...
with Blah1
module Abstraction1 ...
with Blah2
module Abstraction2 ...
Let's imagine that the abstractions being defined by these modules are
not based on Int and Intset, but merely use these sorts as auxiliary
notions.
Suppose the annotations of Abstraction1 and Abstraction2 have the
Einterpretation. Let Alg1 be the algebra with respect to which the
annotations of Abstraction1 are true, and let Alg2 be analogous.
Notice that there is no guarantee that the interpretations of Int in
these two algebras are the same (i.e., isomorphic); and even if they
are isomorphic, it will require an argument to establish that the
isomorphism between interpretations of Int can be extended to one
between the interpretations of Intset.
Note what this implies if we want to use both Abstraction1 and
Abstraction2 in order to implement some other module: It may not be
possible to identify the meaning of Int (or Intset) supplied in the
annotations of Abstraction1 with the meaning supplied in the
annotations of Abstraction2. That is, there might not exist a single
algebra with the property that it satisfies both Blah1 and blah2,
*and* that the annotations of these modules, interpreted with respect
to that single algebra, are true. (Or, if there is such an algebra,
we may made need some heavy arguments to prove it.) whenever we
can*not* justify identifying these symbols, then we have to
distinguish them by renamings, and the rules stipulating what we must
rename can become rather complicated. *And* after we've satisfied
logical necessities by renamings we may wind up with many "copies" (or
pseudocopies) of all kinds of mathematical notions, including the
most familiar.
This really is a mess. The problems simply disappear if we instead
adopt the Ainterpretation.
So, my argument is that the official interpretation of 2tiered
specifications should change from E to A, because the gains overwhelm
the losses. What, if anything, is wrong with this argument?
c. Note: the legitimate place for an Einterpretation arises in
interpreting the formal parameters of generics. That is, if I say
(using the notation of Ada)
generic
type T is private;  matches (almost) any type
type index is <>;  matches discrete type
type T_array is array(index) of T;
with function less_than(x,y: T) return boolean;
"less_than must be a total order of T"
 function parameter
procedure sort(A: in out T_array);
"the out value of A must be a sorting of its in value with
respect to less_than"
then, as far as the implementor of procedure sort is concerned, the
annotations of less_than have Einterpretation: He may assume only
that there is some total order with respect to which the annotations
of the actual function matching less_than will be true.