ChangeLog
=========

Revision 1.6.0:
===============
 * Support for Strings
 * Enhanced JML support
 * Improved integration of external SMT solvers
 * Improved "verification-based testing" mechanism
 * Real Time Java (RTSJ) calculus
 * GUI improvements
 * Various bugfixes


Revision 1.4.0:
===============
 * Unified proof obligation framework
     ** sharing of proof obligations across different specification languages
     ** unified API for adding new proof obligations
     ** same GUI elements used for all specification languages
     ** more elegant translation of \old, @pre-like constructs
 * Improved JavaCard DL Specification interface
     ** specification of DL invariants
 * Rewrite of JML front-end
     ** ghost variables/fields and JML set statement
     ** non_null by default
     ** \old in loop invariants supported
     ** \object_creation(type) in JML assignable clauses
 * New standalone OCL front-end
     ** discontinued support for Borland Together integration
 * Java language support enhancements:
     ** enum types (partially)
     ** inner and anonymous classes
     ** enhanced for loop
     ** variable method arguments
     ** covariant method signature
 * Generation of JML specifications
 * Strictly pure queries can be pushed directly into an update
 * Stable proof loading and saving
 * Classpath directive
 * various bugfixes


Revision 1.2.0:
===============
 * significantly improved proof strategies wrt. quantifier treatment
   and arithmetics
 * improved proof tree view, i.e. 
     ** hiding of closed subtrees
     ** hiding of intermediate proof steps
     ** search in proof tree  
 * improved proof saving and loading
 * includes _alpha_ version of the visual debugger 
 * various bugfixes 
 
Revision 1.0.1:
===============
  * fixed an installation problem when KeY had not been installed before

Revision 1.0.0:
===============

  * KeY-Book examples are based on this version
    (except Schorr-Waite, which provides a developer version on 
    the book example site)
  * new proof-obligation generation framework 
         * used currently only by the OCL translation; 
            adaption of JML translation is underway
  * new method lemma rule
  * considerable improvements concerning arithmetics
  * lots of bugfixes and improved stability

Revision 1.0pre1a:
==================
  * bug fixes and improvements
  * polynomial integer simplification

Revision 1.0pre1:
================
  * pre-release of upcoming 1.0
  * several improvements and fixes


Not yet integrated (targeted for >= pre2):
  * new proofobligation generation
  * new method lemma generation
      
      
Revision 0.99.2: 
================
   * fixed: Initialisation procedure of the KeY prover
            (KeY did not work properly if installed on a fresh system
             without a working KeY configuration file) 
   * fixed: Source Code Distribution 0.99.1 was way too big

Revision 0.99.1: 
================
   * bug fixes concerning JML front-end

Release 0.99: 
=============
   * first version with the JML front-end
   * support of loop invariants
   * lots of new stuff