search

kiniry / Mobius

4 stars 8 forks source link

ESC/Java2 support for JML 5.5 keywords #288

Open atiti opened 11 years ago

atiti commented 11 years ago

{{{

!html

Reply to: Dermot Cochran }}} {{{

Begin forwarded message:

From: "Gary T. Leavens" leavens@eecs.ucf.edu Date: January 10, 2008 4:39:50 AM GMT+00:00 To: JML Release Notifications <jmlspecs- releases@lists.sourceforge.net> Subject: [Jmlspecs-releases] JML Release 5.5 now available

Hi,

We've finally made the 5.5 release of the JML tools. This release is available from from the sourceforge project page for JML http://sourceforge.net/projects/jmlspecs or directly from sourceforge.net http://sourceforge.net/project/showfiles.php?group_id=65346 in the file JML.5.5.tar.gz. This is a gzipped tar file.

Some highlights of the release are summarized below. See the NEWS.txt file in the release for other changes, including changes inherited from the previous release of JML (more or less) and many bug fixes. Highlights include:

  - Various changes enable the new assertion semantics.  This
    semantics requires that users write "protective"

specifications, in that the runtime checker will no longer attempt to mask exceptions that occur during assertion evaluation, but will instead propagate those out to the calling program. Thus an assertion holds if and only if the assertion
expression evaluates successfully (no exceptions are raised) and it is
true. This new semantics has been turned on by default (to
recover to old semantics use jmlc command line option -O). This fixes bug

1745623. Thanks to Patrice Chalin and Fredrick Rioux.

  - Added the "refining" statement discussed in the jmlspecs-

interest mailing list and a new keyword "extract" from the paper by Shaner, Leavens and Naumann (to appear in OOPSLA 2007). This updated the checker and documents. Thanks to Steve Shaner.

See the NEWS.txt file in the release for more details, bug fixes, and incompatabilities with the previous release.

Please let us know your comments on JML, and if you find bugs. You can now file bug reports from the sourceforge.net project page for the jmlspecs project, http://sourceforge.net/projects/jmlspecs and you can see the bugs we know about there.

     Gary T. Leavens
     Department of Computer Science, Iowa State University
     229 Atanasoff Hall, Ames, Iowa 50011-1041 USA
     http://www.cs.iastate.edu/~leavens  phone: +1-515-294-1580

     Gary T. Leavens
     210 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@eecs.ucf.edu

Check out the new SourceForge.net Marketplace. It's the best place to buy or sell services for just about anything Open Source. http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/ marketplace

Jmlspecs-releases mailing list Jmlspecs-releases@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/jmlspecs-releases

}}}

atiti commented 11 years ago

From: Dermot Cochran (GH: None) Date: Thu Jan 10 12:17:59 2008

added mailto line

This message has 1 attachment(s)

atiti commented 11 years ago

From: dcochran (GH: dcochran) Date: Wed Feb 20 12:05:05 2008

Either JML4 or OpenJML or both, but not JML5

atiti commented 11 years ago

From: dcochran (GH: dcochran) Date: Mon Jun 30 11:36:23 2008

Milestone ESCJava2.0b5 release deleted