version 2.30, Oct 24, 2011
==========================

  o [Jessie and Krakatoa] manuals have been extensively updated to
    adopt the Why3 back-ends
  o [Jessie/Frama-C plugin] the default back-end is now to call Why3
    VC generator, and then the Why3 IDE. The former behavior can be
    obtained using option -jessie-atp=gui
  o [Krakatoa] new option -gen-only whichs stops after generation of
    jessie file. The default is now to start jessie and then Why3 IDE.
    the old usage "gwhy file.java" continues to use the Why2 backend.
  o [Krakatoa/Jessie/Frama-C plugin] fixed traceability issues
  o [Krakatoa/Jessie/Frama-C plugin] new backend using Why3 VC generator
  o [Jessie] add extensionality axiom to integer range type. allows to
    prove valid properties that were unprovable before.
  o [Caduceus] support discontinued, not distributed anymore
  o [Why3 output] support for syntax changes of Why3 0.70
  o [Why3 output] better explanations
  o [Why] fix encoding to multi-sorted logic with finite type
  o [Why] option -default-locs
  o [Why] added support for Vampire (based on simplify output)
  o [Why] option --delete-old-vcs erases previous files when using
    --multi-why or --multi-altergo
  o [Why] option --multi-altergo outputs VCs in separate files, like
    --multi-why but in Alt-Ergo's syntax instead of the general Why's
    syntax (e.g. algebraic types are encoded for Alt-Ergo)
  o [Jessie] fixed bug with region analysis, case of pointer
    comparison in annotations. fixes Frama-C BTS 0814
  o [Krakatoa] fixed a problem with scope of labels
  o [Krakatoa] fixed support for string constants
  o [Jessie] order of lemmas now kept the same as in the input. Fixes
    Frama-C BTS 0024
  o [Why lib] completed axiomatization of floats

version 2.29, Mar 1, 2011
=========================

  o [Krakatoa] Documentation: many errors fixed
  o [Jessie] plugin synchronized with Frama-C Carbon stable
  o [Why] fixed typing for division in programs
  o [Why] accepts "lemma" has keyword in input. outputs them accordingly
    for provers
  o [Why] Why3 output: avoids Why3 keywords
  o [Why] improved Gappa output

version 2.28, Dec 17, 2010
==========================

  o [Why] support for Coq 8.3
  o [Why] support for Alt-Ergo 0.92.2
  o [Coq output] removed dependencies on Float and Gappa libraries,
    added dependency on Flocq library
  o [Jessie] emit a warning when generating a dummy variant for
    recursive functions and loops (Frama-C bug 512)
  o [Jessie] preliminary support for \at in region computation
  o [Why] added --smtlib-v1 option (default smtlib format is v2.0)
  o [Why] added support for verit prover
  o [Why] improved support for integer division (better triggers)

version 2.27, Oct 14, 2010
==========================

  o [Why] fixed compilation with Ocaml 3.12
  o [Why] support for Alt-Ergo 0.92.1
  o [Why] fixed compilation with Ocaml 3.12
  o [Why] emacs mode distributed and installed
  o [Why] fixed bug 10851: wrong Coq output for if then else
  o [Why] distinction between computer division and math division
    Fixes Frama-C BTS 0539
  o [Why] added support for Why3 output syntax
  o [Jessie] improved translation of successive assignments on
    the same memory block. As a side effect, translation of
    array initializers from C is much better for provers.
    Fixes Frama-C BTS0377 feature request
  o [Jessie] disabled the experimental support for unions and pointer casts,
    since it is too buggy for public release
  o [Jessie] fixed bug with division by zero in expressions evaluated at
    compile-time (fixes Frama-C BTS0473)
  o [Krakatoa] error message when a comment starts with /*(extra space)@
  o [WhyConfig] bug fix when detecting a prover which was removed

version 2.26, May 10, 2010
==========================

  o [Why] fixed detection of Alt-Ergo
  o [GWhy] fixed some assert failure raised when .gwhyrc is absent
  o [Why] fixed mistakes with files extensions, which were introduced
    by the former fix for GWhy temporary files

version 2.24, April 19, 2010
============================

  o [Frama-C plugin] synchronized with Frama-C Boron 20100412
  o [Gwhy] better handling of temporary files
  o [Jessie] fixed bug 0443 (assigns \nothing and separation analysis)
  o [Jessie] fixed bug with assertions attached to behaviors
  o [Why] support for truncate_real_to_int in Gappa output
  o [Frama-C plugin] logic functions do not accept struct or union as
    parameters
  o [Jessie, Frama-C plugin] make the right difference between
    "reads \nothing" and no reads clause at all
  o [Jessie, Frama-C plugin] the "defensive" model for floating-point
    computations is now the default
  o [Jessie] fixed bug 0370: missing coercion on decreasing measures
  o [Jessie] support for "let x = t in a" when a is an assertion
  o [Frama-C plugin] support for statement contracts, fixes bug 0399
  o [Jessie] fixed bugs 0391 and 0401 (avoid name clash with axiom
    names and inductive case names)
  o [Jessie/Krakatoa/Frama-C plugin] fixed bug with labels inside \old
    and \at.  Moreover, label Pre is now allowed in function
    contracts, as specified in ACSL.
  o [Why] improved detection of external provers
  o [Frama-C plugin] option "-jessie-adhoc-normalization" triggers a code
    normalization suited for jessie without launching the analysis
    (fixes bts 332)
  o [Why] option "-output -" outputs the generated files (.why,
    .smt, .mlw) on stdout
  o [Why-dp] with the option "-simple" output only one line by goal
  o [Why-dp] option "-timeout 0" disables the time limit.
  o [Why-dp] option "-prover" allows to select the prover to use
    independently from the extension
  o [Why-dp] reads the file to send to the prover from stdin if no
    files are provided. In that case the option "-prover" is mandatory.
  o [Jessie] interpretation of floating-point parameters does not forget
    anymore the format of origin, which then provides proper bounds for them.
  o [Frama-C plugin] bts 0361 fixed: free allows NULL as argument
  o [PVS output] fixed problems with idents starting with underscore
  o [Krakatoa & Frama-C plugin] new pragma TerminationPolicy to allow
    the user to prevent generation of VCs for termination

version 2.23, December 4, 2009
==============================

  o [Why] fixed bug with let construct in logic
  o [Simplify output] fixed bug with function definitions
  o [GWhy] VC explanation when using --fast-wp option

version 2.22, November 30, 2009
===============================

  o [Jessie] fixed bug when return type is a logic type
  o [Krakatoa] fixed bug with final fields
  o [Frama-C plugin] fixed bug 0341
  o [Frama-C plugin] fixed bug 0034
  o [GWhy] Fixed pb default prover selection (BTS Frama-C 0037)
  o [Jessie] fixed problem with axiomatization of address operator
  o [Jessie/Krakatoa/Frama-C plugin] support for the 'for' modifier in
    decreases clauses and loop variants
  o [Alt-Ergo output] avoid empty list of arguments
  o [GWhy] added alternative "boomy" icon set
  o [Alt-Ergo+Simplify output] well_founded() translated by false
    instead of true, for soundness
  o [Jessie/Krakatoa/Frama-C plugin] support for decreases clauses,
    even for mutually recursive functions
  o [Frama-C plugin] bug fix 0284
  o [Frama-C plugin] support for "complete behaviors" and "disjoint
    behaviors" clauses. fixes bug 0026.
  o [Jessie][Frama-C] bug fix: 0103. Loops without variant are given a
      default unprovable variant.
  o [Frama-C plugin] bug fix: 0112 (partially fixes bts0039 and bts0080)
  o [Frama-C plugin] bug fix: 0306
  o [Frama-C plugin] bugs closed: 0041, 0063, 0073, 0094, 0102, 0199, 0273
  o [Jessie] Polymorphic logic types added (use < >)

version 2.21, October 15, 2009
==============================

  o [GWhy] Fixed 'Not_found' exception if .whyrc absent
  o [Frama-C plugin] Fixed installation problems.
  o [Frama-C plugin] predicates for finiteness of floats (\is_finite,
    \is_infinite, etc.) do not fail in mode JessieFloatModel(real) but
    give the expected truth value.
  o [Jessie] do not fail anymore on pointer casts over floats or reals.
    Fixes bug 273 of Frama-C BTS

version 2.20, October 2nd, 2009
===============================

  o [Jessie][Frama-C] Integration of the Jessie plugin for Frama-C
    Compatible with Frama-C release Beryllium 2 (20090902)
  o [Why][Jessie] add a new assertion check which is used like assert.
    It try to prove the assertion but do not use it as hypothesis.
  o [Why] fixed some bugs with Coq output
  o [GWhy] new column gappa+hypotheses selection

version 2.19, June 23rd, 2009
=============================

  o This version is synchronized with Frama-C Beryllium beta 1 200906xx
    (http://frama-c.cea.fr/)
  o [Jessie] support for label 'Post' in assigns clauses
  o [Jessie] support for loop_assigns clauses
  o [Why] added a let/in construct in logic (let x = term in term /
    let x = term in predicate)
  o [Krakatoa/Jessie] "reads" clauses on logic functions and
    predicates, which disappeared in version 2.16, have been
    resurected. Beware that the semantics is slightly different from
    Caduceus one: it has to precisely give the memory footprint of the
    function, and not only an under-approximation. It is use to
    automatically generate footprint axioms.
  o [GWhy] improved prover column configuration, improved config saving
    incompatibility warning: old .gwhyrc files will be ignored and overwritten
  o [Why] deprecated options -no-prelude, -no-arrays, -fp
  o [Why] new declaration [include "file"] in Why input language
  o [Why] prelude is split into smaller files: bool.why integer.why
    real.why
  o [Jessie] added several builtin functions on reals:
    \exp, \log, \cos, \sin, etc.
  o [Why] added several functions on reals in prelude:
    exp, log, cos, sin, etc. (see prelude.why)
  o [Jessie] syntax change for loops: can have behaviors with assigns clauses
  o [Why] fixed typing bug with polymorphic function symbols and comparisons
  o [GWhy] new column for Gappa prover (http://lipforge.ens-lyon.fr/www/gappa/)
  o [Coq output] improved output of -e when e is an integer constant
  o [Jessie] fix incompleteness bug with "assigns \nothing" clauses
  o [GWhy] columns can be added/removed interactively

version 2.18, January 22th, 2009
================================

  o Jessie: bug fix related to assignment to the null pointer
  o Krakatoa: several bug fixes related to constructors (class invariant
    not anymore assumed true at entrance, object fields initialized to
    their default values)
  o Krakatoa/Jessie: support for "for" sections (associated to various
    behaviors) in code annotations (assert and loop invariants).
    See e.g tests/java/BinarySearch.java
  o Caduceus: fixed 'pvs' target in generated makefile
  o Why: min and max functions in the prelude, with appropriate
    axiomatization

version 2.17, December 17th, 2008
================================

  o This version is synchronized with Frama-C Lithium 20081201
    (http://frama-c.cea.fr/)
  o why-cpulimit: specific implementation for Cygwin (contributed by
    Dillon Pariente)
  o jessie: bug fix: inductive predicates and multiple labels
  o jessie: new support for floating-point computations
  o krakatoa/jessie: bug fix: axiomatic and multiple labels
  o New prover column in GWhy for Alt-Ergo with selection of hypotheses
    (see option -select of Alt-Ergo)

version 2.16, October 29th, 2008
================================

  o This version is synchronized with Frama-C Lithium beta 1
    (http://frama-c.cea.fr/)
  o GWhy: improved display of VCs
  o Krakatoa/Jessie: changed syntax for axiomatic definitions. 'reads'
    clauses are now obsolete.
  o Krakatoa/Jessie: support for inductive definitions
  o Why: Improved support for inductive definitions. For automatic provers,
    an inversion axiom is generated.
  o New option -alt-ergo to output VCs in Alt-Ergo syntax. Beware that
    because of inductive definition, -alt-ergo is now different from
    -why output: inductive definitions are expansed.
  o License changed to GNU LGPL 2, with a special exception on
    linking (see enclosed file LICENSE)

version 2.15, September 9th, 2008
=================================

  o Why: preliminary support for inductive definitions
  o Krakatoa/Jessie: new syntax for axiomatic definitions
  o Coq support for floats requires Coq version 8.1 at least
  o Jessie bug fix: 'simplify' entry of the generated makefile was ignoring
    prelude axioms

version 2.14, July 28th, 2008
=============================
  o tools `dp' and `cpulimit' renamed into `why-dp' and `why-cpulimit'
  o krakatoa/jessie: preliminary support for statement contracts
  o krakatoa/jessie/why: new builtin logic symbols \int_max, \int_min,
    \real_max, \real_min
  o Zenon: fixed syntax for Zenon 0.5.0 (missing $hyp)
  o WP: no more duplication of VCs when operators &&, || and not are
    applied to pure boolean expressions; command line option
    -split-bool-op to revert to the old behavior
  o krakatoa: loop annotations: 'decreases' keyword replaced by 'loop_variant'
  o WP: universal quantification forall b:bool. P(b) no more turned
    into P(true) and P(false) when there is a possible size increasing
  o SMT-lib output: fixed bug with variants (when -split-user-conj
    not set); predicate zwf_zero added to prelude.why
  o SMT-lib output: fixed bug with if_then_else
  o krakatoa/jessie: support for ( ? : ) operator in terms and propositions
  o configuration: detection of Alt-ergo executable name (ergo/alt-ergo)
  o jessie/why: reorganization of PVS output
  o krakatoa/jessie: version number, and CHANGES files are now those of why
  o krakatoa/jessie: added support for bitwise operator on booleans
  o krakatoa/jessie/why/provers: better support of real numbers
  o CVC3: no more options +arith-new +quant-polarity -quant-new
  o fixed HOL4 output; contribution by Vladimir Timashov
    (vladimir.timashov@gmail.com)
  o gwhy: fixed efficiency issue with large comments
  o jessie: fixed coq entry in jessie-generated makefile
  o why typing safely fails when duplicate parameter names in
    logic definitions

version 2.13, May 27th, 2008
============================

  o krakatoa: bug fix: method lookup in class Object
  o krakatoa: if possible, avoid failure in constant expression evaluation
  o gwhy: better support of non-ascii input characters in GWhy
  o fixed parsing of float constants with exponents

version 2.12, May 23rd, 2008
============================

  o krakatoa: assigns clause now correctly typed in the post-state
  o krakatoa: array ranges in assigns clause: now correctly parse [..], [..n] and [n..]
  o krakatoa: support for model fields (in interfaces)
  o krakatoa: support for user-defined logic types
  o krakatoa: partial support for Strings
  o fixed typing bug with polymorphic logic constants/functions used
    in programs (resulted in bugs in -encoding sstrat)

version 2.11, March 17th, 2008
==============================

  o krakatoa: documentation is now is reasonable shape, although still incomplete
  o krakatoa: loop annotations: having an invariant but no decreases clause is allowed
  o krakatoa: bug fix: value axiom for logic constants
  o krakatoa: many improvements in generation of memory safety VCs
  o fixed bug with --prune-hyp

version 2.10b, January 31st, 2008
=================================

  o krakatoa: first release officially replacing version 0.67
  o CVC3: now called with options +arith-new +quant-polarity -quant-new
    (requires version 1.2.1)
  o SMT-lib output: fixed bug with reals
  o gwhy: benchmark (Ctrl-B) does not verify all functions in parallel anymore

version 2.10a, January 14th, 2008
=================================
  o configuration: fixed detection of ocamldep when ocamldep.opt is
    not installed / fixed detection of local ocamlgraph

version 2.10, December 20th, 2007
=================================
  o the Krakatoa front-end for Java programs is now distributed with Why
  o dp: new option -smt-solver to set the SMT solver (Yices, Z3, CVC3)
  o new option --fast-wp to use quadratic WP algorithm
  o localization of VC wrt source code (options --locs and --explain) and
    visualization in gwhy
  o gwhy: added prover Z3 (http://research.microsoft.com/projects/z3/)
  o SMT-lib output: integer division (/) is now translated into an
    uninterpreted function symbol div_int
  o simplify2why: fixed bugs

version 2.04, August 2nd, 2007
==============================
  o gwhy: Ctrl-B successively tries all provers on all proof obligations
  o new option -load-file to read an input file without generating
    output for the prover
  o new prover interface Graph which iteratively allows to select more
    and more hypotheses and to discharge POs in Simplify
  o new option -prune-hyp to select relevant hypotheses in the goal
  o fixed Isabelle output (contribution by Yasuhiko Minamide)

version 2.03, April 20th, 2007
==============================
  o fixed PVS output
  o gwhy: added prover CVC3 (http://www.cs.nyu.edu/acsys/cvc3/)
  o fixed bug with polymorphic exceptions (not accepted anymore)
  o fixed bug in generalization test
  o Coq output: renaming of Coq's reserved keywords

version 2.02, February 23rd, 2007
=================================
  o new tool why-stat to display statistics regarding symbols used in goals
  o new options -why and -multi-why to get verification conditions in
    Why syntax (useful when computing VCs takes much time)
  o gwhy: font size can be changed dynamically using Ctrl-+ and Ctrl--
  o WP: the invariant at loop entry does not appear anymore in the
    verification condition related to the invariant preservation
  o option -no-simplify-triggers changed to -simplify-triggers,
    defaulting to false, because Caduceus bench shows it is good in
    general, and moreover generated triggers with Krakatoa and jessie
    make Simplify fail
  o Simplify output: fixed bug with leading underscores in identifiers
  o compatibility with Coq development version (ring syntax has changed)
  o option --encoding sstrat automatically added when --smtlib or
    --cvcl is selected and no encoding specified
  o new option --exp to expand the predicate definitions
  o Coq output: the command "Implicit Arguments id" is automatically
    inserted for polymorphic symbols

version 2.01, November 29th, 2006
=================================
  o new predicate distinct(t1,t2,...,tn) with n terms of the same type
    mapped to the primitive DISTINCT in Simplify and SMTlib outputs,
    expanded for other provers
  o fixed bug in CVC Lite output (BOOLEAN now reserved for predicates;
    new type BOOL introduced for term booleans)
  o dp now displays times for searching proofs
  o no using anymore the external command 'timeout', but use our own
    command 'cpulimit' for the same purpose. Time limit is now user
    CPU time instead of wall clock time.
  o fixed bugs in smtlib output: all variables are "?" prefixed,
    brackets around constants are removed,
    validity question is turned into a sat question,
    Boolean sort with Boolean_false and  Boolean_true constants
    are introduced,
    Unit sort is introduced
  o fixed bugs into the harvey (rv-fol) output (principally the
    command lines)
  o triggers added to axioms of the caduceus model

version 2.00, June 12th, 2006
=============================
  o quantifiers triggers can be given with the following syntax
       forall x,y:int [f(x),g(y) | h(x,y)]. p(x,y)
    currently, the triggers are only meaningful for the Simplify prover
  o new encodings of Why logic into first-order monosorted logic for
    untyped provers (like Simplify or Zenon) : there are three
    possible encodings that can be selected through the command
    line --encoding option
  o better naming of type variables in Coq output (A1, A2,
    etc. instead of A718, etc.)
  o fixed bugs with polymorphic logic constants used in programs
  o a missing function postcondition is now given the default value
    "true" (and a warning is emitted for local functions)
  o Zenon output (--zenon option); see focal.inria.fr/zenon
  o new option --split-user-conj to split user conjunctions in goals
    (resulting in more numerous proof obligations)
  o Mizar output updated for Mizar 7.6.01
  o new behavior w.r.t. termination proofs: variants can be omitted in
    loops and recursive functions; new command line options --partial
    and --total to specify respectively partial correctness
    (i.e. variants are not considered even when present) or total
    correctness (i.e. variants are mandatory)
  o fixed bug with polymorphic parameters that should not be generalized
  o new construct "e {{ Q }}" (opaque sub-expression)
  o new construct "assert {P}; e"
  o any logic term can be used in programs
  o types must be declared (new declaration "type foo")
  o fixed bug with missing exceptional postconditions (false in now
    inserted and a warning is emitted)
  o array types now accepted in logic/predicate arguments
  o --coq now selects the Coq version determined at compiled time

version 1.82, September 1st, 2005
=================================
  o fixed variable capture issue in haRVey output
  o fixed bugs in Isabelle output (Yasuhiko Minamide)
  o support for declaration "function" with Isabelle/CVC/harvey/PVS
  o new declaration "goal" to declare a proof obligation
    e.g. goal foo : forall x:int. x = x+0

version 1.81, June 20th, 2005
=============================
  o support for CVC Lite syntax 2.0.0, old syntax not supported anymore
  o support for haRVey 0.5.6
  o a predicate label can be a string (e.g. :"bla bla":pred)
  o a missing exceptional postcondition is now given the default value "false"
    instead of "true" (i.e. the corresponding exception cannot be raised)
  o new declaration "function" to define a logic function
    e.g. function f(x:int, y:int) : int = x+y

version 1.80, June 3rd, 2005
============================
  o Isabelle/HOL output (--isabelle option) contribution by Yasuhiko Minamide
  o HOL 4 output (--hol4 option) contribution by Seungkeol Choe
  o SMT-LIB format output (--smtlib option)

version 1.75, March 15th, 2005
==============================
  o fixed installation issue with Coq 8.0pl2
  o new option -where to print Why's library path

version 1.71, February 3rd, 2005
================================
  o Simplify output: axioms are also printed with universal
    quantifiers moved inside as much as possible (forall x y, P x =>
    Q x y becomes forall x, P x => forall y, Q x y)

version 1.69, January 4th, 2005
===============================
  o labeled predicates with syntax ":id: predicate" and lowest precedence

version 1.64, October 13th, 2004
================================
  o Coq output now in V8 syntax when Coq V8 is detected at configuration

version 1.63, August 26th, 2004
===============================
  o WP completely redesigned: side-effects free expressions are now
    given an adequate specification, so that the WP calculus does not
    enter them. It results in significantly simpler proof obligations.
  o new tool `dp' to call decision procedures Simplify and CVC Lite
    (calls the DP once for each goal with a timeout and displays stats)
  o CVC Lite output (option --cvcl; see http://chicory.stanford.edu/CVCL/)
  o Coq: parameters no more generated when -valid is not set
  o PVS: support for Why polymorphic symbols and/or axioms

version 1.62, June 24th, 2004
=============================
  o new option --all-vc to get all verification conditions (no more
    automatic discharging of the most trivial conditions)

version 1.61, May 27th, 2004
============================
  o Simplify output: do not fail on floats anymore (now uninterpreted symbols)
  o added primitive int_of_real: real -> int (in both logic and programs)

version 1.60, May 18th, 2004
============================
  o fixed WP for while loops (may break Coq proofs)
  o new connective <->

version 1.55, May 3rd, 2004
===========================
  o type `float' is renamed into `real'
  o absurd and raise now polymorphic

version 1.51, April 6th, 2004
=============================
  o Simplify typing constraints only with --simplify-typing option
  o fixed bug in automatic annotation of x := e when e has a postcondition

version 1.50, March 26th, 2004
==============================
  o first release of Caduceus
  o added ``typing'' contraints in Simplify output (using predicates ISxxx)
  o new declaration "predicate" to define a predicate
  o new option --dir to output files into a given directory

version 1.42, March 16th, 2004
==============================
  o new option --pvs-preamble
  o change in syntax: "external" is now a modifier for "parameter" and
    "logic" (see the manual for explainations); to be conservative,
    the following substitutions have to be made:
       "external" -> "external parameter"
       "logic"    -> "external logic"
  o new command "axiom <ident> : <predicate>" to declare an axiom

version 1.40, December 19th, 2003
================================
  o disabled C support: C is now supported by an external tool, Caduceus
    (to be released soon with Why)
  o support for polymorphism (contribution by C. March)
  o syntax of haRVey output now uses integer constants, predefined
    arithmetic operators, and does not change capitalization of
    variables, to be conform with the syntax of the next version of
    haRVey (presumably 0.4)
    Also added option --no-harvey-prelude

version 1.32
============
  o output for Coq version 8 with --coq-v8
    (--coq is now equivalent to --coq-v7, and is still the default output)
    examples in V7 syntax now in examples-v7/ and in V8 syntax in examples/
  o Mizar output (with option --mizar)
    Mizar article in lib/mizar/why.miz (installed by "make install")

version 1.3, September 17th, 2003
=================================
  o new tool why2html to convert Why input files to HTML
  o Simplify output (with option --simplify)
  o fixed bug with WP of constants false/true (simplification added)
  o better automatic annotation of tests (in particular || and && are given
    postconditions whenever possible)

version 1.22, June 21th, 2003
=============================
  o fixed lost of annotation in C function calls
  o C: /*W external/parameter ...*/ correctly added to C environment
  o Coq: added Hints Unfold Zwf
  o (almost) conservative change in renaming strategy; a reference x1 is now
    renamed into x1 x1_0 x1_1 etc. instead of x1 x2 x3 etc.

version 1.2, May 12th, 2003
===========================
  o true used as default postcondition for exceptions instead of false
    (necessary for a correct translation of C programs)
  o C: fixed bug in translation from ints to booleans
  o better names given to local references in proof obligations
  o improved automatic proof (both completeness and performance)

version 1.10, April 4th, 2003
==============================
  o C: added label statement and alternate syntax /*@ label id */
  o fixed bug in ocaml code generation

version 1.08, March 28th, 2003
==============================
  o C: local variables can be uninitialized
  o examples: C programs for exact string matching (in string-matching)
  o fixed bug in WP (not collecting some intermediate assertions)
  o C: added statement /*@ assert p */
  o new construct "absurd" to denote unreachable code

version 1.07, March 25th, 2003
==============================
  o arbitrary side-effects now allowed in tests (if / while)
  o label "init" suppressed; new syntax label:expression to insert labels
  o syntax: logic may introduce several identifiers in a single declaration
  o linear proof search restricted to WP obligations
  o PVS: change in array type (warray) to get better TCCs
  o fixed ocaml output (array_length)

version 1.04, March 5th, 2003
=============================
  o C: logic declarations with syntax /*W ... */
  o improved automatic proof (thus less obligations)
  o validation in a separate file f_valid.v

version 1.02, February 7th, 2003
================================
  o PVS: fixed integer division and modulo, fixed output
  o haRVey: no more restriction to first-order obligations
  o Coq: the validation is now given a type
  o distinction between preconditions and obligations

version 1.0, January 31st, 2003
================================
  o syntax: pre- and postconditions brackets now come by pairs (but,
    inside, the predicates may be omitted)
  o fixed WP bug in a sequence of calls with before-after annotations
  o no more "pvs" declaration (the user can now edit the _why.pvs file)
  o fixed bug in type-checking of recursive functions with exceptions
  o fixed bug in loop tests automatic annotation;
    now a warning when a loop test cannot be given a postcondition
  o fixed bug in interpretation of @init
  o doc: C programs, Coq and PVS libraries documented
  o logic: if-then-else construct on terms
  o PVS: arrays defined in Why prelude and fixed pretty-print; installation

version 0.92, January 13th, 2003
================================
  o C: fixed bug in array/reference passing
  o fixed check for exceptions in external declarations
  o HOL Light output (with option --hol-light)
  o fixed compatibility with Coq 7.3
  o C: recursive functions, arrays, pointers

version 0.8, December 6th, 2002
===============================
  o haRVey output (option --harvey; see http://www.loria.fr/~ranise/haRVey/)
  o C input (incomplete: no arrays, no pointers, no recursive functions)
  o Coq: helper tactics (AccessSame, AccessOther, ...)
  o fixed bug in application typing
  o major change:
    arrays do not have a dependent type anymore; array_length introduced
  o Emacs mode for editing Why ML source (in lib/emacs)
  o automatic discharge of ...|-(well_founded (Zwf 0))
    and of ...,v=t,...,I and (Zwf 0 t' t),...|-(Zwf 0 t' v)
  o fixed bug in local recursive functions

version 0.72, November 12th, 2002
=================================
  o caml code generation with option --ocaml (beta test)
    (customized with --ocaml-annot, --ocaml-ext, --output)
  o quantifier "exists" added to the logic syntax
  o manual: added lexical conventions
  o examples: added maximum sort (by Sylvain Boulm)
  o new feature: exceptions (beta test)

version 0.71, October 15th, 2002 (bug fix release)
================================
  o better WP for the if-then-else (when the test is annotated)
  o reference masking now forbidden
  o fixed bug in automatic annotations => some postconditions names may change
  o fixed Coq 7.3 compatibility module

version 0.7, October 2nd, 2002
==============================
  o Why library compatible with Coq 7.3 (released version) and with Coq
    development version (determined at configuration)
  o code ported to ocaml 3.06
  o examples: quicksort (2 versions)
  o more obligations automatically discharged
    (True  /  A and B |- A  /  A,B |- A and B)
  o Coq: fixed associativity in pretty-print for /\ and \/ (right)
    right associativity adopted in Why
  o fixed typing and Coq output for primitive float_of_int

version 0.6, July 19th, 2002
============================
  o examples: find
  o doc: predefined functions and predicates
  o floats: predefined functions and predicates, Coq pretty-print
  o fixed bug: x@ reference in a loop post-condition incorrectly translated
  o the variant relation is now necessarily an identifier
  o terms and predicates are now typed; new declaration "logic"
    (terms and predicates syntax are mixed; fixes a parsing bug)

version 0.5,  July 2nd, 2002
============================
  o first (beta) release

Local Variables:
mode: text
End: