Skip to main content

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

Can you post any samples where you are finding problems?

Regards

Jonathan


----- Original Message ----- 
From: "Jonathan Gossage" <jgossage@xxxxxxxx>
To: <stellation-res@xxxxxxxxxxxxxxx>
Sent: Thursday, October 30, 2003 6:47 AM
Subject: RE: [stellation-res] JML


> 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
> >
>
>
> _______________________________________________
> stellation-res mailing list
> stellation-res@xxxxxxxxxxxxxxx
> http://dev.eclipse.org/mailman/listinfo/stellation-res



Back to the top