@(#)$Id: NEWS.txt,v 1.159 2009/03/16 14:49:11 leavens Exp $

    NEWS.txt file for JML and the Common (formerly ISU) JML Tools

New with release 5.6_rc4 (Mar. 16, 2009)

   major improvements:

     - Model programs and refining statements are now parsed, type
       checked, and matching is enforced, using the design of the
       Shaner, Leavens, and Naumann OOPSLA 2007 paper.  This version
       does not yet support runtime assertion checking.  Thanks to
       Steve Shaner.

     - Addition of jmle, which is a tool for executing JML
       specifications.  This can be used to validate specifications,
       to debug them, and to allow specifications to serve as
       prototypes.  The jmle tool generates Java code, so it can be
       used as with any other Java code, in particular with JUnit unit
       testing.  For more information see the README.txt file in the
       org/jmlspecs/jmlexec directory or the paper
       by Krause and Wahls "jmle: A Tool for Executing JML
       Specifications via Constraint Programming" at 
       http://users.dickinson.edu/~wahlst/papers/tool.pdf
       Thanks to Tim Wahls.

   minor improvements:

     - Better handling of multi-dimensional arrays and a fixed null
       pointer exception in jmle, thanks to Tim Wahls. 

     - The jmle tool now correctly uses static fields from classes that are
       not compiled using jmle. Thanks to Timo Lindfors for reporting this
       bug, and to Tim Wahls for fixing it.

     - The ant tasks for JML are back in the jml-release.jar file.

     - Updates to the Universe type system, including support for
       Generic Universe types. The largest visible change
       is the improved defaulting of the ownership modifiers, which is
       now described in the JML Reference manual. Also
       multi-dimensional arays of primitive types can now take two
       ownership modifiers. Thanks to Werner Dietl.

     - Various fixes to the Universe type system annotations for the
       JDK (and the JML tools), thanks to Werner Dietl.

     - A temporary fix to bug #1961579, thanks to Tim Wahls and Werner
       Dietl for help on this.

     - A fix to the interface of java/util/Locale in Locale.jml.

     - An improvement to the specification of Method.invoke.  Thanks
       to Patrice Chalin.

     - Various fixes to the JML Reference Manual, thanks to Patrice
       Chalin, Jooyong Lee, Dan Zimmerman, Ghaith Haddad, and Neeraj
       Khanolkar.  In particular clarifications in the sections on
       quantifiers and set comprehensions to better describe some of
       the semantics and simplify the set comprehension grammar.

     - The parser will now properly escalate runtime exceptions,
       including NPE's, where it wasn't doing so before.  Thanks to
       Steve Shaner.

   incompatible changes:


# Copyright (C) 2008 University of Central Florida

# This file is part of JML

# JML is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2, or (at your option)
# any later version.

# JML is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
# GNU General Public License for more details.

# You should have received a copy of the GNU General Public License
# along with JML; see the file COPYING.  If not, write to
# the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.