Skip to content

GitLab

why3
why3
Commit bcae786c authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Doc: standard library updated, with ref to the URL of the on-line 

doc generated by why3doc
parent c854f2d9
Hide whitespace changes
Inline Side-by-side
Showing with 98 additions and 149 deletions
ROADMAP
View file @ bcae786c
......@@ -85,14 +85,21 @@
- also: BTS 13736
https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* Documentation
- (ANDREI) make the glossary available
- (CLAUDE) revoir documentation du smoke detector
- (CLAUDE) complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
* detect editors
*** check if coqide and also emacs/proof-general is installed
* deplacer option -bench de why3replayer dans une commande de why3session
* IDE
** todo: run detection immediately at start up if conf file absent or
outdated. should become doable with the new Session module
......@@ -104,9 +111,6 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* (JCF) reject global "val"s in typing environment for logic decls.
* (CLAUDE) complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
==================== Roadmap for release 0.72 ========================
......@@ -175,11 +179,6 @@ See manual Section xx
install.tex:179:% \todo{que devient l'option -to-known-prover de why3session ?
manpages.tex:790:% \todo{A adapter en fonction de la decision sur l'upgrade de prover}
library.tex:8:\todo{Plutot la version produite avec why3doc}
library.tex:42:\section{Library \texttt{int}} \todo{Completer}
library.tex:120:\section{Library \texttt{array}} \todo{Mettre a jour}
library.tex:224:\section{Library \texttt{string}} \todo{Detailler}
manpages.tex:15:\item[\texttt{why3bench}] produces benchmarks \todo{obsolete ?}
manpages.tex:809:\section{The \texttt{why3doc} tool} \todo{Documenter}
......@@ -190,8 +189,6 @@ See manual Section xx
ses realisations ne pas oublier de dire que les dependances avec le
.why ou .mlw: ne sera pas vérifié
- (CLAUDE) revoir documentation du smoke detector
- DONE Documenter l'utilisation de plusieurs versions du meme
prouveur comme CVC3 et Z3
......
doc/library.tex
View file @ bcae786c
\chapter{Standard Library: Why3 Theories}
\chapter{Standard Library}
\label{chap:library}
We provide here a short description of logic symbols defined in the
standard library. Only the most general-purpose ones are
described. For more details, one should directly read the
corresponding file,
\todo{Plutot la version produite avec why3doc}
or alternatively, use the \verb|why3| with option
This chapter provides a short description of the contents of \why
standard library. It contains both standard logic theories, described
in Section~\ref{sec:stdlib}, and standard ML modules, described in
Section~\ref{sec:mllibrary}.
Only a rough introduction of the theories and modules is given
here. For detailed information, one should refer to the on-line
documentation automatically generated from the actual sources,
available at \url{http://why3.lri.fr/stdlib/}.
\section{Standard Theories}
\label{sec:stdlib}
We present the most important theories here, see the URL above for the
others.
Notice there is an alternative way to explore the contents of a
library, using the \verb|why3| command with option
\verb|-T| and a qualified theory name, for example:
\begin{verbatim}
> why3 -T bool.Ite
......@@ -23,160 +36,128 @@ theory Ite
end
\end{verbatim}
In the following, for each library, we describe the (main) symbols
In the following, for each library, we describe the main theories
defined in it.
\section{Library \texttt{bool}}
\subsection{Library \texttt{bool}}
\begin{description}
\item[Bool] boolean data type \verb|bool| with constructors \verb|True| and
\verb|False|; operations \verb|andb|, \verb|orb|, \verb|xorb|, \verb|notb|.
\item[Bool] provides the Boolean data type \verb|bool| with
constructors \verb|True| and \verb|False|; and operations \verb|andb|, \verb|orb|, \verb|xorb|, \verb|notb|.
\item[Ite] polymorphic if-then-else operator written as \verb|ite|.
\item[Ite] provides the polymorphic if-then-else operator written as \verb|ite|.
\end{description}
\section{Library \texttt{int}}
\todo{Completer}
\subsection{Library \texttt{int}}
\begin{description}
\item[Int] basic operations \verb|+|, \verb|-| and \verb|*|; comparison
operators \verb|<|, \verb|>|, \verb|>=| and \verb|<=|.
\item[Int] provides the basic operations \verb|+|, \verb|-| and
\verb|*|; and comparison operators \verb|<|, \verb|>|, \verb|>=| and
\verb|<=|.
\item[Abs] absolute value written as \verb|abs|.
\item[Abs] provides the absolute value written as \verb|abs|.
\item[EuclideanDivision] division and modulo, where division rounds
\item[EuclideanDivision] defines division and modulo, where division rounds
down, written as \verb|div| and \verb|mod|.
\item[ComputerDivision] division and modulo, where division rounds to
\item[ComputerDivision] defines division and modulo, where division rounds to
zero, also written as \verb|div| and \verb|mod|.
\item[MinMax] \verb|min| and \verb|max| operators.
\item[MinMax] provides \verb|min| and \verb|max| operators.
\end{description}
\section{Library \texttt{real}}
See the on-line web documentation for the other theories defined in the
\texttt{int} library.
\subsection{Library \texttt{real}}
\begin{description}
\item[Real] basic operations \verb|+|, \verb|-|, \verb|*| and \verb|/|;
\item[Real] provides basic operations \verb|+|, \verb|-|, \verb|*| and \verb|/|;
comparison operators.
\item[RealInfix] basic operations with alternative syntax \verb|+.|,
\item[RealInfix] provides basic operations with alternative syntax \verb|+.|,
\verb|-.|, \verb|*.|, \verb|/.|, \verb|<.|, \verb|>.|, \verb|<=.| and \verb|>=.|, to
allow simultaneous use of integer and real operators.
\item[Abs] absolute value written as \verb|abs|.
\item[Abs] provides absolute value written as \verb|abs|.
\item[MinMax] \verb|min| and \verb|max| operators.
\item[MinMax] provides \verb|min| and \verb|max| operators.
\item[FromInt] operator \verb|from_int| to convert an integer to a real.
\item[FromInt] provides the operator \verb|from_int| to convert an integer to a real.
\item[Truncate] conversion operators from real to integers:
\item[Truncate] provides conversion operators from real to integers:
\verb|truncate| rounds to 0, \verb|floor| rounds down and
\verb|ceil| rounds up.
\item[Square] operators \verb|sqr| and \verb|sqrt| for square and square root.
\item[Square] provides operators \verb|sqr| and \verb|sqrt| for square and square root.
\item[ExpLog] functions \verb|exp|, \verb|log|, \verb|log2|, and \verb|log10|.
% \item[ExpLog] functions \verb|exp|, \verb|log|, \verb|log2|, and \verb|log10|.
\item[PowerReal] function \verb|pow| with two real parameters.
% \item[PowerReal] function \verb|pow| with two real parameters.
\item[PowerInt] function \verb|pow| with integer only exponents.
% \item[PowerInt] function \verb|pow| with integer only exponents.
\item[Trigonometry] functions \verb|cos|, \verb|sin|, \verb|tan|, and
\verb|atan|. Constant \verb|pi|.
% \item[Trigonometry] functions \verb|cos|, \verb|sin|, \verb|tan|, and
% \verb|atan|. Constant \verb|pi|.
\item[Hyperbolic] functions \verb|cosh|, \verb|sinh|, \verb|tanh|,
\verb|acosh|, \verb|asinh|, \verb|atanh|.
% \item[Hyperbolic] functions \verb|cosh|, \verb|sinh|, \verb|tanh|,
% \verb|acosh|, \verb|asinh|, \verb|atanh|.
\item[Polar] functions \verb|hypot| and \verb|atan2|.
% \item[Polar] functions \verb|hypot| and \verb|atan2|.
\end{description}
\section{Library \texttt{floating\_point}}
See the on-line web documentation for the other theories defined in the
\texttt{real} library, such exponential, logarithm, power,
trigonometric functions.
\subsection{Library \texttt{floating\_point}}
This library provides a theory of IEEE-754 floating-point numbers. It
is inspired by~\cite{ayad10ijcar}.
\begin{description}
\item[Rounding] type \verb|mode| with 5 constants
\verb|NearestTiesToEven|, \verb|ToZero|, \verb|Up|, \verb|Down| and
\verb|NearTiesToAway|.
\item[SpecialValues] handling of infinities and NaN.
\item[GenFloat] generic floats parameterized by the maximal
representable number. Functions \verb|round|, \verb|value|,
\verb|exact|, \verb|model|, predicate \verb|no_overflow|.
\item[Single] instance of GenFloat for 32-bits single precision numbers.
\item[Double] instance of GenFloat for 64-bits double precision numbers.
\end{description}
\subsection{Library \texttt{map}}
This library provides the data type of purely applicative maps. It is
polymorphic both in the index type and the contents. There are also a
few theories and operators specialized to maps indexed by integers,
such as the sorted predicate, permutation, etc.
\section{Library \texttt{array}}
\subsection{Library \texttt{option}}
\todo{Mettre a jour}
This library provides the classical ML option type with constructors
\verb|None| and \verb|Some|.
\begin{description}
\subsection{Library \texttt{list}}
\item[Array] polymorphic arrays, a.k.a maps. Type \verb|t|
parameterized by both the type of indices and the type of
data. Functions \verb|get| and \verb|set| to access and update
arrays. Function \verb|create_const| to produce an array initialized
by a given constant.
This library provides the classical ML type of polymorphic lists, with
constructors \verb|Nil| and \verb|Cons|. Most of the classical list
operators are provided in separate theories.
\item[ArrayLength] arrays indexed by integers and holding their
length. Function \verb|length|.
\section{Standard ML Modules}
\label{sec:mllibrary}
\item[ArrayRich] additional functions on arrays indexed by
integers. Functions \verb|sub| and \verb|app| to extract a sub-array
and append arrays.
The standard ML modules provided allow to write imperative
programs. The two main modules are the one providing ML references,
and the one providing arrays.
\end{description}
\subsection{Library \texttt{ref}}
\section{Library \texttt{option}}
\begin{description}
\item[Option] data type \verb|option 'a| with constructors \verb|None| and
\verb|Some|.
\end{description}
\section{Library \texttt{list}}
\begin{description}
\item[List] data type \verb|list 'a| with constructors \verb|Nil| and
\verb|Cons|.
\item[Length] function \verb|length|
\item[Mem] function \verb|mem| for testing for list membership.
\item[Nth] function \verb|nth| for extract the $n$-th element.
\item[HdTl] functions \verb|hd| and \verb|tl|.
\item[Append] function \verb|append|, concatenation of lists.
\item[Reverse] function \verb|reverse| for list reversal.
\item[Sorted] predicate \verb|sorted| for lists of integers.
\item[NumOcc] number of occurrences in a list.
\item[Permut] list permutations.
\item[Induction] structural induction on lists.
\item[Map] list map operator.
\end{description}
\chapter{Standard Library: Why3ML Modules}
\label{chap:mllibrary}
\section{Library \texttt{ref}}
\begin{description}
\item[Ref] references \emph{i.e.} mutable variables:
\item[Ref] provides references \emph{i.e.} mutable variables:
type \verb|ref 'a| and functions \verb|ref| for creation,
\verb|(!)| for access, and \verb|(:=)| for mutation
\item[Refint] references with additional functions \texttt{incr} and
\texttt{decr} over integer references
\verb|(!)| for access, and \verb|(:=)| for mutation.
\item[Refint] provides additional functions \texttt{incr},
\texttt{decr} and a few others, over integer references.
\end{description}
\section{Library \texttt{array}}
\subsection{Library \texttt{array}}
\begin{description}
\item[Array]polymorphic arrays (type \texttt{array 'a}, infix
......@@ -191,42 +172,13 @@ is inspired by~\cite{ayad10ijcar}.
(\verb|permut_sub| and \verb|permut|)
\end{description}
\section{Library \texttt{queue}}
\begin{description}
\item[Queue] polymorphic mutable queues (type \texttt{t 'a} and
functions \texttt{create}, \texttt{push}, \texttt{pop},
\texttt{top}, \texttt{clear}, \texttt{copy}, \texttt{is\_empty},
\texttt{length})
\end{description}
\section{Library \texttt{stack}}
\begin{description}
\item[Stack] polymorphic mutable stacks (type \texttt{t 'a} and
functions \texttt{create}, \texttt{push}, \texttt{pop},
\texttt{top}, \texttt{clear}, \texttt{copy}, \texttt{is\_empty},
\texttt{length})
\end{description}
\section{Library \texttt{hashtbl}}
\subsection{Standard Data Types}
\begin{description}
\item[Hashtbl] hash tables with monomorphic keys (type \texttt{key})
and polymorphic values (type \texttt{t 'a} of hash tables, syntax
$h[k]$ for access, functions \texttt{create}, \texttt{clear},
\texttt{add}, \texttt{mem}, \texttt{find}, \texttt{find\_all},
\texttt{copy}, \texttt{remove}, and \texttt{replace})
\end{description}
A few other classical data types are provided, such as queues (library
\texttt{queue}), stacks (library \texttt{stack}), hash tables (library
\texttt{hashtbl}), characters and strings (library \texttt{string}),
etc.
\section{Library \texttt{string}}
\todo{Detailler}
\begin{description}
\item[Char]
\item[String]
\end{description}
%%% Local Variables:
%%% mode: latex
......
doc/manpages.tex
View file @ bcae786c
......@@ -583,7 +583,7 @@ nothing. On the other hand if the proof is obsolete we mark it with an
For example, here are the session tree produced on the ``hello
proof'' example of Section~\ref{chap:starting}.
{\footnotesize
{\scriptsize
\begin{verbatim}
hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Alt-Ergo (0.93)
| `-Simplify (1.5.4)?
......
doc/manual.tex
View file @ bcae786c
......@@ -44,7 +44,7 @@
\begin{document}
\sloppy
\hbadness=1000
\hbadness=5000
\thispagestyle{empty}
......
doc/syntax.tex
View file @ bcae786c
......@@ -11,7 +11,7 @@ These declarations can be directly written in the theory or taken from
existing theories. The base logic of \why is first-order
logic with polymorphic types.
\subsection{Example 1: lists}
\section{Example 1: lists}
The Figure~\ref{fig:tutorial1} contains an example of \why input
text, containing three theories. The first theory, \texttt{List},
......@@ -109,7 +109,7 @@ Note that the type signature of \lstinline{sorted} predicate does not
include the name of a parameter (see \texttt{l} in the definition
of \texttt{length}): it is unused and therefore optional.
\subsection{Example 1 (continued): lists and abstract orderings}
\section{Example 1 (continued): lists and abstract orderings}
In the previous section we have seen how a theory can reuse the
declarations of another theory, coming either from the same input
......@@ -294,7 +294,7 @@ written as:
However, since \why favours short theories over long and complex ones,
this feature is rarely used.
\subsection{Example 2: Einstein's problem}
\section{Example 2: Einstein's problem}
\index{Einstein's logic problem}
We now consider another, slightly more complex example: how to use \why
......
doc/whyml.tex
View file @ bcae786c
......@@ -86,7 +86,7 @@ The additional keyword \texttt{module} means that we are looking for
and \texttt{array.mlw} here), instead of \texttt{.why} files.
Modules \texttt{Ref} and \texttt{Array} respectively provide a type
\texttt{ref 'a} for references and a type \texttt{array 'a} for
arrays (see Chapter~\ref{chap:mllibrary}), together with useful
arrays (see Section~\ref{sec:mllibrary}), together with useful
operations and traditional syntax.
We are now in position to define a program function
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment