Commit 7857d36c authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'master' into itp

parents d08458c4 600a962a
...@@ -170,11 +170,10 @@ pvsbin/ ...@@ -170,11 +170,10 @@ pvsbin/
/lib/isabelle/map/ /lib/isabelle/map/
/lib/isabelle/real/ /lib/isabelle/real/
/lib/isabelle/set/ /lib/isabelle/set/
/lib/isabelle/Why3_Bool.thy /lib/isabelle/ROOT
/lib/isabelle/Why3_BV.thy /lib/isabelle/Why3_BV.thy
/lib/isabelle/Why3_Int.thy
/lib/isabelle/Why3_List.thy
/lib/isabelle/Why3_Number.thy /lib/isabelle/Why3_Number.thy
/lib/isabelle/Why3_Real.thy
/lib/isabelle/Why3_Set.thy /lib/isabelle/Why3_Set.thy
/lib/isabelle/why3.ML /lib/isabelle/why3.ML
/lib/isabelle/last_build /lib/isabelle/last_build
......
...@@ -20,6 +20,7 @@ Claude Marché <claude.marche@inria.fr> <cmarche@dispater.(none)> ...@@ -20,6 +20,7 @@ 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@orcus.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@belzebuth.(none)> Claude Marché <claude.marche@inria.fr> <cmarche@belzebuth.(none)>
Guillaume Melquiond <guillaume.melquiond@inria.fr> <melquion@moloch.saclay.inria.fr> Guillaume Melquiond <guillaume.melquiond@inria.fr> <melquion@moloch.saclay.inria.fr>
Kim Nguyễn <kim.nguyen@lri.fr> <kn@lri.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@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> <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> <nguyenthiminhtuyen@minhtuyen.local>
......
* marks an incompatible change * marks an incompatible change
Version 0.88.0, October 6, 2017
===============================
Language
o two new forms of type declarations: integer range types and
floating-point types. To denote constants in such types, integer
constants and real constants can be cast to such types. This
support is exploited in drivers for provers that support bitvector
theories (CVC4, Z3) and floating-point theory (Z3).
More details in the manual, section 7.2.4 "Theories".
* a quote character (') inside an identifier must either be at the
end, or be followed by either a digit, the underscore character
(_) or another quote. Identifiers with a quote followed by a
letter are reserved.
Standard library
o new theory ieee_float formalizing floating-point arithmetic,
compliant to IEEE-754, mapped to SMT-LIB FP theory.
User features
o proof strategies: why3 config now generates default proof strategies
using the installed provers. These are available under name "Auto
level 0", "Auto level 1" and "Auto level 2" in why3 ide.
More details in the manual, section 10.6 "Proof Strategies".
o counterexamples: better support for array values, support for
floating-point values, support for Z3 in addition to CVC4.
More details in the manual, section 6.3.5 "Displaying Counterexamples".
Provers Provers
0 support for Coq 8.6.1 (released Jul 25, 2017) o support for Isabelle 2017
* discarded support for Isabelle 2016 (2016-1 still supported)
o support for Coq 8.6.1 (released Jul 25, 2017)
o tentative support for Coq 8.7
* discarded tactic support for Coq 8.4 (proofs still supported)
o support for CVC4 1.5 (released Jul 10, 2017) o support for CVC4 1.5 (released Jul 10, 2017)
o support for E 2.0 (released Jul 4, 2017) o support for E 2.0 (released Jul 4, 2017)
o support for E 1.9.1 (release Aug 31, 2016) o support for E 1.9.1 (release Aug 31, 2016)
Tools
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.3, January 12, 2017 Version 0.87.3, January 12, 2017
================================ ================================
bug fixes Bug fixes
o fixed OCaml extraction with respect to ghost parameters o fixed OCaml extraction with respect to ghost parameters
o assorted bug fixes o assorted bug fixes
provers Provers
o support for Alt-Ergo 1.30 (released Nov 21, 2016) o support for Alt-Ergo 1.30 (released Nov 21, 2016)
o support for Coq 8.6 (released Dec 8, 2016) o support for Coq 8.6 (released Dec 8, 2016)
o support for Gappa 1.3 (released Jul 20, 2016) o support for Gappa 1.3 (released Jul 20, 2016)
...@@ -31,14 +57,14 @@ provers ...@@ -31,14 +57,14 @@ provers
Version 0.87.2, September 1, 2016 Version 0.87.2, September 1, 2016
================================= =================================
bug fixes Bug fixes
o improved well-formedness of extracted OCaml code o improved well-formedness of extracted OCaml code
o assorted bug fixes o assorted bug fixes
Version 0.87.1, May 27, 2016 Version 0.87.1, May 27, 2016
============================ ============================
bug fixes Bug fixes
o assorted bug fixes o assorted bug fixes
Version 0.87.0, March 15, 2016 Version 0.87.0, March 15, 2016
......
...@@ -1058,7 +1058,7 @@ COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double ...@@ -1058,7 +1058,7 @@ COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES) COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES)) COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
COQLIBS_IEEEFLOAT_FILES = GenericFloat COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64
COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES)) COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES))
endif endif
...@@ -1125,7 +1125,7 @@ ifeq (@enable_coq_fp_libs@,yes) ...@@ -1125,7 +1125,7 @@ ifeq (@enable_coq_fp_libs@,yes)
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/ $(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/
endif endif
update-coq: remove-coq-headers update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float headers-coq update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
...@@ -1299,7 +1299,7 @@ clean:: ...@@ -1299,7 +1299,7 @@ clean::
ifeq (@enable_isabelle_libs@,yes) ifeq (@enable_isabelle_libs@,yes)
ISABELLEVERSIONSPECIFIC=why3.ML Why3_Bool.thy Why3_BV.thy Why3_Int.thy Why3_List.thy Why3_Number.thy Why3_Set.thy ISABELLEVERSIONSPECIFIC=ROOT why3.ML Why3_BV.thy Why3_Number.thy Why3_Real.thy Why3_Set.thy
ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC)) ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC))
ISABELLEVERSIONSPECIFICSOURCES=$(addsuffix .@ISABELLEVERSION@, $(ISABELLEVERSIONSPECIFICTARGETS)) ISABELLEVERSIONSPECIFICSOURCES=$(addsuffix .@ISABELLEVERSION@, $(ISABELLEVERSIONSPECIFICTARGETS))
...@@ -2175,23 +2175,16 @@ dist: $(MORE_DIST) ...@@ -2175,23 +2175,16 @@ dist: $(MORE_DIST)
# file headers # file headers
############### ###############
headers: headers-coq headers:
headache -c misc/headache_config.txt -h misc/header.txt \ headache -c misc/headache_config.txt -h misc/header.txt \
Makefile.in configure.in \ Makefile.in configure.in \
src/*/*.ml src/*/*.ml[iyl4] \ src/*/*.ml src/*/*.ml[iyl4] \
plugins/*/*.ml plugins/*/*.ml[ily] \ plugins/*/*.ml plugins/*/*.ml[ily] \
lib/coq-tactic/*.v lib/coq/*.v \ lib/coq-tactic/*.v lib/coq/*.v lib/coq/*/*.v \
src/server/*.c src/server/*.h \ src/server/*.c src/server/*.h \
src/ide/resetgc.c \ src/ide/resetgc.c \
examples/use_api/*.ml examples/use_api/*.ml
headers-coq:
headache -c misc/headache_config.txt -h misc/header.txt \
lib/coq/*/*.v
remove-coq-headers:
headache -r -c misc/headache_config.txt lib/coq/*/*.v
######### #########
# myself # myself
######### #########
......
# Why version # Why version
VERSION=0.87+git VERSION=0.88+git
...@@ -497,10 +497,13 @@ coq_compat_version= ...@@ -497,10 +497,13 @@ coq_compat_version=
if test "$enable_coq_tactic" = no -a "$enable_coq_libs" = no; then if test "$enable_coq_tactic" = no -a "$enable_coq_libs" = no; then
enable_coq_support=no enable_coq_support=no
AC_MSG_WARN(coq support disabled)
reason_coq_support=" (disabled by user)" reason_coq_support=" (disabled by user)"
fi fi
if test "$enable_coq_tactic" = no; then
reason_coq_tactic=" (disabled by user)"
fi
if test "$enable_coq_support" = yes; then if test "$enable_coq_support" = yes; then
AC_CHECK_PROG(COQC,coqc,coqc,no) AC_CHECK_PROG(COQC,coqc,coqc,no)
if test "$COQC" = no ; then if test "$COQC" = no ; then
...@@ -525,6 +528,10 @@ if test "$enable_coq_support" = yes; then ...@@ -525,6 +528,10 @@ if test "$enable_coq_support" = yes; then
coq_compat_version="COQ84" coq_compat_version="COQ84"
COQPPLIBS="$COQLIB/parsing/grammar.cma" COQPPLIBS="$COQLIB/parsing/grammar.cma"
AC_MSG_RESULT($COQVERSION) AC_MSG_RESULT($COQVERSION)
if test "$enable_coq_tactic" = yes; then
enable_coq_tactic=no
reason_coq_tactic=" (coq >= 8.5 not found)"
fi
;; ;;
8.5*) 8.5*)
coq_compat_version="COQ85" coq_compat_version="COQ85"
...@@ -600,7 +607,6 @@ fi ...@@ -600,7 +607,6 @@ fi
if test "$enable_pvs_libs" = no; then if test "$enable_pvs_libs" = no; then
enable_pvs_support=no enable_pvs_support=no
AC_MSG_WARN(PVS support disabled)
reason_pvs_support=" (disabled by user)" reason_pvs_support=" (disabled by user)"
else else
AC_CHECK_PROG(PVS,pvs,pvs,no) AC_CHECK_PROG(PVS,pvs,pvs,no)
...@@ -639,7 +645,6 @@ fi ...@@ -639,7 +645,6 @@ fi
if test "$enable_isabelle_libs" = no; then if test "$enable_isabelle_libs" = no; then
enable_isabelle_support=no enable_isabelle_support=no
AC_MSG_WARN(Isabelle support disabled)
reason_isabelle_support=" (disabled by user)" reason_isabelle_support=" (disabled by user)"
else else
AC_CHECK_PROG(ISABELLE,isabelle,isabelle,no) AC_CHECK_PROG(ISABELLE,isabelle,isabelle,no)
...@@ -657,16 +662,16 @@ else ...@@ -657,16 +662,16 @@ else
ISABELLEVERSION=2016-1 ISABELLEVERSION=2016-1
AC_MSG_RESULT($ISABELLEDETECTEDVERSION) AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;; ;;
2016*) 2017*)
enable_isabelle_support=yes enable_isabelle_support=yes
ISABELLEVERSION=2016 ISABELLEVERSION=2017
AC_MSG_RESULT($ISABELLEDETECTEDVERSION) AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;; ;;
*) *)
AC_MSG_RESULT($ISABELLEDETECTEDVERSION) AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
enable_isabelle_support=no enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle 2016 or later; Isabelle discarded) AC_MSG_WARN(You need Isabelle 2016-1 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2016)" reason_isabelle_support=" (need version >= 2016-1)"
;; ;;
esac esac
fi fi
......
\chapter{The \why API} \chapter{The \why API}
\label{chap:api}\index{API} \label{chap:api}\index{API}
%HEVEA\cutname{api.html}
This chapter is a tutorial for the users who want to link their own This chapter is a tutorial for the users who want to link their own
OCaml code with the \why library. We progressively introduce the way OCaml code with the \why library. We progressively introduce the way
......
\chapter{Executing \whyml Programs} \chapter{Executing \whyml Programs}
\label{chap:exec}\index{whyml@\whyml} \label{chap:exec}\index{whyml@\whyml}
%HEVEA\cutname{exec.html}
This chapter shows how \whyml code can be executed, either by being This chapter shows how \whyml code can be executed, either by being
interpreted or compiled to some existing programming language. interpreted or compiled to some existing programming language.
......
\chapter{Compilation, Installation} \chapter{Compilation, Installation}
\label{sec:install} \label{sec:install}
%HEVEA\cutname{install.html}
In short, installation proceeds as follows. In short, installation proceeds as follows.
\begin{flushleft}\ttfamily \begin{flushleft}\ttfamily
......
...@@ -11,9 +11,9 @@ using ``Edit'' action in \texttt{why3 ide}. ...@@ -11,9 +11,9 @@ using ``Edit'' action in \texttt{why3 ide}.
\subsection{Installation} \subsection{Installation}
You need version Isabelle2016 or Isabelle2016-1. Former versions are not You need version Isabelle2016-1 or Isabelle2017. Former versions are not
supported. We assume below that your version is 2016-1, please replace supported. We assume below that your version is 2017, please replace
2016-1 by 2016 otherwise. 2017 by 2016-1 otherwise.
Isabelle must be installed before compiling \why. After compilation Isabelle must be installed before compiling \why. After compilation
and installation of \why, you must manually add the path and installation of \why, you must manually add the path
...@@ -22,7 +22,7 @@ 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} \end{verbatim}
into either the user file into either the user file
\begin{verbatim} \begin{verbatim}
.isabelle/Isabelle2016-1/etc/components .isabelle/Isabelle2017/etc/components
\end{verbatim} \end{verbatim}
or the system-wide file or the system-wide file
\begin{verbatim} \begin{verbatim}
......
\chapter{Interactive Proof Assistants} \chapter{Interactive Proof Assistants}
%HEVEA\cutname{itp.html}
% ... We then provide specific information about some ITPs. % ... We then provide specific information about some ITPs.
......
\chapter{Reference Manuals for the \why Tools} \chapter{Reference Manuals for the \why Tools}
\label{chap:manpages} \label{chap:manpages}
%HEVEA\cutname{manpages.html}
This chapter details the usage of each of the command-line tools This chapter details the usage of each of the command-line tools
provided by the \why environment. The main command is \texttt{why3}; provided by the \why environment. The main command is \texttt{why3};
...@@ -475,7 +476,7 @@ are grouped together under several tabs. ...@@ -475,7 +476,7 @@ are grouped together under several tabs.
When the selected prover finds (counterexample) model, it is possible to When the selected prover finds (counterexample) model, it is possible to
display parts of this model in the terms of the original Why3 input. display parts of this model in the terms of the original Why3 input.
Currently, this is supported for CVC4 prover version 1.5 and newer. Currently, this is supported for CVC4 prover version 1.5 and Z3.
To display the counterexample in Why3 IDE, the counterexample model generation To display the counterexample in Why3 IDE, the counterexample model generation
must be enabled in File -/> Preferences -/> get must be enabled in File -/> Preferences -/> get
...@@ -489,7 +490,7 @@ displayed in a comment at the line below. ...@@ -489,7 +490,7 @@ displayed in a comment at the line below.
An alternative way how to display a counterexample is to use the option An alternative way how to display a counterexample is to use the option
\texttt{-{}-get-ce} of the \texttt{prove} command. \texttt{-{}-get-ce} of the \texttt{prove} command.
Why3 source code elemets that should be a part of counterexample must be Why3 source code elements that should be a part of counterexample must be
explicitly marked with \texttt{"model"} label. The following example shows a explicitly marked with \texttt{"model"} label. The following example shows a
Why3 theory with some terms annotated with the \texttt{model} label and the Why3 theory with some terms annotated with the \texttt{model} label and the
generated counterexample in comments: generated counterexample in comments:
......
...@@ -108,7 +108,7 @@ ...@@ -108,7 +108,7 @@
%BEGIN LATEX %BEGIN LATEX
\begin{LARGE} \begin{LARGE}
%END LATEX %END LATEX
Version \whyversion{}, January 2017 Version \whyversion{}, October 2017
%BEGIN LATEX %BEGIN LATEX
\end{LARGE} \end{LARGE}
%END LATEX %END LATEX
...@@ -159,6 +159,7 @@ ANR project (ANR-12-INSE-0010\begin{latexonly}, ...@@ -159,6 +159,7 @@ ANR project (ANR-12-INSE-0010\begin{latexonly},
\end{center} \end{center}
\chapter*{Foreword} \chapter*{Foreword}
%HEVEA\cutname{foreword.html}
%This is the manual for the Why platform version 3, or \why for %This is the manual for the Why platform version 3, or \why for
%short. %short.
...@@ -262,6 +263,7 @@ Thi-Minh-Tuyen Nguyen, M\'ario Pereira, Asma Tafat, Piotr Trojanek. ...@@ -262,6 +263,7 @@ Thi-Minh-Tuyen Nguyen, M\'ario Pereira, Asma Tafat, Piotr Trojanek.
\appendix \appendix
\chapter{Release Notes} \chapter{Release Notes}
%HEVEA\cutname{changes.html}
\section{Release Notes for version 0.80: syntax changes w.r.t. 0.73} \section{Release Notes for version 0.80: syntax changes w.r.t. 0.73}
......
\chapter{Getting Started} \chapter{Getting Started}
\label{chap:starting} \label{chap:starting}
%HEVEA\cutname{starting.html}
\section{Hello Proofs} \section{Hello Proofs}
......
\chapter{The \why Language} \chapter{The \why Language}
\label{chap:syntax} \label{chap:syntax}
%HEVEA\cutname{syntax.html}
This chapter describes the input syntax, and informally gives its semantics, This chapter describes the input syntax, and informally gives its semantics,
illustrated by examples. illustrated by examples.
......
\chapter{Language Reference} \chapter{Language Reference}
\label{chap:syntaxref} \label{chap:syntaxref}
%HEVEA\cutname{syntaxref.html}
This chapter gives the grammar and semantics for \why and \whyml input files. This chapter gives the grammar and semantics for \why and \whyml input files.
......
\chapter{Technical Informations} \chapter{Technical Informations}
%HEVEA\cutname{technical.html}
\section{Structure of Session Files} \section{Structure of Session Files}
...@@ -642,7 +642,7 @@ language are: ...@@ -642,7 +642,7 @@ language are:
To examplify this basic programming language, we give below the To examplify this basic programming language, we give below the
default strategies that are attached to the default buttons of the default strategies that are attached to the default buttons of the
IDE, assuming that the provers Alt-Ergo 1.01, CVC4 1.4 and Z3 4.4.1 IDE, assuming that the provers Alt-Ergo 1.30, CVC4 1.5 and Z3 4.5.0
were detected by the \verb|why3 config --detect| command were detected by the \verb|why3 config --detect| command
\begin{description} \begin{description}
\item[Split] is bound to the 1-line strategy \item[Split] is bound to the 1-line strategy
...@@ -650,16 +650,26 @@ were detected by the \verb|why3 config --detect| command ...@@ -650,16 +650,26 @@ were detected by the \verb|why3 config --detect| command
t split_goal_wp exit t split_goal_wp exit
\end{verbatim} \end{verbatim}
\item[Auto level 0] is bound to
\begin{verbatim}
c Z3,4.5.0, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
\end{verbatim}
The three provers are tried for a time limit of 1 second and memory
limit of 1~Gb, each in turn. This is a perfect strategy for a first
attempt to discharge a new goal.
\item[Auto level 1] is bound to \item[Auto level 1] is bound to
\begin{verbatim} \begin{verbatim}
start: start:
c Z3,4.4.1, 1 1000 c Z3,4.5.0, 1 1000
c Alt-Ergo,1.01, 1 1000 c Alt-Ergo,1.30, 1 1000
c CVC4,1.4, 1 1000 c CVC4,1.5, 1 1000
t split_goal_wp start t split_goal_wp start
c Z3,4.4.1, 10 4000 c Z3,4.5.0, 10 4000
c Alt-Ergo,1.01, 10 4000 c Alt-Ergo,1.30, 10 4000
c CVC4,1.4, 10 4000 c CVC4,1.5, 10 4000
\end{verbatim} \end{verbatim}
The three provers are first tried for a time limit of 1 second and The three provers are first tried for a time limit of 1 second and
memory limit of 1~Gb, each in turn. If none of them succeed, a memory limit of 1~Gb, each in turn. If none of them succeed, a
...@@ -670,17 +680,17 @@ c CVC4,1.4, 10 4000 ...@@ -670,17 +680,17 @@ c CVC4,1.4, 10 4000
\item[Auto level 2] is bound to \item[Auto level 2] is bound to
\begin{verbatim} \begin{verbatim}
start: start:
c Z3,4.4.1, 1 1000 c Z3,4.5.0, 1 1000
c Eprover,1.8-001, 1 1000 c Eprover,2.0, 1 1000
c Spass,3.7, 1 1000 c Spass,3.7, 1 1000
c Alt-Ergo,1.01, 1 1000 c Alt-Ergo,1.30, 1 1000
c CVC4,1.4, 1 1000 c CVC4,1.5, 1 1000
t split_goal_wp start t split_goal_wp start
c Z3,4.4.1, 5 2000 c Z3,4.5.0, 5 2000
c Eprover,1.8-001, 5 2000 c Eprover,2.0, 5 2000
c Spass,3.7, 5 2000 c Spass,3.7, 5 2000
c Alt-Ergo,1.01, 5 2000 c Alt-Ergo,1.30, 5 2000
c CVC4,1.4, 5 2000 c CVC4,1.5, 5 2000
t introduce_premises afterintro t introduce_premises afterintro
afterintro: afterintro:
t inline_goal afterinline t inline_goal afterinline
...@@ -688,12 +698,11 @@ g trylongertime ...@@ -688,12 +698,11 @@ g trylongertime
afterinline: afterinline:
t split_goal_wp start t split_goal_wp start
trylongertime: trylongertime:
c Z3,4.4.1, 30 4000 c Z3,4.5.0, 30 4000
c Eprover,1.8-001, 30 4000 c Eprover,2.0, 30 4000
c Spass,3.7, 30 4000 c Spass,3.7, 30 4000
c Alt-Ergo,1.01, 30 4000 c Alt-Ergo,1.30, 30 4000
c CVC4,1.4, 30 4000 c CVC4,1.5, 30 4000
\end{verbatim} \end{verbatim}
Notice that now 5 provers are used. The provers are first tried for Notice that now 5 provers are used. The provers are first tried for
a time limit of 1 second and memory limit of 1~Gb, each in turn. If a time limit of 1 second and memory limit of 1~Gb, each in turn. If
...@@ -701,7 +710,7 @@ c CVC4,1.4, 30 4000 ...@@ -701,7 +710,7 @@ c CVC4,1.4, 30 4000
the same strategy is retried on each sub-goals. If the split does the same strategy is retried on each sub-goals. If the split does
not succeed, the prover are tried again with limits of 5 s and 2 not succeed, the prover are tried again with limits of 5 s and 2
Gb. If all fail, we attempt the transformation of introduction of Gb. If all fail, we attempt the transformation of introduction of
premises in the context, followed by an inlining of the definiiions premises in the context, followed by an inlining of the definitions
in the goals. We then attempt a split again, if the split succeeds, in the goals. We then attempt a split again, if the split succeeds,
we restart from the beginning, if it fails then provers are tried we restart from the beginning, if it fails then provers are tried
again with 30s and 4 Gb. again with 30s and 4 Gb.
......
\chapter{The \whyml Programming Language} \chapter{The \whyml Programming Language}
\label{chap:whyml} \label{chap:whyml}
%HEVEA\cutname{whyml.html}
This chapter describes the \whyml programming language. This chapter describes the \whyml programming language.
A \whyml input text contains a list of theories (see A \whyml input text contains a list of theories (see
......
...@@ -29,6 +29,7 @@ transformation "eliminate_builtin" ...@@ -29,6 +29,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition" transformation "eliminate_definition"
transformation "eliminate_inductive" transformation "eliminate_inductive"
transformation "eliminate_algebraic" transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"