Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
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
113
Issues
113
List
Boards
Labels
Milestones
Merge Requests
13
Merge Requests
13
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
7c69ef9f
Commit
7c69ef9f
authored
Apr 12, 2018
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
ignore files generated by doc/extract_ocaml_code
parent
05ea6612
Changes
4
Hide whitespace changes
Inline
Sidebyside
Showing
4 changed files
with
42 additions
and
41 deletions
+42
41
.gitignore
.gitignore
+1
0
Makefile.in
Makefile.in
+6
6
doc/api.tex
doc/api.tex
+34
34
doc/extract_ocaml_code.ml
doc/extract_ocaml_code.ml
+1
1
No files found.
.gitignore
View file @
7c69ef9f
...
...
@@ 127,6 +127,7 @@ why3.conf
/doc/apidoc.tex
/doc/apidoc/
/doc/stdlibdoc/
/doc/*__*.ml
# /lib
/lib/why3cpulimit
...
...
Makefile.in
View file @
7c69ef9f
...
...
@@ 1825,13 +1825,13 @@ doc/bnf$(EXE): doc/bnf.mll
doc/extract_ocaml_code
:
doc/extract_ocaml_code.ml
$(OCAMLC)
str.cma
o
$@
$<
doc/logic_%.ml
:
examples/use_api/logic.ml doc/extract_ocaml_code
doc/logic_
_
%.ml
:
examples/use_api/logic.ml doc/extract_ocaml_code
doc/extract_ocaml_code examples/use_api/logic.ml
$*
doc
doc/whyconf_%.ml
:
src/driver/whyconf.ml doc/extract_ocaml_code
doc/whyconf_
_
%.ml
:
src/driver/whyconf.ml doc/extract_ocaml_code
doc/extract_ocaml_code src/driver/whyconf.ml
$*
doc
doc/call_provers_%.ml
:
src/driver/call_provers.ml doc/extract_ocaml_code
doc/call_provers_
_
%.ml
:
src/driver/call_provers.ml doc/extract_ocaml_code
doc/extract_ocaml_code src/driver/call_provers.ml
$*
doc
OCAMLCODE_LOGIC
=
opening printformula declarepropvars declarepropatoms
\
...
...
@@ 1845,9 +1845,9 @@ OCAMLCODE_LOGIC = opening printformula declarepropvars declarepropatoms \
OCAMLCODE_CALLPROVERS
=
proveranswer proverresult resourcelimit
OCAMLCODE
=
$(
addprefix
doc/logic_,
$(
addsuffix
.ml,
$(OCAMLCODE_LOGIC)
))
\
$(
addprefix
doc/call_provers_,
$(
addsuffix
.ml,
$(OCAMLCODE_CALLPROVERS)
))
\
doc/whyconf_provertype.ml
OCAMLCODE
=
$(
addprefix
doc/logic_
_
,
$(
addsuffix
.ml,
$(OCAMLCODE_LOGIC)
))
\
$(
addprefix
doc/call_provers_
_
,
$(
addsuffix
.ml,
$(OCAMLCODE_CALLPROVERS)
))
\
doc/whyconf_
_
provertype.ml
DOC
=
api glossary ide intro
exec
macros manpages
install
\
manual starting syntax syntaxref technical version whyml
\
...
...
doc/api.tex
View file @
7c69ef9f
...
...
@@ 24,7 +24,7 @@ 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
$
\mathit
{
true
}
\lor
\mathit
{
false
}$
.
\lstinputlisting
{
logic
_
opening.ml
}
\lstinputlisting
{
logic
_
_
opening.ml
}
The library uses the common type
\texttt
{
term
}
both for terms
(
\ie
expressions that produce a value of some particular type)
and formulas (
\ie
booleanvalued expressions).
...
...
@@ 35,7 +35,7 @@ and formulas (\ie booleanvalued expressions).
Such a formula can be printed using the module
\texttt
{
Pretty
}
providing prettyprinters.
\lstinputlisting
{
logic
_
printformula.ml
}
\lstinputlisting
{
logic
_
_
printformula.ml
}
Assuming the lines above are written in a file
\texttt
{
f.ml
}
, it can
be compiled using
...
...
@@ 50,12 +50,12 @@ formula 1 is: true \/ false
Let us 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.
\lstinputlisting
{
logic
_
declarepropvars.ml
}
\lstinputlisting
{
logic
_
_
declarepropvars.ml
}
The type
\texttt
{
lsymbol
}
is the type of function and predicate symbols (which
we call logic symbols for brevity). Then the atoms
$
A
$
and
$
B
$
must be built
by the general function for applying a predicate symbol to a list of terms.
Here we just need the empty list of arguments.
\lstinputlisting
{
logic
_
declarepropatoms.ml
}
\lstinputlisting
{
logic
_
_
declarepropatoms.ml
}
As expected, the output is as follows.
\begin{verbatim}
...
...
@@ 74,7 +74,7 @@ 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
$
\mathit
{
true
}
\lor
\mathit
{
false
}$
above, this is done as follows.
\lstinputlisting
{
logic
_
buildtask.ml
}
\lstinputlisting
{
logic
_
_
buildtask.ml
}
To make the formula a goal, we must give a name to it, here ``goal1''. A
goal name has type
\texttt
{
prsymbol
}
, for identifiers denoting
propositions in a theory or a task. Notice again that the concrete
...
...
@@ 86,12 +86,12 @@ Notice that lemmas are not allowed in tasks
and can only be used in theories.
Once a task is built, it can be printed.
\lstinputlisting
{
logic
_
printtask.ml
}
\lstinputlisting
{
logic
_
_
printtask.ml
}
The task for our second formula is a bit more complex to build, because
the variables A and B must be added as abstract (
\ie
not defined)
propositional symbols in the task.
\lstinputlisting
{
logic
_
buildtask2.ml
}
\lstinputlisting
{
logic
_
_
buildtask2.ml
}
Execution of our OCaml program now outputs:
\begin{verbatim}
...
...
@@ 117,44 +117,44 @@ file \texttt{why3.conf}, as it was built using the \texttt{why3config}
command line tool or the
\textsf
{
Detect Provers
}
menu of the graphical
IDE. The following API calls allow to access the content of this
configuration file.
\lstinputlisting
{
logic
_
getconf.ml
}
\lstinputlisting
{
logic
_
_
getconf.ml
}
The type
\texttt
{
'a Whyconf.Mprover.t
}
is a map indexed by provers. A
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
}
:
\lstinputlisting
{
whyconf
_
provertype.ml
}
\lstinputlisting
{
whyconf
_
_
provertype.ml
}
The map
\texttt
{
provers
}
provides the set of existing provers.
In the following, we directly
attempt to access a prover named ``AltErgo'', any version.
\lstinputlisting
{
logic
_
getanyaltergo.ml
}
\lstinputlisting
{
logic
_
_
getanyaltergo.ml
}
We could also get a specific version with :
\lstinputlisting
{
logic
_
getaltergo200.ml
}
\lstinputlisting
{
logic
_
_
getaltergo200.ml
}
The next step is to obtain the driver associated to this prover. A
driver typically depends on the standard theories so these should be
loaded first.
\lstinputlisting
{
logic
_
getdriver.ml
}
\lstinputlisting
{
logic
_
_
getdriver.ml
}
We are now ready to call the prover on the tasks. This is done by a
function call that launches the external executable and waits for its
termination. Here is a simple way to proceed:
\lstinputlisting
{
logic
_
callprover.ml
}
\lstinputlisting
{
logic
_
_
callprover.ml
}
This way to call a prover is in general too naive, since it may never
return if the prover runs without time limit. The function
\texttt
{
prove
\_
task
}
has an optional parameter
\texttt
{
limit
}
, a record defined
in module
\texttt
{
Call
\_
provers
}
:
\lstinputlisting
{
call
_
provers
_
resourcelimit.ml
}
\lstinputlisting
{
call
_
provers
_
_
resourcelimit.ml
}
where the field
\texttt
{
limit
\_
time
}
is the maximum allowed running time in seconds,
and
\texttt
{
limit
\_
mem
}
is the maximum allowed memory in megabytes. The type
\texttt
{
prover
\_
result
}
is a record defined in module
\texttt
{
Call
\_
provers
}
:
\lstinputlisting
{
call
_
provers
_
proverresult.ml
}
\lstinputlisting
{
call
_
provers
_
_
proverresult.ml
}
with in particular the fields:
\begin{itemize}
\item
\texttt
{
pr
\_
answer
}
: the prover answer, explained below;
\item
\texttt
{
pr
\_
time
}
: the time taken by the prover, in seconds.
\end{itemize}
A
\texttt
{
pr
\_
answer
}
is the sum type defined in module
\texttt
{
Call
\_
provers
}
:
\lstinputlisting
{
call
_
provers
_
proveranswer.ml
}
\lstinputlisting
{
call
_
provers
_
_
proveranswer.ml
}
corresponding to these kinds of answers:
\begin{itemize}
\item
\texttt
{
Valid
}
: the task is valid according to the prover.
...
...
@@ 173,7 +173,7 @@ corresponding to these kinds of answers:
\end{itemize}
Here is thus another way of calling the AltErgo prover, on our second
task.
\lstinputlisting
{
logic
_
calltimelimit.ml
}
\lstinputlisting
{
logic
_
_
calltimelimit.ml
}
The output of our program is now as follows.
\begin{verbatim}
On task 1, altergo answers Valid (0.01s)
...
...
@@ 190,29 +190,29 @@ Here is the way we build the formula $2+2=4$. The main difficulty is to
access the internal identifier for addition: it must be retrieved from
the standard theory
\texttt
{
Int
}
of the file
\texttt
{
int.why
}
(see
Chap~
\ref
{
sec:library
}
).
\lstinputlisting
{
logic
_
buildfmla.ml
}
\lstinputlisting
{
logic
_
_
buildfmla.ml
}
An important point to notice as that when building the application of
$
+
$
to the arguments, it is checked that the types are correct. Indeed
the constructor
\texttt
{
t
\_
app
\_
infer
}
infers the type of the resulting
term. One could also provide the expected type as follows.
\lstinputlisting
{
logic
_
buildtermalt.ml
}
\lstinputlisting
{
logic
_
_
buildtermalt.ml
}
When building a task with this formula, we need to declare that we use
theory
\texttt
{
Int
}
:
\lstinputlisting
{
logic
_
buildtaskimport.ml
}
\lstinputlisting
{
logic
_
_
buildtaskimport.ml
}
\section
{
Building Quantified Formulas
}
To illustrate how to build quantified formulas, let us consider
the formula
$
\forall
x:int. x
*
x
\geq
0
$
. The first step is to
obtain the symbols from
\texttt
{
Int
}
.
\lstinputlisting
{
logic
_
quantfmla1.ml
}
\lstinputlisting
{
logic
_
_
quantfmla1.ml
}
The next step is to introduce the variable
$
x
$
with the type int.
\lstinputlisting
{
logic
_
quantfmla2.ml
}
\lstinputlisting
{
logic
_
_
quantfmla2.ml
}
The formula
$
x
*
x
\geq
0
$
is obtained as in the previous example.
\lstinputlisting
{
logic
_
quantfmla3.ml
}
\lstinputlisting
{
logic
_
_
quantfmla3.ml
}
To quantify on
$
x
$
, we use the appropriate smart constructor as follows.
\lstinputlisting
{
logic
_
quantfmla4.ml
}
\lstinputlisting
{
logic
_
_
quantfmla4.ml
}
\section
{
Building Theories
}
...
...
@@ 225,33 +225,33 @@ be done by a sequence of calls:
\end{itemize}
Creation of a theory named
\verb

My_theory

is done by
\lstinputlisting
{
logic
_
buildth1.ml
}
\lstinputlisting
{
logic
_
_
buildth1.ml
}
First let us add formula 1 above as a goal:
\lstinputlisting
{
logic
_
buildth2.ml
}
\lstinputlisting
{
logic
_
_
buildth2.ml
}
Note that we reused the goal identifier
\verb

goal_id1

that we
already defined to create task 1 above.
Adding formula 2 needs to add the declarations of predicate variables A
and B first:
\lstinputlisting
{
logic
_
buildth3.ml
}
\lstinputlisting
{
logic
_
_
buildth3.ml
}
Adding formula 3 is a bit more complex since it uses integers, thus it
requires to ``use'' the theory
\verb

int.Int

. Using a theory is
indeed not a primitive operation in the API: it must be done by a
combination of an ``export'' and the creation of a namespace. We
provide a helper function for that:
\lstinputlisting
{
logic
_
buildth4.ml
}
\lstinputlisting
{
logic
_
_
buildth4.ml
}
Addition of formula 3 is then
\lstinputlisting
{
logic
_
buildth5.ml
}
\lstinputlisting
{
logic
_
_
buildth5.ml
}
Addition of goal 4 is nothing more complex:
\lstinputlisting
{
logic
_
buildth6.ml
}
\lstinputlisting
{
logic
_
_
buildth6.ml
}
Finally, we close our theory under construction as follows.
\lstinputlisting
{
logic
_
buildth7.ml
}
\lstinputlisting
{
logic
_
_
buildth7.ml
}
We can inspect what we did by printing that theory:
\lstinputlisting
{
logic
_
printtheory.ml
}
\lstinputlisting
{
logic
_
_
printtheory.ml
}
which outputs
\begin{verbatim}
my new theory is as follows:
...
...
@@ 277,12 +277,12 @@ end
From a theory, one can compute at once all the proof tasks it contains
as follows:
\lstinputlisting
{
logic
_
splittheory.ml
}
\lstinputlisting
{
logic
_
_
splittheory.ml
}
Note that the tasks are returned in reverse order, so we reverse the
list above.
We can check our generated tasks by printing them:
\lstinputlisting
{
logic
_
printalltasks.ml
}
\lstinputlisting
{
logic
_
_
printalltasks.ml
}
One can run provers on those tasks exactly as we did above.
...
...
doc/extract_ocaml_code.ml
View file @
7c69ef9f
...
...
@@ 58,7 +58,7 @@ let search_begin () =
let
end_re
=
Str
.
regexp_string
(
"END{"
^
section
^
"}"
)
let
file_out
=
Filename
.
concat
output_dir
(
basename
^
"_"
^
section
^
ext
)
let
file_out
=
Filename
.
concat
output_dir
(
basename
^
"_
_
"
^
section
^
ext
)
let
ch_out
=
try
...
...
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