Home My Page Projects Why3
Summary Activity Tracker Lists SCM Files

Project Filelist for Why3

File Release Notes and Changelog

Release Name: 0.87.0

Change Log
Version 0.87.0, March 15, 2016
================================

Language
  * Add new logical connectives "by" and "so" as keywords

Tools
  o add a command-line option --extra-expl-prefix to specify
    additional possible prefixes for VC explanations.  (Available for
    why3 commands "prove" and "ide".)
  * removed "jstree" style from the "session" command

Transformations
  * All split transformations respect the "stop_split" label now.
    split_*_wp is a synonym for split_*_right
  * split_*_right split the left-hand side subformulas
    when they carry the "case_split" label
  * split_intro is now the composition of split_goal_right and
    introduce_premises

Library
  * improved bitvector theories

API
  * Renamed functions in Split_goal
  * split_intro moved to Introduction

Encodings
  * When a task has no polymorphic object (except for the special
    cases of equality and maps) then the translation to SMT-LIB
    format is direct

Provers
  * discarded support for Alt-Ergo versions older than 0.95.2
  o support for Alt-Ergo 1.01 (released Feb 16, 2016) and
    non-free versions 1.10 and 1.20
  o support for Coq 8.4pl6 (released Apr 9, 2015)
  o support for Coq 8.5 (released Jan 21, 2016)
  o support for Gappa 1.2.0 (released May 19, 2015)
  * discarded support for Isabelle 2014
  o support for Isabelle 2015 (released May 25, 2015) and
    Isabelle 2016 (released Feb 17, 2016)
  o support for Z3 4.4.0 (released Apr 29, 2015) and
    4.4.1 (released Oct 5, 2015)
  o support for Zenon 0.8.0 (released Oct 21, 2014)
  o support for Zenon_modulo 0.4.1 (released Jul 2, 2015)

Distribution
  * non-free files have been removed: "boomy" icon set,
    javascript helpers for "why3 session html --style jstree"