Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

library.tex 5.85 KB
Newer Older
1
\chapter{Standard Library}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
2 3
\label{chap:library}

4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
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 
23
\verb|-T| and a qualified theory name, for example:
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26 27
\begin{verbatim}
> why3 -T bool.Ite
theory Ite
  (* use BuiltIn *)
28

MARCHE Claude's avatar
MARCHE Claude committed
29
  (* use Bool *)
30 31

  function ite (b:bool) (x:'a) (y:'a) : 'a =
MARCHE Claude's avatar
MARCHE Claude committed
32 33 34 35 36 37 38
    match b with
    | True -> x
    | False -> y
    end
end
\end{verbatim}

39
In the following, for each library, we describe the main theories
40
defined in it.
MARCHE Claude's avatar
MARCHE Claude committed
41

42
\subsection{Library \texttt{bool}}
MARCHE Claude's avatar
MARCHE Claude committed
43 44 45

\begin{description}

46 47
\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|.
MARCHE Claude's avatar
MARCHE Claude committed
48

49
\item[Ite] provides the polymorphic if-then-else operator written as \verb|ite|.
MARCHE Claude's avatar
MARCHE Claude committed
50 51 52

\end{description}

53
\subsection{Library \texttt{int}}
MARCHE Claude's avatar
MARCHE Claude committed
54

MARCHE Claude's avatar
MARCHE Claude committed
55 56
\begin{description}

57 58
\item[Int] provides the basic operations \verb|+|, \verb|-|, and
  \verb|*|, and the comparison operators \verb|<|, \verb|>|, \verb|>=|, and
59
  \verb|<=|.
MARCHE Claude's avatar
MARCHE Claude committed
60

61
\item[Abs] provides the absolute value written as \verb|abs|.
MARCHE Claude's avatar
MARCHE Claude committed
62

63
\item[EuclideanDivision] defines division and modulo, where division rounds
64
  down, written as \verb|div| and \verb|mod|.
MARCHE Claude's avatar
MARCHE Claude committed
65

66
\item[ComputerDivision] defines division and modulo, where division rounds to
67
  zero, also written as \verb|div| and \verb|mod|.
MARCHE Claude's avatar
MARCHE Claude committed
68

69
\item[MinMax] provides \verb|min| and \verb|max| operators.
MARCHE Claude's avatar
MARCHE Claude committed
70 71 72

\end{description}

73 74 75 76
See the on-line web documentation for the other theories defined in the
\texttt{int} library.

\subsection{Library \texttt{real}}
MARCHE Claude's avatar
MARCHE Claude committed
77

MARCHE Claude's avatar
MARCHE Claude committed
78
\begin{description}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
79

80
\item[Real] provides basic operations \verb|+|, \verb|-|, \verb|*| and \verb|/|;
81
  comparison operators.
MARCHE Claude's avatar
docs  
MARCHE Claude committed
82

83
\item[RealInfix] provides basic operations with alternative syntax \verb|+.|,
84
  \verb|-.|, \verb|*.|, \verb|/.|, \verb|<.|, \verb|>.|, \verb|<=.|, and \verb|>=.|, to
85
  allow simultaneous use of integer and real operators.
MARCHE Claude's avatar
docs  
MARCHE Claude committed
86

87
\item[Abs] provides absolute value written as \verb|abs|.
MARCHE Claude's avatar
docs  
MARCHE Claude committed
88

89
\item[MinMax] provides \verb|min| and \verb|max| operators.
MARCHE Claude's avatar
docs  
MARCHE Claude committed
90

91
\item[FromInt] provides the operator \verb|from_int| to convert an integer to a real.
MARCHE Claude's avatar
MARCHE Claude committed
92

93
\item[Truncate] provides conversion operators from real to integers:
94
  \verb|truncate| rounds to 0, \verb|floor| rounds down, and
95
  \verb|ceil| rounds up.
MARCHE Claude's avatar
MARCHE Claude committed
96

97
\item[Square] provides operators \verb|sqr| and \verb|sqrt| for square and square root.
MARCHE Claude's avatar
MARCHE Claude committed
98

99
% \item[ExpLog] functions \verb|exp|, \verb|log|, \verb|log2|, and \verb|log10|.
MARCHE Claude's avatar
docs  
MARCHE Claude committed
100

101
% \item[PowerReal] function \verb|pow| with two real parameters.
MARCHE Claude's avatar
MARCHE Claude committed
102

103
% \item[PowerInt] function \verb|pow| with integer only exponents.
MARCHE Claude's avatar
docs  
MARCHE Claude committed
104

105 106
% \item[Trigonometry] functions \verb|cos|, \verb|sin|, \verb|tan|, and
%   \verb|atan|. Constant \verb|pi|.
MARCHE Claude's avatar
MARCHE Claude committed
107

108 109
% \item[Hyperbolic] functions \verb|cosh|, \verb|sinh|, \verb|tanh|,
%   \verb|acosh|, \verb|asinh|, \verb|atanh|.
MARCHE Claude's avatar
MARCHE Claude committed
110

111
% \item[Polar] functions \verb|hypot| and \verb|atan2|.
MARCHE Claude's avatar
MARCHE Claude committed
112

MARCHE Claude's avatar
MARCHE Claude committed
113 114
\end{description}

115 116 117 118 119
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}}
MARCHE Claude's avatar
MARCHE Claude committed
120 121

This library provides a theory of IEEE-754 floating-point numbers. It
122
is inspired by~\cite{ayad10ijcar}.
MARCHE Claude's avatar
MARCHE Claude committed
123

124
\subsection{Library \texttt{map}}
MARCHE Claude's avatar
MARCHE Claude committed
125

126 127 128 129
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.
MARCHE Claude's avatar
MARCHE Claude committed
130

131
\subsection{Library \texttt{option}}
MARCHE Claude's avatar
MARCHE Claude committed
132

133 134
This library provides the classical ML option type with constructors
\verb|None| and \verb|Some|.
MARCHE Claude's avatar
MARCHE Claude committed
135

136
\subsection{Library \texttt{list}}
MARCHE Claude's avatar
MARCHE Claude committed
137

138 139 140
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.
MARCHE Claude's avatar
MARCHE Claude committed
141

142 143
\section{Standard ML Modules}
\label{sec:mllibrary}
MARCHE Claude's avatar
MARCHE Claude committed
144

145 146 147
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.
MARCHE Claude's avatar
MARCHE Claude committed
148

149
\subsection{Library \texttt{ref}}
MARCHE Claude's avatar
MARCHE Claude committed
150

MARCHE Claude's avatar
MARCHE Claude committed
151 152

\begin{description}
153
\item[Ref] provides references \emph{i.e.} mutable variables:
154
  type \verb|ref 'a| and functions \verb|ref| for creation,
155 156 157
  \verb|(!)| for access, and \verb|(:=)| for mutation.
\item[Refint] provides additional functions \texttt{incr},
  \texttt{decr} and a few others, over integer references.
158 159
\end{description}

160
\subsection{Library \texttt{array}}
161 162

\begin{description}
163 164 165 166 167 168 169 170 171 172
\item[Array]polymorphic arrays (type \texttt{array 'a}, infix
  syntax $a[i]$ for access and $a[i] \leftarrow e$ for update,
  functions \texttt{length}, \texttt{make}, \texttt{append},
  \texttt{sub}, \texttt{copy}, \texttt{fill}, and \texttt{blit})
\item[ArraySorted] an array of integers is sorted
  (\verb|array_sorted_sub| and \verb|array_sorted|)
\item[ArrayEq] two arrays are identical
  (\verb|array_eq_sub| and \verb|array_eq|)
\item[ArrayPermut] two arrays are permutation of each other
  (\verb|permut_sub| and \verb|permut|)
173 174
\end{description}

175
\subsection{Standard Data Types}
176

177 178 179 180
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.
181

MARCHE Claude's avatar
docs  
MARCHE Claude committed
182 183 184 185 186 187

%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: