Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
35cff9e2
Commit
35cff9e2
authored
Feb 01, 2013
by
Guillaume Melquiond
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fix some typos in documentation.
parent
4845badd
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
25 additions
and
27 deletions
+25
-27
doc/api.tex
doc/api.tex
+15
-17
doc/technical.tex
doc/technical.tex
+10
-10
No files found.
doc/api.tex
View file @
35cff9e2
...
...
@@ -11,14 +11,14 @@ at URL~\url{http://why3.lri.fr/api/}.
We assume the reader has a fair knowledge of the OCaml
language. Notice that the
\why
library must be installed, see
Section~
\ref
{
sec:installlib
}
. The OCaml code given below is available in
the source distribution as
\
url
{
examples/use
_
api/use
_
api.ml
}
.
the source distribution as
\
verb
|
examples/use_api/use_api.ml
|
.
\section
{
Building Propositional Formulas
}
The first step is to know how to build propositional formulas. The
module
\texttt
{
Term
}
gives a few functions for building these. Here is
a piece of OCaml code for building the formula
$
true
\lor
false
$
.
a piece of OCaml code for building the formula
$
\mathit
{
true
}
\lor
\mathit
{
false
}
$
.
\begin{ocamlcode}
(* opening the Why3 library *)
open Why3
...
...
@@ -55,7 +55,7 @@ Running the generated executable \texttt{f} results in the following output.
formula 1 is: true
\/
false
\end{verbatim}
Let
'
s now build a formula with propositional variables:
$
A
\land
B
Let
u
s now build a formula with propositional variables:
$
A
\land
B
\rightarrow
A
$
. Propositional variables must be declared first before
using them in formulas. This is done as follows.
\begin{ocamlcode}
...
...
@@ -87,12 +87,12 @@ when building those directly using library calls.
\section
{
Building Tasks
}
Let
'
s see how we can call a prover to prove a formula. As said in
Let
u
s see how we can call a prover to prove a formula. As said in
previous chapters, a prover must be given a task, so we need to build
tasks from our formulas. Task can be build incrementally from an empty
task by adding declaration to it, using the functions
\texttt
{
add
\_*\_
decl
}
of module
\texttt
{
Task
}
. For the formula
$
true
\lor
false
$
above, this is done as follows.
\texttt
{
add
\_*\_
decl
}
of module
\texttt
{
Task
}
. For the formula
$
\mathit
{
true
}
\lor
\mathit
{
false
}
$
above, this is done as follows.
\begin{ocamlcode}
let task1 : Task.task = None (* empty task *)
let goal
_
id1 : Decl.prsymbol =
...
...
@@ -106,10 +106,9 @@ propositions in a theory or a task. Notice again that the concrete
syntax of
\why
requires these symbols to be capitalized, but it is not
mandatory when using the library. The second argument of
\texttt
{
add
\_
prop
\_
decl
}
is the kind of the proposition:
\texttt
{
Paxiom
}
,
\texttt
{
Plemma
}
or
\texttt
{
Pgoal
}
(notice, however, that lemmas are not allowed in tasks
and can only be used in theories).
\texttt
{
Paxiom
}
,
\texttt
{
Plemma
}
or
\texttt
{
Pgoal
}
.
Notice that lemmas are not allowed in tasks
and can only be used in theories.
Once a task is built, it can be printed.
\begin{ocamlcode}
...
...
@@ -164,10 +163,9 @@ let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get
_
provers config
\end{ocamlcode}
The type
\texttt
{
'a Whyconf.Mprover.t
}
is a map indexed by provers. A
provers is a record with a name, a version and an alternative description
(if someone want to compare different command line options of the same
provers for example). It's definition is in the module
\texttt
{
Whyconf
}
:
prover is a record with a name, a version, and an alternative description
(to differentiate between various configurations of a given prover). Its
definition is in the module
\texttt
{
Whyconf
}
:
\begin{ocamlcode}
type prover =
{
prover
_
name : string; (* "Alt-Ergo" *)
...
...
@@ -355,7 +353,7 @@ let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux
We illustrate now how one can build theories. Building a theory must
be done by a sequence of calls:
\begin{itemize}
\item
creating a theory ``under construction'', of type
\verb
|
Theory.theory_uc
|
;
\item
creating a theory ``under construction'', of type
\verb
|
Theory.theory_uc
|
;
\item
adding declarations, one at a time ;
\item
closing the theory under construction, obtaining something of type
\verb
|
Theory.theory
|
.
\end{itemize}
...
...
@@ -366,7 +364,7 @@ let my_theory : Theory.theory_uc =
Theory.create
_
theory (Ident.id
_
fresh "My
_
theory")
\end{ocamlcode}
First let
'
s add the formula 1 above as a goal:
First let
u
s add the formula 1 above as a goal:
\begin{ocamlcode}
let decl
_
goal1 : Decl.decl =
Decl.create
_
prop
_
decl Decl.Pgoal goal
_
id1 fmla1
...
...
@@ -483,7 +481,7 @@ One can run provers on those tasks exactly as we did above.
\section
{
Proof sessions
}
See the example
\
url
{
examples/use
_
api/create
_
session.ml
}
of the distribution for
See the example
\
verb
|
examples/use_api/create_session.ml
|
of the distribution for
an illustration on how to manipulate proof sessions from an OCaml program.
...
...
doc/technical.tex
View file @
35cff9e2
...
...
@@ -98,16 +98,15 @@ name = "CoqIDE"
One can use a custom configuration file.
\texttt
{
why3config
}
and other
\texttt
{
why3
}
tools use priorities for which
user's configuration file to consider:
\begin{itemize}
and other
\texttt
{
why3
}
tools look for it in the following order:
\begin{enumerate}
\item
the file specified by the
\texttt
{
-C
}
or
\texttt
{
-
{}
-config
}
options,
\item
the file specified by the environment variable
\texttt
{
WHY3CONFIG
}
if set
.
\texttt
{
WHY3CONFIG
}
if set
,
\item
the file
\texttt
{
\$
HOME/.why3.conf
}
(
\texttt
{
\$
USERPROFILE/.why3.conf
}
under Windows) or, in the case of
local installation,
\texttt
{
why3.conf
}
in Why3 sources top directory.
\end{
itemiz
e}
\end{
enumerat
e}
If none of these files exists, a built-in default configuration is used.
The configuration file is a human-readable text file, which consists
...
...
@@ -121,15 +120,16 @@ the example, or it can be composed by a family name and one family
argument,
\texttt
{
prover
}
is one family name,
\texttt
{
coq
}
and
\texttt
{
alt-ergo
}
are the family argument.
Inside a section, one key can be associated with an integer (
\eg
{}
-555),
a boolean (true, false) or a string (
\eg
{}
"emacs"). One key can appear
only once except if its a multi-value key. The order of apparition of
the keys inside a section matter only for the multi-value key.
Sections contain associations
\texttt
{
key=value
}
. A value is either
an integer (
\eg
{}
-555), a boolean (true, false), or a string (
\eg
{}
"emacs"). Some specific keys can be attributed multiple values and are
thus allowed to occur several times inside a given section. In that
case, the relative order of these associations matter.
\section
{
Drivers of External Provers
}
\label
{
sec:drivers
}
The drivers of external provers are readable files, in
directory
Drivers of external provers are readable files from
directory
\texttt
{
drivers
}
. Experimented users can modify them to change the way
the external provers are called, in particular which transformations
are applied to goals.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment