Skip to content
GitLab
Explore
Sign in
Register
Primary navigation
Search or go to…
Project
W
why3
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
GitLab community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Nils Fitinghoff
why3
Commits
5519abf1
Commit
5519abf1
authored
7 years ago
by
Guillaume Melquiond
Browse files
Options
Downloads
Patches
Plain Diff
Uniformize Sec. vs Section.
parent
c15adff5
No related branches found
No related tags found
No related merge requests found
Changes
3
Show whitespace changes
Inline
Side-by-side
Showing
3 changed files
doc/install.tex
+3
-3
3 additions, 3 deletions
doc/install.tex
doc/syntaxref.tex
+1
-1
1 addition, 1 deletion
doc/syntaxref.tex
doc/whyml.tex
+1
-1
1 addition, 1 deletion
doc/whyml.tex
with
5 additions
and
5 deletions
doc/install.tex
+
3
−
3
View file @
5519abf1
...
...
@@ -12,7 +12,7 @@ package manager. It is as simple as
\begin{verbatim}
> opam install why3
\end{verbatim}
Then jump to Sec
.
~
\ref
{
provers
}
to install external provers.
Then jump to Sec
tion
~
\ref
{
provers
}
to install external provers.
\subsection
{
Installation Instructions from Source Distribution
}
...
...
@@ -85,7 +85,7 @@ make install
\end{verbatim}
Installation can be tested as follows:
\begin{enumerate}
\item
install some external provers (see
~
Sec
.
~
\ref
{
provers
}
below)
\item
install some external provers (see
Sec
tion
~
\ref
{
provers
}
below)
\item
run
\verb
|
why3 config --detect
|
\item
run some examples from the distribution,
\eg
you should
obtain the following (provided the required provers are installed on
...
...
@@ -137,7 +137,7 @@ have to run the following command:
> why
3
config
--
detect
\end
{
verbatim
}
It scans your
\texttt
{
PATH
}
for provers and updates your configuration
file
(
see Sec
.
~
\ref
{
sec:why
3
config
}
)
accordingly.
file
(
see Sec
tion
~
\ref
{
sec:why
3
config
}
)
accordingly.
\subsection
{
Multiple Versions of the Same Prover
}
...
...
This diff is collapsed.
Click to expand it.
doc/syntaxref.tex
+
1
−
1
View file @
5519abf1
...
...
@@ -733,7 +733,7 @@ indexed by 63-bit integers are imported as follows:
\end{whycode}
In particular, the types and operations from these modules are mapped
to native OCaml's types and operations when
\why
code is extracted to
OCaml (see Sec
.
~
\ref
{
sec:extract
}
).
OCaml (see Sec
tion
~
\ref
{
sec:extract
}
).
%%% Local Variables:
%%% mode: latex
...
...
This diff is collapsed.
Click to expand it.
doc/whyml.tex
+
1
−
1
View file @
5519abf1
...
...
@@ -56,7 +56,7 @@ See Chapter~\ref{chap:manpages} for more details regarding command lines.
\medskip
As an introduction to
\whyml
, we use a small logical puzzle
(Sec
.
~
\ref
{
sec:Einstein
}
) and then the five problems from the VSTTE
(Sec
tion
~
\ref
{
sec:Einstein
}
) and then the five problems from the VSTTE
2010 verification competition~
\cite
{
vstte10comp
}
.
The source code for all these examples is contained in
\why
's
distribution, in sub-directory
\texttt
{
examples/
}
. Look for files
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment