RE: [stellation-res] JML

["Jonathan Gossage" <jgossage@xxxxxxxx>]

I havn't had a chance to try it yet because I have been involved in the
refactoring. I am just starting something at work
where I could try it out today and let you know what I think

Regards

Jonathan

> -----Original Message-----
> From: stellation-res-admin@xxxxxxxxxxxxxxx
> [mailto:stellation-res-admin@xxxxxxxxxxxxxxx]On Behalf Of Mark C.
> Chu-Carroll
> Sent: Wednesday, October 29, 2003 10:14 PM
> To: stellation-res@xxxxxxxxxxxxxxx
> Subject: [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
>
> _______________________________________________
> stellation-res mailing list
> stellation-res@xxxxxxxxxxxxxxx
> http://dev.eclipse.org/mailman/listinfo/stellation-res
>