Commit 4822694f authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'master' into new_system

parents a7c1eea4 7129b259
......@@ -152,7 +152,6 @@ why3.conf
/src/coq-tactic/.why3-vo-*
# Coq
/lib/coq/bv/BV_Gen.v
# PVS
.pvscontext
......@@ -200,6 +199,8 @@ pvsbin/
/src/util/config.ml
/src/util/lexlib.ml
/src/util/rc.ml
/src/util/json_parser.mli
/src/util/json_parser.ml
# /src/session
/src/session/xml.ml
......@@ -216,6 +217,13 @@ pvsbin/
/plugins/tptp/tptp_parser.conflicts
/plugins/parser/dimacs.ml
# /plugins/python/
/plugins/python/py_lexer.ml
/plugins/python/py_parser.ml
/plugins/python/py_parser.mli
/plugins/python/test/
/plugins/python/py_parser.conflicts
# /drivers
/drivers/coq-realizations.aux
/drivers/pvs-realizations.aux
......@@ -228,6 +236,8 @@ pvsbin/
/tests/test-and/
/tests/test-extraction/*
!/tests/test-extraction/main.ml
/tests/python/*/why3session.xml
/tests/python/*/why3shapes.gz
# /examples/
/examples/in_progress/course/
......@@ -288,6 +298,7 @@ pvsbin/
/modules/pqueue/
/modules/mach/array/
/modules/mach/int/
/modules/python/
# Try Why3
/src/trywhy3/trywhy3.byte
......@@ -304,9 +315,13 @@ pvsbin/
/src/trywhy3/index.html
/src/trywhy3/ace-builds/
/src/trywhy3/*.png
/src/trywhy3/alt-ergo-1.00-private-2015-01-29
/src/trywhy3/alt-ergo*
/src/trywhy3/fontawesome/
# IDE
/src/ide/fontawesome
/src/ide/ace-builds
# jessie3
/src/jessie/config.log
/src/jessie/Makefile
......
......@@ -13,10 +13,12 @@ S src/coq-tactic
S src/why3session
S src/why3doc
S src/jessie
S src/trywhy3
S plugins/parser
S plugins/printer
S plugins/transform
S plugins/tptp
S plugins/python
B src/util
B src/core
......@@ -33,10 +35,12 @@ B src/coq-tactic
B src/why3session
B src/why3doc
B src/jessie
B src/trywhy3
B plugins/parser
B plugins/printer
B plugins/transform
B plugins/tptp
B plugins/python
B lib/why3
PKG str unix num dynlink @ZIPLIB@ @LABLGTK2PKG@ @META_OCAMLGRAPH@
......@@ -12,9 +12,13 @@ with contributions of
Sylvie Boldo
Martin Clochard
Simon Cruanes
Sylvain Dailler
Clément Fumex
Leon Gondelman
David Hauzar
Daisuke Ishii
Johannes Kanig
Mikhail Mandrykin
David Mentré
Benjamin Monate
Thi-Minh-Tuyen Nguyen
......
* marks an incompatible change
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 ??, 2017
=================================
Version 0.87.3, January 12, 2017
================================
bug fixes
o
o fixed OCaml extraction with respect to ghost parameters
o assorted bug fixes
Provers
o support for Alt-Ergo 1.30 (released ??, 2016)
o support for Coq 8.6 (released ?, 2016)
o support for Gappa 1.3 (released ?, 2016)
provers
o support for Alt-Ergo 1.30 (released Nov 21, 2016)
o support for Coq 8.6 (released Dec 8, 2016)
o support for Gappa 1.3 (released Jul 20, 2016)
* discarded support for Isabelle 2015
o support for Isabelle 2016-1 (released Dec 2016)
o support for Z3 4.5.0 (released ? 2016)
o support for Z3 4.5.0 (released Nov 8, 2016)
Version 0.87.2, September 1, 2016
=================================
......
This diff is collapsed.
####################################################################
# #
# The Why3 Verification Platform / The Why3 Development Team #
# Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University #
# Copyright 2010-2017 -- 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 #
......@@ -176,8 +176,8 @@ OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
echo "ocaml version is $OCAMLVERSION"
case "$OCAMLVERSION" in
0.*|1.*|2.*|3.*|4.00.*)
AC_MSG_ERROR(You need Objective Caml 4.01.0 or higher);;
0.*|1.*|2.*|3.*|4.00.*|4.01.*|4.02.[[0-2]])
AC_MSG_ERROR(You need Objective Caml 4.02.3 or higher);;
esac
# Ocaml library path
......
......@@ -5,8 +5,9 @@ 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
one can use the library to build terms, formulas, theories, proof
tasks, call external provers on tasks, and apply transformations on
tasks. The complete documentation for API calls is given
at URL~\url{http://why3.lri.fr/api-\whyversion/}.
tasks. The complete documentation for API calls is given\begin{latexonly}
at URL~\urlapi{}.\end{latexonly}
%HEVEA at this \ahref{\urlapi}{URL}.
We assume the reader has a fair knowledge of the OCaml
language. Notice that the \why library must be installed, see
......
......@@ -588,7 +588,7 @@ counterexample of an abstract value:
More examples of using counterexample feature of Why3 can be found in the file
examples/tests/cvc4-models.mlw and examples/tests/cvc4-models.mlw.
More information how counterexamples in Why3 works can be found
in~\cite{sefm16}.
in~\cite{hauzar16sefm}.
%
% how to use counterexamples - explain labels, projections, the option --get-ce of why3prove and the setting in why3ide
......
......@@ -232,21 +232,36 @@ Claude March\'e and Andrei Paskevich},
year = {2007}
}
@inproceedings{sefm16,
author = {Guillaume Melquiond},
title = {Floating-point arithmetic in the {C}oq system},
booktitle = {Proceedings of the 8th Conference on Real Numbers and
Computers},
address = {Santiago de Compostela, Spain},
year = {2008},
pages = {93--102},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {RNC},
@InProceedings{hauzar16sefm,
topics = {team},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-pdf = {http://www.lri.fr/~melquion/doc/08-rnc8-article.pdf}
author = {Hauzar, David and March\'e, Claude and Moy, Yannick},
title = {Counterexamples from Proof Failures in {SPARK}},
booktitle = {Software Engineering and Formal Methods},
year = 2016,
pages = {215--233},
hal = {https://hal.inria.fr/hal-01314885}
}
@techreport{ieee754-2008,
abstract = {This standard specifies interchange and arithmetic
formats and methods for binary and decimal
floating-point arithmetic in computer programming
environments. This standard specifies exception
conditions and their default handling. An
implementation of a floating-point system conforming
to this standard may be realized entirely in
software, entirely in hardware, or in any
combination of software and hardware. For operations
specified in the normative part of this standard,
numerical results and exceptions are uniquely
determined by the values of the input data, sequence
of operations, and destination formats, all under
user control.},
booktitle = {{IEEE} Std 754-2008},
doi = {10.1109/IEEESTD.2008.4610935},
journal = {IEEE Std 754-2008},
pages = {1--58},
title = {{IEEE} Standard for Floating-Point Arithmetic},
year = {2008}
}
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, September 2016
Version \whyversion{}, January 2017
%BEGIN LATEX
\end{LARGE}
%END LATEX
......@@ -209,9 +209,9 @@ Report any bug to the \why Bug Tracking System:
We gratefully thank the people who contributed to \why, directly or
indirectly: Romain Bardou, Stefan Berghofer, Sylvie Boldo, Martin
Clochard, Simon Cruanes, Leon Gondelman, Johannes Kanig, St\'ephane
Clochard, Simon Cruanes, L\'eon Gondelman, Johannes Kanig, St\'ephane
Lescuyer, David Mentr\'e, Sim\~ao Melo de Sousa, Benjamin Monate,
Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
Thi-Minh-Tuyen Nguyen, M\'ario Pereira, Asma Tafat, Piotr Trojanek.
\cleardoublepage
......
\begin{syntax}
module ::= "module" uident label* mdecl* "end"
module ::= "module" uident-nq label* mdecl* "end"
\
mdecl ::= decl ; theory declaration
| "type" mtype-decl ("with" mtype-decl)* ; mutable types
| "type" lident ("'" lident)* invariant+ ; added invariant
| "let" "ghost"? lident label* pgm-defn ;
| "type" lident-nq ("'" lident-nq)* invariant+ ; added invariant
| "let" "ghost"? lident-nq label* pgm-defn ;
| "let" "rec" rec-defn ;
| "val" "ghost"? lident label* pgm-decl ;
| "exception" lident label* type? ;
| "namespace" "import"? uident mdecl* "end" ;
| "val" "ghost"? lident-nq label* pgm-decl ;
| "exception" lident-nq label* type? ;
| "namespace" "import"? uident-nq mdecl* "end" ;
\
mtype-decl ::= lident label* ("'" lident label*)* ;
mtype-decl ::= lident-nq label* ("'" lident-nq label*)* ;
mtype-defn ;
\
mtype-defn ::= ; abstract type
......@@ -19,7 +19,7 @@
| "=" "{" mrecord-field (";" mrecord-field)* "}" ; record type
invariant*
\
mrecord-field ::= "ghost"? "mutable"? lident label* ":" type
mrecord-field ::= "ghost"? "mutable"? lident-nq label* ":" type
\
pgm-defn ::= fun-body ;
| "=" "fun" binder+ spec* "->" spec* expr ;
......
......@@ -5,9 +5,11 @@
\
alpha ::= lalpha | ualpha
\
lident ::= lalpha (alpha | digit | "'")*
suffix ::= (alpha | digit | "'")*
\
uident ::= ualpha (alpha | digit | "'")*
lident ::= lalpha suffix
\
uident ::= ualpha suffix
\
ident ::= lident | uident
\
......@@ -15,5 +17,17 @@
\
uqualid ::= uident | uqualid "." uident
\
qualid ::= ident | uqualid "." ident ;%
qualid ::= ident | uqualid "." ident
\
digit-or-us ::= "0"-"9" | "_"
\
alpha-no-us ::= "a"-"z" | "A"-"Z"
\
suffix-nq ::= (alpha-no-us | "'"* digit-or-us)* "'"*
\
lident-nq ::= lalpha suffix-nq
\
uident-nq ::= ualpha suffix-nq
\
ident-nq ::= lident-nq | uident-nq ;%
\end{syntax}
......@@ -24,12 +24,23 @@ In the following, strings are referred to with the non-terminal
\subsection{Identifiers}
The syntax distinguishes lowercase and
uppercase identifiers and, similarly, lowercase and uppercase
qualified identifiers.
Identifiers are non-empty sequences of characters among letters,
digits, the underscore character and the quote character. They cannot
start with a digit or a quote.
\begin{center}\framebox{\input{./qualid_bnf.tex}}\end{center}
The syntax distinguishes identifiers that start with a lowercase or an
uppercase letter (resp. \nonterm{lident}{} and \nonterm{uident}{}), and
similarly, lowercase and uppercase qualified identifiers.
The restricted classes of identifiers denoted by \nonterm{lident-nq}{}
and \nonterm{uident-nq}{} correspond to identifiers where the quote
character cannot be followed by a letter. Identifiers where a quote is
followed by a letter are reserved and cannot be used as identifier for
declarations introduced by the user (see Section~\ref{sec:rangetypes}).
\subsection{Constants}
The syntax for constants is given in Figure~\ref{fig:bnf:constant}.
Integer and real constants have arbitrary precision.
......@@ -115,6 +126,7 @@ Note that the syntax for type
expressions notably differs from the usual ML syntax (\eg the
type of polymorphic lists is written \texttt{list 'a}, not \texttt{'a list}).
\subsection{Formulas}
The syntax for formulas is given Figure~\ref{fig:bnf:formula}.
......@@ -179,6 +191,101 @@ The syntax for theories is given on Figure~\ref{fig:bnf:theorya} and~\ref{fig:bn
\label{fig:bnf:theoryb}
\end{figure}
\subsubsection{Algebraic types}
TO BE COMPLETED
\subsubsection{Record types}
TO BE COMPLETED
\subsubsection{Range types}
\label{sec:rangetypes}
A declaration of the form \texttt{type r = < range \textit{a b} >}
defines a type that projects into the integer range
\texttt{[\textit{a,b}]}. Note that in order to make such a declaration
the theory \texttt{int.Int} must be imported.
Why3 let you cast an integer literal in a range type
(e.g. \texttt{(42:r)}) and will check at typing that the literal is in
range. Defining such a range type $r$ automatically introduces the
following:
\begin{whycode}
function r'int r : int
constant r'maxInt : int
constant r'minInt : int
\end{whycode}
The function \texttt{r'int} projects a term of type \texttt{r} to its
integer value. The two constants represent the high bound and low
bound of the range respectively.
Unless specified otherwise with the meta \texttt{"keep:literal"} on
\texttt{r}, the transformation \emph{eliminate\_literal} introduces an
axiom
\begin{whycode}
axiom r'axiom : forall i:r. r'minInt <= r'int i <= r'maxInt
\end{whycode}
and replaces all casts of the form \texttt{(42:r)} with a constant and
an axiom as in:
\begin{whycode}
constant rliteral7 : r
axiom rliteral7_axiom : r'int rliteral7 = 42
\end{whycode}
This type is used in the standard library in the theories
\texttt{bv.BV8}, \texttt{bv.BV16}, \texttt{bv.BV32}, \texttt{bv.BV64}.
\subsubsection{Floating-point Types}
A declaration of the form \texttt{type f = < float \textit{eb sb} >}
defines a type of floating-point numbers as specified by the IEEE-754
standard~\cite{ieee754}. Here the literal \texttt{\textit{eb}}
represents the number of bits in the exponent and the literal
\texttt{\textit{sb}} the number of bits in the significand (including
the hidden bit). Note that in order to make such a declaration the
theory \texttt{real.Real} must be imported.
Why3 let you cast a real literal in a float type
(e.g. \texttt{(0.5:f)}) and will check at typing that the literal is
representable in the format. Note that Why3 do not implicitly round a
real literal when casting to a float type, it refuses the cast if the
literal is not representable.
Defining such a type \texttt{f} automatically introduces the following:
\begin{whycode}
predicate f'isFinite f
function f'real f : real
constant f'eb : int
constant f'sb : int
\end{whycode}
As specified by the IEEE standard, float formats includes infinite
values and also a special NaN value (Not-a-Number) to represent
results of undefined operations such as $0/0$. The predicate
\texttt{f'isFinite} indicates whether its argument is neither infinite
nor NaN. The function \texttt{f'real} projects a finite term of type
\texttt{f} to its real value, its result is not specified for non finite
terms.
Unless specified otherwise with the meta \texttt{"keep:literal"} on
\texttt{f}, the transformation \emph{eliminate\_literal} will
introduce an axiom
\begin{whycode}
axiom f'axiom :
forall x:f. f'isFinite x -> -. max_real <=. f'real x <=. max_real
\end{whycode}
where \texttt{max\_real} is the value of the biggest finite float in
the specified format. The transformation also replaces all casts of
the form \texttt{(0.5:f)} with a constant and an axiom as in:
\begin{whycode}
constant fliteral42 : f
axiom fliteral42_axiom : f'real fliteral42 = 0.5 /\ f'isFinite fliteral42
\end{whycode}
This type is used in the standard library in the theories
\texttt{ieee\_float.Float32} and \texttt{ieee\_float.Float64}.
\subsection{Files}
A \why input file is a (possibly empty) list of theories.
......
\begin{syntax}
theory ::= "theory" uident label* decl* "end"
theory ::= "theory" uident-nq label* decl* "end"
\
decl ::= "type" type-decl ("with" type-decl)* ;
| "constant" constant-decl ;
......@@ -7,29 +7,29 @@
| "predicate" predicate-decl ("with" logic-decl)* ;
| "inductive" inductive-decl ("with" inductive-decl)* ;
| "coinductive" inductive-decl ("with" inductive-decl)* ;
| "axiom" ident ":" formula ;
| "lemma" ident ":" formula ;
| "goal" ident ":" formula ;
| "axiom" ident-nq ":" formula ;
| "lemma" ident-nq ":" formula ;
| "goal" ident-nq ":" formula ;
| "use" imp-exp tqualid ("as" uident)? ;
| "clone" imp-exp tqualid ("as" uident)? subst? ;
| "namespace" "import"? uident decl* "end" ;
| "namespace" "import"? uident-nq decl* "end" ;
\
logic-decl ::= function-decl ;
| predicate-decl
\
constant-decl ::= lident label* ":" type ;
| lident label* ":" type "=" term
constant-decl ::= lident-nq label* ":" type ;
| lident-nq label* ":" type "=" term
\
function-decl ::= lident label* type-param* ":" type ;
| lident label* type-param* ":" type "=" term
function-decl ::= lident-nq label* type-param* ":" type ;
| lident-nq label* type-param* ":" type "=" term
\
predicate-decl ::= lident label* type-param* ;
| lident label* type-param* "=" formula
predicate-decl ::= lident-nq label* type-param* ;
| lident-nq label* type-param* "=" formula
\
inductive-decl ::= lident label* type-param* "=" ;
inductive-decl ::= lident-nq label* type-param* "=" ;
"|"? ind-case ("|" ind-case)* ;
\