Commit 3dd84985 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge branch 'master' into counter-examples

parents 54579859 28b7a239
/examples/in_progress/ export-ignore
/examples/hoare_logic/draft/ export-ignore
/tests/ export-ignore
/bench/encoding/ export-ignore
/misc/ export-ignore
/ROADMAP export-ignore
/DEVELOPER.readme export-ignore
/opam/ export-ignore
.gitignore export-ignore
.gitattributes export-ignore
/check.sh export-ignore
/TODO export-ignore
......@@ -18,6 +18,7 @@ why3.conf
*.vo
*.vd
*.glob
.*.aux
*.elc
*.summary
\#*\#
......@@ -28,6 +29,7 @@ why3.conf
/autom4te.cache
/Makefile
/configure
/install-sh
/semantic.cache
/TAGS
/output_why3
......@@ -120,8 +122,10 @@ why3.conf
/doc/stdlibdoc/
# /lib
/lib/why3-cpulimit
/lib/why3-cpulimit.exe
/lib/why3cpulimit
/lib/why3cpulimit.exe
/lib/why3server
/lib/why3server.exe
# /lib/why3/
/lib/why3/META
......@@ -143,6 +147,9 @@ why3.conf
/src/coq-tactic/why3tac.ml
/src/coq-tactic/.why3-vo-*
# Coq
/lib/coq/bv/BV_Gen.v
# PVS
.pvscontext
orphaned-proofs.prf
......@@ -157,8 +164,7 @@ pvsbin/
/lib/isabelle/map/
/lib/isabelle/real/
/lib/isabelle/set/
/lib/isabelle/Tools/why3
/lib/isabelle/Why3_Number.thy
/lib/isabelle/Why3_BV.thy
/lib/isabelle/why3.ML
/lib/isabelle/last_build
/lib/isabelle/bv
......@@ -275,14 +281,19 @@ pvsbin/
/modules/mach/int/
# Try Why3
/src/trywhy3/trywhy3.js
/src/trywhy3/trywhy3.byte
/src/trywhy3/trywhy3.js
/src/trywhy3/alt_ergo_worker.byte
/src/trywhy3/alt_ergo_worker.js
/src/trywhy3/why3_worker.byte
/src/trywhy3/why3_worker.js
/src/trywhy3/index.en.html
/src/trywhy3/index.fr.html
/src/trywhy3/index.html
/src/trywhy3/ace-builds
/src/trywhy3/ace-builds/
/src/trywhy3/*.png
/src/trywhy3/alt-ergo-1.00-private-2015-01-29
/src/trywhy3/fontawesome/
# jessie3
/src/jessie/config.log
......@@ -293,3 +304,4 @@ pvsbin/
/src/jessie/tests/demo/result/*.log
/trash
trywhy3.tar.gz
François Bobot <francois@bobot.eu> <bobot@lri.fr>
François Bobot <francois@bobot.eu> <francois.bobot@cea.fr>
Martin Clochard <martin.clochard@lri.fr> <martin@pc-stagiaire.(none)>
Martin Clochard <martin.clochard@lri.fr> <clochard@MC-MacBook.(none)>
Sylvain Dailler <dailler@adacore.com> <sdailler@hauzar@adacore.com>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <Jean-Christophe.Filliatre@lri.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <filliatr@lri.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jc@evariste.(none)>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jc@gemini.(none)>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <filliatr@balrog.(none)>
Clément Fumex <clement.fumex@inria.fr> <fumex@moloch.lri.fr>
Léon Gondelman <gondelmans@lri.fr> <gondelmans@lri.fr>
Léon Gondelman <gondelmans@lri.fr> <lgondelmann@gmail.com>
Léon Gondelman <gondelmans@lri.fr> <lgondelman@lg-PC.(none)>
Léon Gondelman <gondelmans@lri.fr> <leon@ubuntu.(none)>
David Hauzar <david.hauzar@inria.fr> <hauzar@moloch.lri.fr>
Johannes Kanig <kanig@adacore.com> <johannes.kanig@lri.fr>
Claude Marché <claude.marche@inria.fr> <Claude.Marche@inria.fr>
Claude Marché <claude.marche@inria.fr> <cmarche@dispater.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@orcus.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@belzebuth.(none)>
Guillaume Melquiond <guillaume.melquiond@inria.fr> <melquion@moloch.saclay.inria.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@acces.lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyenthiminhtuyen@minhtuyen.local>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <thi-minh-tuyen.nguyen@inria.fr>
Andrei Paskevich <andrei@lri.fr> <andrei@tertium.org>
Mário José Parreira Pereira <mpereira@lri.fr> <mario.j.p.pereira@gmail.com>
Mário José Parreira Pereira <mpereira@lri.fr> <parreira@lri.fr>
Mário José Parreira Pereira <mpereira@lri.fr> <mpereira@lri.fr>
Asma Tafat-Bouzid <atafat@lri.fr> <atafat@lri.fr>
Asma Tafat-Bouzid <atafat@lri.fr> <atafat@atafat-desktop.(none)>
Piotr Trojanek <piotr.trojanek@altran.com> <piotr.trojanek@gmail.com>
* marks an incompatible change
Tools
* add a command-line option --extra-expl-prefix to specify
o why3 config now generates default proof strategies using the
installed provers. These are available under name "Auto level 1"
and "Auto level 2" in why3 ide.
Version 0.87.1, May 27, 2016
============================
bug fixes
o assorted bug fixes
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 bitvectors theories
* 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
......@@ -15,14 +47,34 @@ Encodings
format is direct
Provers
o discarded support for Alt-Ergo versions older than 0.95.2
* 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)
o support for Isabelle 2015 (released May 25, 2015)
o support for Z3 4.4.0 (released Apr 29, 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"
Version 0.86.3, February 8, 2016
================================
bug fixes
o assorted bug fixes
provers
o fix compilation issues with Coq 8.5
(the tactic for 8.5 now behaves like idtac on successfully proved goals)
Version 0.86.2, October 13, 2015
================================
......@@ -42,7 +94,7 @@ provers
bug fixes
o why3doc: garbled output
version 0.86, May 11, 2015
Version 0.86, May 11, 2015
==========================
core
......@@ -84,7 +136,7 @@ bug fixes
o IDE: proofs in progress should never be "cleaned"
o IDE: display warnings after reload
version 0.85, September 17, 2014
Version 0.85, September 17, 2014
================================
langage
......@@ -114,7 +166,7 @@ transformations
provers
o fixed wrong warning when detecting Isabelle2014
version 0.84, September 1, 2014
Version 0.84, September 1, 2014
===============================
tools
......@@ -156,7 +208,7 @@ transformations
o new transformation "compute_in_goal" that simplifies the goal, by
computation, as much as possible
version 0.83, March 14, 2014
Version 0.83, March 14, 2014
============================
syntax
......@@ -196,7 +248,7 @@ API
miscellaneous
o fixed compilation bug with lablgtk 2.18
version 0.82, December 12, 2013
Version 0.82, December 12, 2013
===============================
o lemma functions
......@@ -236,7 +288,7 @@ version 0.82, December 12, 2013
o [fix] syntax highlighting bugs: should be fixed by removing the old language
file alt-ergo.lang from alt-ergo distribution
version 0.81, March 25, 2013
Version 0.81, March 25, 2013
============================
o [prover] experimental support for SPASS >= 3.8 (with types)
......@@ -259,8 +311,9 @@ version 0.81, March 25, 2013
is not accepted anymore.
version 0.80, Oct 31, 2012
==========================
Version 0.80, October 31, 2012
==============================
* [whyml] modified syntax for mlw programs; a summary of changes is
given in Appendix A of the manual
o [whyml] support for type invariants and ghost code
......@@ -284,8 +337,9 @@ version 0.80, Oct 31, 2012
* [config] modifiers in --extra-config are now called [prover_modifier]
instead of just [prover]
version 0.73, Jul 19, 2012
==========================
Version 0.73, July 19, 2012
===========================
o [IDE] "Clean" was cleaning too much
* no more executable why3ml (why3 now handles WhyML files)
o [Provers] support for Z3 4.0
......@@ -303,8 +357,9 @@ version 0.73, Jul 19, 2012
o new option -e for "why3session latex" allows to specify when to
split tables in parts
version 0.72, May 11, 2012
Version 0.72, May 11, 2012
==========================
o [Coq] new tactic "why3" to call external provers as oracles
o [Coq output] new feature: theory realizations (see manual, chapter 9)
o new tool why3session (see manual, section 6.7)
......@@ -329,7 +384,7 @@ version 0.72, May 11, 2012
a single abstract function/predicate symbol and Dlogic for
a list of (mutually recursive) defined symbols.
version 0.71, October 13, 2011
Version 0.71, October 13, 2011
==============================
o [examples] a lot of new program examples in directory examples/programs
......@@ -344,7 +399,7 @@ version 0.71, October 13, 2011
marked obsolete if it was made by a prover with another version
than the current.
version 0.70, July 6, 2011
Version 0.70, July 6, 2011
==========================
New features
......@@ -386,8 +441,8 @@ version 0.70, July 6, 2011
So old code performing "prove_task t () ()" should be translated to
"wait_on_call (prove_task t ()) ()".
version 0.64, Feb 16, 2011
==========================
Version 0.64, February 16, 2011
===============================
o configure: if possible, use ocamlfind to find lablgtk2 and sqlite3
o algebraic types: must be well-founded, non-positive constructors
......@@ -417,12 +472,7 @@ version 0.64, Feb 16, 2011
repositories)
o better Gappa output: support for sqrt, for negative constants
version 0.63, Dec 21, 2010
==========================
Version 0.63, December 21, 2010
===============================
o first public release. See release notes in manual
# Emacs parameters
Local Variables:
mode: text
End:
......@@ -23,9 +23,10 @@ Installation from the git repository
First run
autoconf
automake --add-missing
to build the file ./configure, then follow instructions from the
section above.
to build the ./configure file and install the helper scripts, then follow
instructions from the section above.
Detailed instructions
......
This diff is collapsed.
This diff is collapsed.
# Why version
VERSION=0.86+git
VERSION=0.87+git
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 5.
Ltac z3 := why3 "z3" timelimit 5.
Inductive Why3Unhabited : Prop := .
Axiom letUsTrustWhy3 : Why3Unhabited.
Ltac ae := why3 "alt-ergo" timelimit 5 ; case letUsTrustWhy3.
Ltac z3 := why3 "z3" timelimit 5; case letUsTrustWhy3.
Require Export ZArith.
Open Scope Z_scope.
......@@ -52,9 +56,8 @@ with p : nat -> Prop :=
| cc : p O.
Goal p O.
(* not a first order goal
ae.
*)
(* not a first order goal *)
try ae.
exact cc.
Qed.
......@@ -64,9 +67,8 @@ with bar : nat -> Prop :=
d : forall f:nat->nat, bar (f O).
Goal fooo O.
(* Don't know
ae.
*)
(* Don't know *)
try ae.
exact (c (d (fun x => O))).
Qed.
......@@ -84,9 +86,8 @@ Qed.
Parameter f : (nat -> nat) -> nat.
Goal f (plus O) = f (plus O).
(* not a first order goal
ae.
*)
(* not a first order goal *)
try ae.
trivial.
Qed.
......@@ -324,14 +325,5 @@ Require Import Rfunctions.
Require Import Rbasic_fun.
Goal forall (x:R), (0 <= x * x)%R.
(* don't know
ae
*)
(* timeout
z3.
*)
(* timeout
why3 "cvc3" timelimit 3.
*)
intros.
Admitted.
ae.
Qed.
module M
type t = { ghost a : bool; b : int; c : int }
let bad (z : t) : int
ensures { result = if z.a then z.b else z.c }
= match z with
| { a = True; b = x } | { a = False; c = x } -> x
end
end
####################################################################
# #
# The Why3 Verification Platform / The Why3 Development Team #
# Copyright 2010-2015 -- INRIA - CNRS - Paris-Sud University #
# Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University #
# #
# This software is distributed under the terms of the GNU Lesser #
# General Public License version 2.1, with the special exception #
......@@ -127,6 +127,12 @@ AC_ARG_ENABLE(profiling,
AS_HELP_STRING([--enable-profiling], [enable profiling]),,
enable_profiling=no)
# Emacs compilation
AC_ARG_ENABLE(emacs-compilation,
AS_HELP_STRING([--disable-emacs-compilation], [do not compile why3.elc]),,
enable_emacs_compilation=yes)
# either relocation or local, not both
if test "$enable_relocation" = yes ; then
if test "$enable_local" = yes ; then
......@@ -140,23 +146,22 @@ AC_MSG_CHECKING(executable suffix)
if uname -s | grep -q CYGWIN ; then
EXE=.exe
STRIP='echo "no strip "'
CPULIMIT=cpulimit-win
AC_MSG_RESULT(.exe <Cygwin>)
else
if uname -s | grep -q MINGW ; then
EXE=.exe
STRIP=strip
CPULIMIT=cpulimit-win
AC_MSG_RESULT(.exe <MinGW>)
else
EXE=
STRIP=strip
CPULIMIT=cpulimit
AC_MSG_RESULT(<none>)
fi
fi
AC_PROG_CC()
AC_PROG_CC
AC_PROG_MKDIR_P
AC_PROG_INSTALL
# Check for Ocaml compilers
......@@ -349,7 +354,13 @@ if test "$enable_html_doc" = yes ; then
fi
# checking for emacs
AC_CHECK_PROG(EMACS,emacs,emacs,no)
if test "$enable_emacs_compilation" = yes ; then
AC_CHECK_PROG(EMACS,emacs,emacs,no)
if test "$EMACS" = no ; then
enable_emacs_compilation=no
AC_MSG_WARN([Cannot find emacs, compilation of why3.elc disabled.])
fi
fi
# checking for Zarith
if test "$enable_zarith" = yes; then
......@@ -618,21 +629,21 @@ else
ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
case $ISABELLEDETECTEDVERSION in
2014*)
2015*)
enable_isabelle_support=yes
ISABELLEVERSION=2014
ISABELLEVERSION=2015
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
2015*)
2016*)
enable_isabelle_support=yes
ISABELLEVERSION=2015
ISABELLEVERSION=2016
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
*)
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle 2014 or 2015; Isabelle discarded)
reason_isabelle_support=" (need version >= 2014)"
AC_MSG_WARN(You need Isabelle 2015 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2015)"
;;
esac
fi
......@@ -709,17 +720,13 @@ dnl AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince)
VERSION=$PACKAGE_VERSION
BUILDDATE="$(date)"
# substitutions to perform
AC_SUBST(VERSION)
AC_SUBST(BUILDDATE)
AC_SUBST(enable_verbose_make)
AC_SUBST(EXE)
AC_SUBST(STRIP)
AC_SUBST(CPULIMIT)
AC_SUBST(OCAMLC)
AC_SUBST(OCAMLOPT)
......@@ -791,6 +798,8 @@ AC_SUBST(enable_html_doc)
AC_SUBST(RUBBER)
AC_SUBST(HEVEA)
AC_SUBST(HACHA)
AC_SUBST(enable_emacs_compilation)
AC_SUBST(EMACS)
AC_SUBST(enable_frama_c)
......
......@@ -15,7 +15,7 @@ generated parts or adding empty lines inside them.
will be lost when the file is regenerated by \why. This part ends
at the first empty line.
\item Abstract logic symbols are assumed with the vernacular directive
\verb+Paramater+. Axioms are assumed with the \verb+Axiom+
\verb+Parameter+. Axioms are assumed with the \verb+Axiom+
directive. When regenerating a script, \why assumes that all such
symbols have been generated by a previous run. As a consequence,
the user should not introduce new symbols with these two
......
......@@ -6,6 +6,8 @@
| formula "&&" formula ; asymmetric conj.
| formula "\/" formula ; disjunction
| formula "||" formula ; asymmetric disj.
| formula "by" formula ; proof indication
| formula "so" formula ; consequence indication
| "not" formula ; negation
| lqualid ; symbol
| prefix-op term ;
......
......@@ -7,13 +7,13 @@ When using Isabelle from \why, files generated from \why theories and
goals are stored in a dedicated XML format. Those files should not be
edited. Instead, the proofs must be completed in a file with the same
name and extension \texttt{.thy}. This is the file that is opened when
using ``Edit'' action in \texttt{why3ide}.
using ``Edit'' action in \texttt{why3 ide}.
\subsection{Installation}
You need version Isabelle2014 or Isabelle2015. Former versions are not
supported. We assume below that your version is 2015, please replace
2015 by 2014 otherwise.
You need version Isabelle2015 or Isabelle2016. Former versions are not
supported. We assume below that your version is 2016, please replace
2016 by 2015 otherwise.
Isabelle must be installed before compiling \why. After compilation
and installation of \why, you must manually add the path
......@@ -22,7 +22,7 @@ and installation of \why, you must manually add the path
\end{verbatim}
into either the user file
\begin{verbatim}
.isabelle/Isabelle2015/etc/components
.isabelle/Isabelle2016/etc/components
\end{verbatim}
or the system-wide file
\begin{verbatim}
......@@ -33,15 +33,15 @@ or the system-wide file
The most convenient way to call Isabelle for discharging a \why goal
is to start the Isabelle/jedit interface in server mode. In this mode,
one must start the server once, before launching \texttt{why3ide},
one must start the server once, before launching \texttt{why3 ide},
using
\begin{verbatim}
isabelle why3_jedit
\end{verbatim}
Then, inside a \texttt{why3ide} session, any use of ``Edit'' will
Then, inside a \texttt{why3 ide} session, any use of ``Edit'' will
transfer the file to the already opened instance of jEdit. When the
proof is completed, the user must send back the edited proof to
\texttt{why3ide} by closing the opened buffer, typically by hitting
\texttt{why3 ide} by closing the opened buffer, typically by hitting
\texttt{Ctrl-w}.
\subsection{Realizations}
......
......@@ -42,8 +42,12 @@
%%% listings for Why3 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\RequirePackage{listings}
\RequirePackage{amssymb}
% cannot use \usepackage here because it breaks hevea (no colored keywords anymore :-()
\input{../share/latex/why3lang.sty}
% \RequirePackage{listings}
% \RequirePackage{amssymb}
\lstset{
basicstyle={\ttfamily},
......@@ -56,39 +60,6 @@
showstringspaces=false,
}
\lstdefinelanguage{why3}
{
morekeywords={namespace,predicate,function,inductive,type,use,clone,%
import,export,theory,module,end,in,with,%
let,rec,for,to,do,done,match,if,then,else,while,try,invariant,variant,%
absurd,raise,assert,exception,private,abstract,mutable,ghost,%
downto,raises,writes,reads,requires,ensures,returns,val,model,%
goal,axiom,lemma,forall,meta},%
string=[b]",%
sensitive=true,%