[Prev][Next][Index]

A miscellany


Some miscellaneous questions about LSL and about 2-tiered
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
home-grown 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 home-grown editor includes a new assertion
of the form

     well-founded 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
   well-founded 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
    well-founded 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
       well-founded 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 2-tiered semantics: In
places like Jeanette Wing's thesis the semantics of a specification
like

   use trait Blah
   module stack is 
     procedure push ...
     ... entry-exit 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 E-interpretation and my
proposed revision the A-interpretation.)

a.  What's lost: With the A-interpretation 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 A-interpretation you gain compositionality
as a practical possibility.  Composing two E-specifications 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
E-interpretation.  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
pseudo-copies) of all kinds of mathematical notions, including the
most familiar.

This really is a mess.  The problems simply disappear if we instead
adopt the A-interpretation.  

So, my argument is that the official interpretation of 2-tiered
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 E-interpretation 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 E-interpretation: 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.