[
Date Prev][
Date Next][
Thread Prev][
Thread Next][
Date Index][
Thread Index]
[
List Home]
Jonathan (or anyone else active out there):
Have you tried using JML for any of the work you're doing on Stellation?
(Or for anything else for that matter?)
If so, can you send a quick summary to the list of your experience with
it?
I'm just starting to try to use it for the new API implementation, and
I'm finding
it frustrating. It seems as if it's positioned itself in a rather
bizzare niche semantically.
What I mean by that is, it seems as if wants to be tied to the
programming language
very directly, so that the specifications use Java syntax and
semantics; at
the same time, it wants to have a degree of analyzability which goes far
beyond Java. If I'm doing it right, the result is that you get a
bizzare situation where most
of the things that you might like to use for specifying a real program
are off
limits, because they don't have the properties that allow them to be
used in
the JML spec; at the same time, JML doesn't include the expressive tools
that you would want to specify things, because they want you to use
Java. So you end up with these bizzare double implementations, where
you write a real method, which operates with side effects on a data
structure,
and a specification method which does the same thing in an awkward
way using the pure classes from the JML library.
The thing is, I know some of the people involved in JML, and I find it
hard to believe that they'd make a mistake like this, so I'm wondering
if I'm just not grokking it because
I'm not approaching it correctly.
So I'd like to hear about any experience or opinions that anyone else
has
concerning using JML on real systems.
-Mark
Mark Craig Chu-Carroll, IBM T.J. Watson Research Center
*** The Stellation project: Advanced SCM Research
*** http://stellation.eclipse.org
*** Work: mcc@xxxxxxxxxxxxxx/Home: markcc@xxxxxxx