<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />

version 2.04, August 2nd, 2007
==============================
  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: