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
122
Issues
122
List
Boards
Labels
Service Desk
Milestones
Merge Requests
15
Merge Requests
15
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
681eeaf3
Commit
681eeaf3
authored
Mar 17, 2017
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
fix URL badly handled by hevea
parent
63b6b623
Changes
2
Hide whitespace changes
Inline
Sidebyside
Showing
2 changed files
with
35 additions
and
33 deletions
+35
33
doc/api.tex
doc/api.tex
+34
33
doc/version.tex.in
doc/version.tex.in
+1
0
No files found.
doc/api.tex
View file @
681eeaf3
...
...
@@ 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
...
...
@@ 291,9 +292,9 @@ 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
}
).
\begin{ocamlcode}
let two : Term.term =
let two : Term.term =
Term.t
_
const (Number.ConstInt (Number.int
_
const
_
dec "2"))
let four : Term.term =
let four : Term.term =
Term.t
_
const (Number.ConstInt (Number.int
_
const
_
dec "4"))
let int
_
theory : Theory.theory =
Env.read
_
theory env ["int"] "Int"
...
...
@@ 327,7 +328,7 @@ 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
}
.
\begin{ocamlcode}
let zero : Term.term =
let zero : Term.term =
Term.t
_
const (Number.ConstInt (Number.int
_
const
_
dec "0"))
let mult
_
symbol : Term.lsymbol =
Theory.ns
_
find
_
ls int
_
theory.Theory.th
_
export ["infix *"]
...
...
@@ 362,14 +363,14 @@ be done by a sequence of calls:
Creation of a theory named
\verb

My_theory

is done by
\begin{ocamlcode}
let my
_
theory : Theory.theory
_
uc =
let my
_
theory : Theory.theory
_
uc =
Theory.create
_
theory (Ident.id
_
fresh "My
_
theory")
\end{ocamlcode}
First let us add formula 1 above as a goal:
\begin{ocamlcode}
let decl
_
goal1 : Decl.decl =
Decl.create
_
prop
_
decl Decl.Pgoal goal
_
id1 fmla1
Decl.create
_
prop
_
decl Decl.Pgoal goal
_
id1 fmla1
let my
_
theory : Theory.theory
_
uc =
Theory.add
_
decl my
_
theory decl
_
goal1
\end{ocamlcode}
...
...
@@ 379,12 +380,12 @@ already defined to create task 1 above.
Adding formula 2 needs to add the declarations of predicate variables A
and B first:
\begin{ocamlcode}
let my
_
theory : Theory.theory
_
uc =
Theory.add
_
param
_
decl my
_
theory prop
_
var
_
A
let my
_
theory : Theory.theory
_
uc =
Theory.add
_
param
_
decl my
_
theory prop
_
var
_
B
let my
_
theory : Theory.theory
_
uc =
Theory.add
_
param
_
decl my
_
theory prop
_
var
_
A
let my
_
theory : Theory.theory
_
uc =
Theory.add
_
param
_
decl my
_
theory prop
_
var
_
B
let decl
_
goal2 : Decl.decl =
Decl.create
_
prop
_
decl Decl.Pgoal goal
_
id2 fmla2
Decl.create
_
prop
_
decl Decl.Pgoal goal
_
id2 fmla2
let my
_
theory : Theory.theory
_
uc = Theory.add
_
decl my
_
theory decl
_
goal2
\end{ocamlcode}
...
...
@@ 395,33 +396,33 @@ combination of an ``export'' and the creation of a namespace. We
provide a helper function for that:
\begin{ocamlcode}
(* [use th1 th2] insert the equivalent of a "use import th2" in
theory th1 under construction *)
let use th1 th2 =
let name = th2.Theory.th
_
name in
Theory.close
_
namespace
(Theory.use
_
export
theory th1 under construction *)
let use th1 th2 =
let name = th2.Theory.th
_
name in
Theory.close
_
namespace
(Theory.use
_
export
(Theory.open
_
namespace th1 name.Ident.id
_
string) th2) true
\end{ocamlcode}
Addition of formula 3 is then
\begin{ocamlcode}
let my
_
theory : Theory.theory
_
uc = use my
_
theory int
_
theory
let decl
_
goal3 : Decl.decl =
let decl
_
goal3 : Decl.decl =
Decl.create
_
prop
_
decl Decl.Pgoal goal
_
id3 fmla3
let my
_
theory : Theory.theory
_
uc =
Theory.add
_
decl my
_
theory decl
_
goal3
let my
_
theory : Theory.theory
_
uc =
Theory.add
_
decl my
_
theory decl
_
goal3
\end{ocamlcode}
Addition of goal 4 is nothing more complex:
\begin{ocamlcode}
let decl
_
goal4 : Decl.decl =
let decl
_
goal4 : Decl.decl =
Decl.create
_
prop
_
decl Decl.Pgoal goal
_
id4 fmla4
let my
_
theory :
Theory.theory
_
uc = Theory.add
_
decl my
_
theory decl
_
goal4
let my
_
theory :
Theory.theory
_
uc = Theory.add
_
decl my
_
theory decl
_
goal4
\end{ocamlcode}
Finally, we close our theory under construction as follows.
\begin{ocamlcode}
let my
_
theory : Theory.theory = Theory.close
_
theory my
_
theory
let my
_
theory : Theory.theory = Theory.close
_
theory my
_
theory
\end{ocamlcode}
We can inspect what we did by printing that theory:
...
...
@@ 433,19 +434,19 @@ which outputs
theory is:
theory My
_
theory
(* use BuiltIn *)
goal goal1 : true
\/
false
predicate A
predicate B
goal goal2 : A /
\
B > A
(* use int.Int *)
goal goal3 : (2 + 2) = 4
goal goal4 : forall x:int. (x * x) >= 0
end
\end{verbatim}
...
...
@@ 453,7 +454,7 @@ end
From a theory, one can compute at once all the proof tasks it contains
as follows:
\begin{ocamlcode}
let my
_
tasks : Task.task list =
let my
_
tasks : Task.task list =
List.rev (Task.split
_
theory my
_
theory None None)
\end{ocamlcode}
Note that the tasks are returned in reverse order, so we reverse the
...
...
@@ 461,7 +462,7 @@ list above.
We can check our generated tasks by printing them:
\begin{ocamlcode}
let () =
let () =
printf "Tasks are:@.";
let
_
=
List.fold
_
left
...
...
doc/version.tex.in
View file @
681eeaf3
\newcommand{\whyversion}{@VERSION@}
\urldef{\urlapi}{\url}{http://why3.lri.fr/api@VERSION@/}
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