Skip to content

GitLab

why3
why3
Commit dba92e2e authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

update documentation for the recent syntax changes

parent 300863d2
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 145 additions and 137 deletions
CHANGES
View file @ dba92e2e
* marks an incompatible change
o WhyML with mutable record fields and type models
o why3replayer
o new syntax for logical connections
conjunction and /\
disjunction or \/
negation not ~
implication implies ->
equivalence iff <->
* "logic" is not a keyword anymore, use "function" and "predicate"
* new syntax for conjunction (/\) and disjunction (\/)
* functions to create an environment are now exported from Env
o fixed Alt-ergo output: no triggers for "exists" quantifier
o [IDE] tool "Replay" works
o [IDE] does not use Threads anymore, thanks to Call_provers.query_call
o VC gen produces explanations in a suitable form for IDE
o [IDE] displays explanations using labels of the form "expl:..."
o fixed Coq output for polymorphic inductive predicates
o [IDE] dropped dependence on Sqlite
* calls to prover can now be asynchronous
Driver.prove_task now returns some intermediate value (of type
prover_call), which can be queried in two ways:
......@@ -20,7 +20,7 @@
- non-blocking way with Call_provers.query_call
So old code performing "prove_task t () ()" should be translated to
"wait_on_call (prove_task t ()) ()".
o record types in the logic
o record types
- introduced with syntax "type t = {| a:int; b:bool |}"
actually syntactic sugar for "type t = `mk t' (a:int) (b:bool)"
i.e. an algebraic with one constructor and projection functions
......
doc/api.tex
View file @ dba92e2e
......@@ -51,7 +51,7 @@ ocamlc str.cma unix.cma nums.cma dynlink.cma \
\end{verbatim}
Running the generated executable \texttt{f} results in the following output.
\begin{verbatim}
formula 1 is: true or false
formula 1 is: true \/ false
\end{verbatim}
Let's now build a formula with propositional variables: $A \land B
......@@ -77,7 +77,7 @@ let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2
As expected, the output is as follows.
\begin{verbatim}
formula 2 is: A and B -> A
formula 2 is: A /\ B -> A
\end{verbatim}
Notice that the concrete syntax of \why\ forbids predicate identifiers
to start with a capital letter. This constraint does not exist when
......@@ -133,16 +133,16 @@ Execution of our OCaml program now outputs:
\begin{verbatim}
task 1 is:
theory Task
goal Goal1 : true or false
goal Goal1 : true \/ false
end
task 2 is:
theory Task
logic A
predicate A
logic B
predicate B
goal Goal2 : A and B -> A
goal Goal2 : A /\ B -> A
end
\end{verbatim}
......
doc/expr.bnf
View file @ dba92e2e
......@@ -36,7 +36,7 @@
\
expr-case ::= pattern "->" expr ;
\
field-value ::= lqualid "=" expr ;
field-value ::= lqualid "=" expr ";" ;
\
triple ::= expr ;
| pre expr post ; Hoare triple
......@@ -50,4 +50,4 @@
loop-inv ::= "invariant" annotation
\
variant ::= "variant" "{" term "}" ("with" lqualid)?
\end{syntax}
\ No newline at end of file
\end{syntax}
doc/formula.bnf
View file @ dba92e2e
......@@ -2,9 +2,9 @@
formula ::= "true" | "false" ;
| formula "->" formula ; implication
| formula "<->" formula ; equivalence
| formula "and" formula ; conjunction
| formula "/\" formula ; conjunction
| formula "&&" formula ; asymmetric conjunction
| formula "or" formula ; disjunction
| formula "\/" formula ; disjunction
| formula "||" formula ; asymmetric disjunction
| "not" formula ; negation
| lqualid ; symbol
......
doc/library.tex
View file @ dba92e2e
......@@ -10,10 +10,10 @@ corresponding file, or alternatively, use the \verb|why3| with option
> why3 -T bool.Ite
theory Ite
(* use BuiltIn *)
(* use Bool *)
logic ite (b:bool) (x:'a) (y:'a) : 'a =
function ite (b:bool) (x:'a) (y:'a) : 'a =
match b with
| True -> x
| False -> y
......@@ -214,8 +214,8 @@ is inspired by~\cite{ayad10ijcar}.
\section{Library \texttt{string}}
\begin{description}
\item[Char]
\item[String]
\item[Char]
\item[String]
\end{description}
%%% Local Variables:
......
doc/manpages.tex
View file @ dba92e2e
......@@ -69,7 +69,7 @@ make install_lib
\why\ can use a wide range of external theorem provers. These need to
be installed separately, and then \why\ needs to be configured to use
them. There is no need to install these provers before compiling and
installing Why.
installing Why.
For installation of external provers, please look at the Why provers
tips page \url{http://why.lri.fr/provers.en.html}.
......@@ -101,9 +101,9 @@ tracking system).
The result of provers detection is stored in the user's
configuration file (\verb+~/.why.conf+ or, in the case of local
installation, \verb+why.conf+ in Why3 sources top directory). This file
installation, \verb+why.conf+ in Why3 sources top directory). This file
is also human-readable, and advanced users may modify it in order to
experiment with different ways of calling provers, \eg{} different
experiment with different ways of calling provers, \eg{} different
versions of the same prover, or with different options.
The provers which are typically looked for are
......@@ -127,7 +127,7 @@ printer, as explained in the corresponding section.
If the user's configuration file is already present,
\texttt{why3config} will only reset unset variables to default value,
but will not try to detect provers.
but will not try to detect provers.
The option \texttt{--detect-provers} should be used to force
\why\ to detect again the available
provers and to replace them in the configuration file. The option
......@@ -152,9 +152,9 @@ The \texttt{why3} tool executes the following steps:
\item Parse and typecheck the given files using the correct parser in order
to obtain a set of \why\ theories for each file. It uses
the filename extension or the \texttt{--format} option to choose
among the available parsers. The \texttt{--list-format} option gives
among the available parsers. The \texttt{--list-format} option gives
the list of registered parsers.
\item Extract the selected goals inside each of the selected theories
\item Extract the selected goals inside each of the selected theories
into tasks. The goals and theories are selected using the options
\texttt{-G/--goal} and \texttt{-T/--theory}. The option
\texttt{-T/--theory} applies to the last file appearing on the
......@@ -248,7 +248,7 @@ the actions of the various menus and buttons of the interface.
\item[Replay] replay all obsolete proofs [NOT YET AVAILABLE]
\item[Remove] Removes a proof attempt or a transformation.
\item[Remove] Removes a proof attempt or a transformation.
\end{description}
......@@ -286,7 +286,7 @@ The preferences window allows you customize
pressed. This might be overidden for a specific prover (the only way
to do that for the moment is to manually edit the config file)
\item the time limit given to provers, in seconds
\item the maximal number of simultaneous provers allowed to run in parallel.
\item the maximal number of simultaneous provers allowed to run in parallel.
\end{itemize}
\subsection{Structure of the database file}
......@@ -497,7 +497,7 @@ definitions~\cite{paskevich09rr}
\item[eliminate\_if\_fmla] replaces formulas of the form \texttt{if f1 then f2
else f3} by an equivalent formula using implications and other
connectives.
connectives.
\item[eliminate\_if]
Apply both transformations above.
......@@ -544,7 +544,8 @@ definitions~\cite{paskevich09rr}
removes definitions of the form
\begin{verbatim}
logic f x_1 .. x_n = (g e_1 .. e_k)
function f x_1 .. x_n = (g e_1 .. e_k)
predicate p x_1 .. x_n = (q e_1 .. e_k)
\end{verbatim}
when each $e_i$ is either a ground term or one of the $x_j$, and
each $x_1$ .. $x_n$ occur at most once in the $e_i$
......@@ -565,14 +566,14 @@ each $x_1$ .. $x_n$ occur at most once in the $e_i$
\item[simplify\_recursive\_definition] reduces mutually recursive
definitions if they are not really mutually recursive, e.g.:
\begin{verbatim}
logic f : ... = .... g ...
function f : ... = .... g ...
with g : .. = e
\end{verbatim}
becomes
\begin{verbatim}
logic g : .. = e
logic f : ... = .... g ...
function g : .. = e
function f : ... = .... g ...
\end{verbatim}
if f does not occur in e
......@@ -586,13 +587,13 @@ or
forall x, t=x -> P(x)
\end{verbatim}
when x does not occur in t
into
into
\begin{verbatim}
P(t)
\end{verbatim}
More generally, it applies this simplification whenever x=t appear
in a negative position.
\item[simplify\_trivial\_quantification\_in\_goal]
same as above but applies only in the goal.
......
doc/starting.tex
View file @ dba92e2e
......@@ -6,7 +6,7 @@
The first and basic step in using \why\ is to write a suitable input
file. When one wants to learn a programming language, you start by
writing a basic program. Here we start by writing a file containing a
basic set of goals.
basic set of goals.
Here is our first \why\ file, which is the file
\texttt{examples/hello\_proof.why} of the distribution.
......@@ -24,7 +24,7 @@ We don't give more details here about the syntax and refer to
Chapter~\ref{chap:syntax} for detailed explanations. In the following,
we show how this file is handled in the \why\ GUI
(Section~\ref{sec:gui}) then in batch mode using the \texttt{why3}
executable (Section~\ref{sec:batch}).
executable (Section~\ref{sec:batch}).
\section{Getting Started with the GUI}
......@@ -73,7 +73,7 @@ file is shown on the bottom right part.
Notice also that three provers were detected, and are now shown
in the ``provers'' section of the left toolbar. In this example,
detected provers are Alt-Ergo~\cite{ergo}, Coq~\cite{CoqArt} and
Simplify~\cite{simplify05}.
Simplify~\cite{simplify05}.
\subsection{Calling provers on goals}
......@@ -99,7 +99,7 @@ are not proved, they are marked with an orange question mark.
You can immediately attempt to prove the remaining goals using another
prover, {\eg} Alt-Ergo, by clicking on the corresponding button. The
goal $G_3$ should be proved now, but not $G_2$.
goal $G_3$ should be proved now, but not $G_2$.
\subsection{Applying transformations}
......@@ -130,7 +130,7 @@ Please take care of the comments of this file. Only the part between
the two last comments can be modified. Moreover, these comments
themselves should not be modified at all, they are used to mark the
part you modify, in order to regenerate the file if the goal is
changed.
changed.
\begin{figure}[tbp]
\includegraphics[width=\textwidth]{coqide.png}
......@@ -147,7 +147,7 @@ explained below.
Currently, the GUI does not allow to modify the input file. You must
exit the GUI and modify the file by some editor of your choice. Let's assume we change the goal $G_2$ by replacing the first occurrence of true by false, \eg
\begin{verbatim}
goal G2 : (false -> false) and (true or false)
goal G2 : (false -> false) /\ (true \/ false)
\end{verbatim}
Starting the IDE on the modified file and expanding everything with
\textsf{Ctrl-E}, we get the tree view shown on Figure~\ref{fig:gui5}.
......@@ -194,7 +194,7 @@ Known provers:
\end{verbatim}
The first word of each line is a unique identifier for the associated prover. We thus
have now the three provers Alt-Ergo~\cite{ergo}, Coq~\cite{CoqArt} and
Simplify~\cite{simplify05}.
Simplify~\cite{simplify05}.
Let's assume now we want to run Simplify on the HelloProof
example. The command to type and its output are as follows, where the
......
doc/syntax.tex
View file @ dba92e2e
......@@ -8,7 +8,7 @@ A \why\ text contains a list of \emph{theories}.
A theory is a list of \emph{declarations}. Declarations introduce new
types, functions and predicates, state axioms, lemmas and goals.
These declarations can be directly written in the theory or taken from
existing theories. The base logic of \why\ is a first-order
existing theories. The base logic of \why\ is first-order
logic with polymorphic types.
\subsection{Example 1: lists}
......@@ -35,7 +35,7 @@ theory Length
use import List
use import int.Int
logic length (l : list 'a) : int =
function length (l : list 'a) : int =
match l with
| Nil -> 0
| Cons _ r -> 1 + length r
......@@ -77,8 +77,9 @@ either appear earlier in the current file, \eg\ \texttt{List}, or are
predefined.
The next declaration defines a recursive function, \texttt{length},
which computes the length of a list. The \texttt{logic} keyword is
used to introduce or define both function and predicate symbols.
which computes the length of a list. The \texttt{function} and
\texttt{predicate} keywords are used to introduce function and
predicate symbols, respectively.
\why\ checks every recursive, or mutually recursive, definition for
termination. Basically, we require a lexicographic and structural
descent for every recursive call for some reordering of arguments.
......@@ -122,7 +123,7 @@ abstract (\emph{i.e.}~declared but not defined) symbols.
\begin{verbatim}
theory Order
type t
logic (<=) t t
predicate (<=) t t
axiom Le_refl : forall x : t. x <= x
axiom Le_asym : forall x y : t. x <= y -> y <= x -> x = y
......@@ -145,7 +146,7 @@ end
theory SortedIntList
use import int.Int
clone SortedGen with type O.t = int, logic O.(<=) = (<=)
clone SortedGen with type O.t = int, predicate O.(<=) = (<=)
end
\end{verbatim}
\caption{Example of Why3 text (continued).}
......@@ -238,7 +239,7 @@ theory SortedIntList
axiom Le_trans : forall x:int, y:int, z:int. x <= y -> y <= z
-> x <= z
(* clone Order with type t = int, logic (<=) = (<=),
(* clone Order with type t = int, predicate (<=) = (<=),
prop Le_trans1 = Le_trans, prop Le_asym1 = Le_asym,
prop Le_refl1 = Le_refl *)
......@@ -248,8 +249,8 @@ theory SortedIntList
| Sorted_Two : forall x:int, y:int, l:list int. x <= y ->
sorted (Cons y l) -> sorted (Cons x (Cons y l))
(* clone SortedGen with type t1 = int, logic sorted1 = sorted,
logic (<=) = (<=), prop Sorted_Two1 = Sorted_Two,
(* clone SortedGen with type t1 = int, predicate sorted1 = sorted,
predicate (<=) = (<=), prop Sorted_Two1 = Sorted_Two,
prop Sorted_One1 = Sorted_One, prop Sorted_Nil1 = Sorted_Nil,
prop Le_trans2 = Le_trans, prop Le_asym2 = Le_asym,
prop Le_refl2 = Le_refl *)
......@@ -347,8 +348,8 @@ theory Bijection
type t
type u
logic of t : u
logic to u : t
function of t : u
function to u : t
axiom To_of : forall x : t. to (of x) = x
axiom Of_to : forall y : u. of (to y) = y
......@@ -392,7 +393,7 @@ and that drinks, cigars and pets are all associated bijectively to persons:
Next we need a way to state that a person lives next to another. We
first define a predicate \texttt{leftof} over two houses.
\begin{verbatim}
logic leftof (h1 h2 : house) =
predicate leftof (h1 h2 : house) =
match h1, h2 with
| H1, H2
| H2, H3
......@@ -406,10 +407,10 @@ for the four positive cases and a universal pattern for the remaining
21 cases. It is then immediate to define a \texttt{neighbour}
predicate over two houses, which completes theory \texttt{Einstein}.
\begin{verbatim}
logic rightof (h1 h2 : house) =
predicate rightof (h1 h2 : house) =
leftof h2 h1
logic neighbour (h1 h2 : house) =
leftof h1 h2 or rightof h1 h2
predicate neighbour (h1 h2 : house) =
leftof h1 h2 \/ rightof h1 h2
end
\end{verbatim}
......
doc/syntaxref.tex
View file @ dba92e2e
......@@ -105,8 +105,8 @@ associativities, from lowest to greatest priority:
\texttt{if then else} / \texttt{let in} & -- \\
label & -- \\
\texttt{->} / \texttt{<->} & right \\
\texttt{or} / \verb!||! & right \\
\texttt{and} / \verb!&&! & right \\
\verb!\/! / \verb!||! & right \\
\verb|/\| / \verb!&&! & right \\
\texttt{not} & -- \\
infix level 1 & left \\
infix level 2 & left \\
......
doc/term.bnf
View file @ dba92e2e
......@@ -6,7 +6,7 @@
| bang-op term ;
| term infix-op term ;
| term "[" term "]" ; brackets
| term "[" term infix-op-1 term "]" ; ternary brackets
| term "[" term "<-" term "]" ; ternary brackets
| lqualid term+ ; function application
| "if" formula "then" term ;
"else" term ; conditional
......@@ -15,7 +15,7 @@
| "match" term ("," term)* "with" ;
("|" term-case)+ "end" ; pattern matching
| "(" term ("," term)+ ")" ; tuple
| "{|" field-value+ "|}" ; record
| "{|" field-value+ "|}" ; record
| term "." lqualid ; field access
| "{|" term "with" field-value+ "|}" ; field update
| term ":" type ; cast
......@@ -32,5 +32,5 @@
| "(" pattern ")" ; parentheses
| pattern "as" lident ; binding
\
field-value ::= lqualid "=" term
\end{syntax}
\ No newline at end of file
field-value ::= lqualid "=" term ";"
\end{syntax}
doc/theory.bnf
View file @ dba92e2e
\begin{syntax}
theory ::= "theory" uident label* decl* "end"
\
decl ::= "type" type-decl ("with" type-decl)* ;
| "logic" logic-decl ("with" logic-decl)* ;
decl ::= "type" type-decl ("with" type-decl)* ;
| "function" function-decl ("with" logic-decl)* ;
| "predicate" predicate-decl ("with" logic-decl)* ;
| "inductive" inductive-decl ("with" inductive-decl)* ;
| "axiom" ident ":" formula ;
| "lemma" ident ":" formula ;
......@@ -22,9 +23,13 @@
\
record-field ::= lident label* ":" type
\
logic-decl ::= lident label* type-param* ":" type ;
| lident label* type-param* ":" type "=" term ;
| lident label* type-param* ;
logic-decl ::= function-decl ;
| predicate-decl
\
function-decl ::= lident label* type-param* ":" type ;
| lident label* type-param* ":" type "=" term
\
predicate-decl ::= lident label* type-param* ;
| lident label* type-param* "=" formula
\
type-param ::= "'" lident ;
......@@ -45,7 +50,8 @@
subst ::= "with" ("," subst-elt)+
\
subst-elt ::= "type" lqualid "=" lqualid ;
| "logic" lqualid "=" lqualid ;
| "function" lqualid "=" lqualid ;
| "predicate" lqualid "=" lqualid ;
| "namespace" (uqualid | ".") "=" (uqualid | ".") ;
| "lemma" uqualid ;
| "goal" uqualid ;
......
doc/whyml.tex
View file @ dba92e2e
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment