FWD: Query on Larch and OOA


I would like to add to Jim Horning's comments.  First, you should
definitely look at Gary Leavens's work on Larch/C++ (there will be a
paper in ACM TOSEM coming out on it soon).

Second, you might also want to look at the work done by Barbara Liskov
and myself on using specs to define a subtype relationship.  A paper
on this work will appear in TOPLAS.  We happen to use Larch-like
specs, but the point is more that you can use Larch-like interface
specs to specify classes and their subclasses and determine whether a
subtype relation holds between them based on these specs.  To me, it
makes more sense to capture this relationship at the interface level,
not the trait level.  Thus, I would keep LSL the way it is and support
different kinds of subtyping/subclassing (and other OO) relationships
at the interface level, depending, of course, on what your programming
language's semantics of subtyping/subclassing is.  The Larch
two-tiered approach is especially nice for this separation of
concerns, unlike the Object-Z approach where all issues get rolled
into the same specification.

You can get to all this work from the Larch Home Page that Jim mentioned.
To save you some navigation, the url for my personal home page is:


Jeannette Wing