Hi John,
On Thu, 18 Sep 2008, John Simmons wrote:
> I hope you don't mind my contacting you. I am trying to learn JML from
> the papers listed on the JML site, and am having a difficult time with
> it. You are an author of several of the papers, so I thought I would
> try asking you for guidance.
>
> I read your paper "Design by Contract with JML," then started reading
> "JML: A Notation for Detailed Design." I quickly realized that this
> later paper was several years older, and that the notation may be out of
> date.
Yes, the second paper is a bit out of date, but not in the big
picture. You could read the "Preliminary Design of JML" paper for
more examples and explanations.
> In particular, I don't understand the various files with extensions like
> ".java-refined", ".jml-refined" in the older paper, and ".refines-java"
> in the newer paper.
The most common way to use JML is to use .java files only, with the
specifications in these files directly. Some papers use multiple
files partly as a way to split large figures into smaller bits that
will fit on pages. But these can also be used to separate parts of a
specification or to separate specifications from code. The most
common use is when the code is controlled by someone else (e.g., it's
in a library) and you don't want to change the code files directly.
Then the typical usage would be to augment a .java file, say Foo.java,
with a .refines-java file, say Foo.refines-java. In the
Foo.refines-java you would write JML specifications for things in the
.java file. You also must say, in Foo.refines-java:
refines "Foo.java"
The two files are added together by jmlc and other tools to form a
specifiction with code combination, as if you had written everything
in one file.
> Is there a current, tutorial introduction that I could use to get me to
> the point where I can actually write JML specifications, and understand
> how to organize them in my .java and other files?
There are some tutorial slides in
http://www.eecs.ucf.edu/~leavens/JML/TeachingMaterial/CAV2007Tutorial/JMLTutorialPresentationWithNotes.pdfSee also the examples page for various instructive examples of
JML. In particular look at the samples (which are also included in the
directory JML/org/jmlspecs/samples of the JML release). In particular,
look at the package org.jmlspecs.samples.dbc for examples in the
design-by-contract style that is most suitable for teaching students
about JML (and is also compatible with ESC/Java).
Gary T. Leavens
439C Harris Center (Bldg. 116)
School of EECS, University of Central Florida
4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
http://www.eecs.ucf.edu/~leavens phone: +1-407-823-4758
leavens@...
-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/_______________________________________________
Jmlspecs-interest mailing list
Jmlspecs-interest@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest
