<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 0.66, March 15th, 2005
==============================
  o support for Coq 8.0pl2 and Why 1.75

version 0.65, October 18th, 2004
================================
  o fixed bug with regeneration of local_memory_why.v
  o entry 'regenerate' in generated makefiles
  o support for Why 1.64 and 1.65 (older versions not recommanded)
  o support for try .. catch statements
  o fixed bug: boolean declarations were not allowed in specifications
  o added support for invariants in interfaces, bug correction on
    final constants in interfaces 
  o modifiable clause now defaults to \everything instead of \nothing 

version 0.64, May 3rd, 2004
==============================
  o fixed bugs with abrupt returns
  o decreases clause is not mandatory in loop annotations

version 0.63, March 25th, 2004
==============================
  o fixes a compilation problem on installation

version 0.62, March 16th, 2004
==============================
  o support for i386/MSWindows architecture
  o added support for floats/doubles, requires Why 1.41 at least
  o added output for the PVS prover, using option -pvs
  o adapted to Why syntax version post-1.40

version 0.60, December 20th, 2003
==============================
  o coq output is now in V8 syntax
  o corrected bug in naming of why functions, which prevented Krak
    validations to check correctly
  o added output for the haRVey prover, using option -harvey
  o local memory is now the default option, use -globalmemorymodel to
    get the older modeling
  o added output for the Simplify prover, using option -simplify
  o Java semantics bug correction: t.length now requires t non null
  o support for JML \fresh predicate
  o option -coqdir to pass additional input dir to coqc
  o option -coqopt to pass any option to coqc
  o support extended (i.e. unofficial) JML constructs: assignable
    clauses for loops; and behavior specification for arbitrary statement,
    with requires, assignable, ensures and signals clauses
  o better handling of memory allocations, making proof obligations
    simpler. 

version 0.55, June 16th, 2003
==============================
  o bug corrections only

version 0.54, May 14th, 2003
==============================
  o exchange names of lemmas mod_access and mod_access_rev, so that
    the one which is use often has the short name.
  o translation of constructors now includes the allocation
    at the beginning. Proofs are significantly simpler. 
  o 'is_value_cell' renamed to the more natural 'is_valid_cell'
  o if Krakatoa detects that a method cannot throw any exception,
    but its JML specification allow a signal, a warning is issued.
    on the other hand, if Krakatoa detects that a method may throw
    some exception, but its JML specification does not allow any
    signal, no warning is issued but krakatoa silently adds the
    post-condition 
      Exception => false 
    to the why program generated.
  o a "final" validation is done by Krakatoa: the file
    Krak_validations.v should compile without errors.
  o validations are generated by default. use -novalid option
    to disable them.

version 0.53, March 12th, 2003
==============================
  o pure boolean methods whose specification has the form 
      \result <==> e
    are translated as propositions, not boolean expressions.
  o overloaded constructors are numbered by distinct numbers
  o why validations are put in separate files. This requires Why
    version 1.02 at least. warning: it is not check anymore that a
    validation m_ext has the same type as its corresponding spec m,
    that may happen because of effects.
  o generated files are all put in directory specified by -p

version 0.4, February 5th, 2003
===============================
  o non-released version, base version for CHANGES file
  o the new release 7.4 of Coq is required

Local Variables: 
mode: text
End: