\chapter{Standard Library} \label{chap:library} 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 theory Ite (* use BuiltIn *) (* use Bool *) function ite (b:bool) (x:'a) (y:'a) : 'a = match b with | True -> x | False -> y end end \end{verbatim} In the following, for each library, we describe the main theories defined in it. \subsection{Library \texttt{bool}} \begin{description} \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] provides the polymorphic if-then-else operator written as \verb|ite|. \end{description} \subsection{Library \texttt{int}} \begin{description} \item[Int] provides the basic operations \verb|+|, \verb|-|, and \verb|*|, and the comparison operators \verb|<|, \verb|>|, \verb|>=|, and \verb|<=|. \item[Abs] provides the absolute value written as \verb|abs|. \item[EuclideanDivision] defines division and modulo, where division rounds down, written as \verb|div| and \verb|mod|. \item[ComputerDivision] defines division and modulo, where division rounds to zero, also written as \verb|div| and \verb|mod|. \item[MinMax] provides \verb|min| and \verb|max| operators. \end{description} See the on-line web documentation for the other theories defined in the \texttt{int} library. \subsection{Library \texttt{real}} \begin{description} \item[Real] provides basic operations \verb|+|, \verb|-|, \verb|*| and \verb|/|; comparison operators. \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] provides absolute value written as \verb|abs|. \item[MinMax] provides \verb|min| and \verb|max| operators. \item[FromInt] provides the operator \verb|from_int| to convert an integer to a real. \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] 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[PowerReal] function \verb|pow| with two real parameters. % \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[Hyperbolic] functions \verb|cosh|, \verb|sinh|, \verb|tanh|, % \verb|acosh|, \verb|asinh|, \verb|atanh|. % \item[Polar] functions \verb|hypot| and \verb|atan2|. \end{description} 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}. \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. \subsection{Library \texttt{option}} This library provides the classical ML option type with constructors \verb|None| and \verb|Some|. \subsection{Library \texttt{list}} 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. \section{Standard ML Modules} \label{sec:mllibrary} 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. \subsection{Library \texttt{ref}} \begin{description} \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] provides additional functions \texttt{incr}, \texttt{decr} and a few others, over integer references. \end{description} \subsection{Library \texttt{array}} \begin{description} \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|) \end{description} \subsection{Standard Data Types} 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. %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: