Skip to main content

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index] [List Home]
[stellation-res] JML

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



Back to the top