Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
36c28017
Commit
36c28017
authored
Oct 10, 2013
by
MARCHE Claude
Browse files
Doc: fixed e.g. and i.e
parent
a7a6413b
Changes
8
Hide whitespace changes
Inline
Side-by-side
doc/intro.tex
View file @
36c28017
...
...
@@ -9,7 +9,7 @@ translates its input to a number of tasks, and dispatches these tasks
to external provers.
Essentially, a task is a sequence of premises followed by a goal
(
i.e.~
a
\emph
{
logical sequent
}
with exactly one formula in the
(
\ie
a
\emph
{
logical sequent
}
with exactly one formula in the
succedent). The language of tasks is based on first-order language
extended with
\begin{itemize}
...
...
doc/library.tex
View file @
36c28017
...
...
@@ -157,7 +157,7 @@ and the one providing arrays.
\begin{description}
\item
[Ref]
provides references
\e
mph
{
i.e.
}
mutable variables:
\item
[Ref]
provides references
,
\
i
e
mutable variables:
type
\verb
|
ref 'a
|
and functions
\verb
|
ref
|
for creation,
\verb
|
(!)
|
for access, and
\verb
|
(:=)
|
for mutation.
\item
[Refint]
provides additional functions
\texttt
{
incr
}
,
...
...
doc/manpages.tex
View file @
36c28017
...
...
@@ -72,7 +72,7 @@ This must be redone each time a new prover is installed.
The provers which
\why
attempts to detect are described in
the readable configuration file
\texttt
{
provers-detection-data.conf
}
of the
\why
data directory (
\eg
{}
of the
\why
data directory (
\eg
\texttt
{
/usr/local/share/why3
}
). Advanced users may try to modify this
file to add support for detection of other provers. (In that case,
please consider submitting a new prover configuration on the bug
...
...
@@ -82,11 +82,11 @@ The result of provers detection is stored in the user's
configuration file (
\verb
+
~/.why3.conf
+
or, in the case of local
installation,
\verb
+
why3.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.
\texttt
{
why3config
}
also detects the plugins installed in the
\why
plugins directory (
\eg
{}
\texttt
{
/usr/local/lib/why3/plugins
}
). A
plugins directory (
\eg
\texttt
{
/usr/local/lib/why3/plugins
}
). A
plugin must register itself as a parser, a transformation or a
printer, as explained in the corresponding section.
\index
{
plugin
}
...
...
@@ -123,7 +123,7 @@ input file. By default, such a file must be written either in \why language
(extension
\texttt
{
.why
}
) or in
\whyml
language (extension
\texttt
{
.mlw
}
).
However, a dynamically loaded
plugin can register a parser for some other format of logical problems,
\eg
{}
TPTP or SMT
lib
.
\eg
TPTP or SMT
-LIB
.
\index
{
why3@
\texttt
{
why3
}}
The
\texttt
{
why3
}
tool executes the following steps:
...
...
@@ -252,7 +252,7 @@ Additionally, a proof attempt can have the following attributes:
\item
[obsolete]
\index
{
obsolete!proof attempt
}
The prover associated to
that proof attempt has not been run on the current task, but on an
earlier version of that task. You need to replay the proof
attempt,
\e
mph
{
i.e.
}
run the prover with the current task of the proof
attempt,
\
i
e
run the prover with the current task of the proof
attempt, in order to update the answer of the prover and remove this
attribute.
\item
[archived]
\index
{
archived!proof attempt
}
The proof attempt is not useful
...
...
@@ -356,7 +356,7 @@ A copy of the tools already available in the left toolbar, plus:
\item
[Non-splitting transformation]
applies one of the available
transformations, as listed in Section~
\ref
{
sec:transformations
}
.
\item
[Splitting transformation]
is the same as above, but for
splitting transformations,
\e
mph
{
i.e.
}
those that can generate
splitting transformations,
\
i
e
those that can generate
several sub-goals.
\end{description}
...
...
doc/manual.tex
View file @
36c28017
...
...
@@ -21,7 +21,7 @@
\usepackage
{
listings
}
\usepackage
{
xspace
}
\
usepackage
{
hevea
}
\
input
{
./my
hevea
.sty
}
%BEGIN LATEX
\setulmarginsandblock
{
30mm
}{
30mm
}{
*
}
...
...
@@ -38,7 +38,7 @@
\setcounter
{
bottomnumber
}{
4
}
\setcounter
{
totalnumber
}{
8
}
\newstyle
{
table.lstframe
}{
width:100
\%
;border-width:1px;
}
%HEVEA
\newstyle{table.lstframe}{width:100\%;border-width:1px;}
% \usepackage[toc,nonumberlist]{glossaries}
% \makeglossaries
...
...
doc/starting.tex
View file @
36c28017
...
...
@@ -106,7 +106,7 @@ prover. On the contrary, the two other goals are not proved, they remain
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
prover,
\eg
Alt-Ergo, by clicking on the corresponding button. The
goal
$
G
_
3
$
should be proved now, but not
$
G
_
2
$
.
\subsection
{
Applying transformations
}
...
...
doc/syntax.tex
View file @
36c28017
...
...
@@ -125,7 +125,7 @@ declarations of another theory, coming either from the same input
text or from the library. Another way to referring to a theory is
by ``cloning''. A
\texttt
{
clone
}
declaration constructs a local
copy of the cloned theory, possibly instantiating some of its
abstract (
\
emph
{
i.e.
}
~
declared but not defined) symbols.
abstract (
\
ie
declared but not defined) symbols.
%BEGIN LATEX
Consider the continued example in Figure~
\ref
{
fig:tutorial2
}
.
...
...
@@ -194,7 +194,7 @@ use of it (see Section~\ref{sec:drivers}).
Notice an important difference between
\texttt
{
use
}
and
\texttt
{
clone
}
. If we
\texttt
{
use
}
a theory, say
\texttt
{
List
}
, twice (directly or indirectly:
\e
mph
{
e.g.
}
~
by
\texttt
{
List
}
, twice (directly or indirectly:
\e
g
by
making
\texttt
{
use
}
of both
\texttt
{
Length
}
and
\texttt
{
Sorted
}
), there is no duplication: there is
still only one type of lists and a unique pair
...
...
@@ -211,7 +211,7 @@ this time we use the abstract order on the values of type
Now, we can instantiate theory
\texttt
{
SortedGen
}
to any
ordered type, without having to retype the definition of
\texttt
{
sorted
}
. For example, theory
\texttt
{
SortedIntList
}
makes
\texttt
{
clone
}
of
\texttt
{
SortedGen
}
(
\
emph
{
i.e.
}
~
copies its
makes
\texttt
{
clone
}
of
\texttt
{
SortedGen
}
(
\
ie
copies its
declarations) substituting type
\texttt
{
int
}
for type
\texttt
{
O.t
}
of
\texttt
{
SortedGen
}
and the default order
on integers for predicate
\texttt
{
O.(<=)
}
.
\why
will
...
...
@@ -285,7 +285,7 @@ optional, if it is omitted, the name of the symbol is \texttt{List.$s$}.
\item
\texttt
{
use import List as L
}
--- every symbol
$
s
$
from
\texttt
{
List
}
is accessible under the name
\texttt
{
L.
$
s
$}
. It is also
accessible simply as
\texttt
{$
s
$}
, but only up to the end of the current
namespace,
\e
mph
{
e.g.
}
~
the current theory. If the current theory, that is the
namespace,
\e
g
the current theory. If the current theory, that is the
one making
\texttt
{
use
}
, is later used under the name
\texttt
{
T
}
,
the name of the symbol would be
\texttt
{
T.L.
$
s
$}
. (This is why we
could refer directly to the symbols of
\texttt
{
Order
}
in theory
...
...
doc/syntaxref.tex
View file @
36c28017
...
...
@@ -102,7 +102,7 @@ application is not allowed (rejected at typing).
\begin{center}
\framebox
{
\input
{
./type
_
bnf.tex
}}
\end{center}
Built-in types are
\texttt
{
int
}
,
\texttt
{
real
}
, and tuple types.
Note that the syntax for type
expressions notably differs from the usual ML syntax (
\e
mph
{
e.g.
}
the
expressions notably differs from the usual ML syntax (
\e
g
the
type of polymorphic lists is written
\texttt
{
list 'a
}
, not
\texttt
{
'a list
}
).
\paragraph
{
Formulas.
}
...
...
doc/technical.tex
View file @
36c28017
...
...
@@ -121,7 +121,7 @@ argument, \texttt{prover} is one family name, \texttt{coq} and
\texttt
{
alt-ergo
}
are the family argument.
Sections contain associations
\texttt
{
key=value
}
. A value is either
an integer (
\eg
{}
-555), a boolean (true, false), or a string (
\eg
{}
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.
...
...
@@ -140,7 +140,7 @@ are applied to goals.
\label
{
sec:transformations
}
Here is a quick documentation of provided transformations. We give
first the non-splitting ones,
\eg
{}
those which produce one goal as
first the non-splitting ones,
\eg
those which produce one goal as
result, and others which produces any number of goals.
Notice that the set of available transformations in your own
...
...
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