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

MARCHE Claude's avatar
MARCHE Claude committed
4
5
We provide here a short description of logic symbols defined in the
standard library. Only the most general-purpose ones are
MARCHE Claude's avatar
MARCHE Claude committed
6
described. For more details, one should directly read the
7
8
corresponding file, or alternatively, use the \verb|why3| with option
\verb|-T| and a qualified theory name, for example:
MARCHE Claude's avatar
MARCHE Claude committed
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
\begin{verbatim}
> why3 -T bool.Ite
theory Ite
  (* use BuiltIn *)
  
  (* use Bool *)
  
  logic ite (b:bool) (x:'a) (y:'a) : 'a =
    match b with
    | True -> x
    | False -> y
    end
end
\end{verbatim}

24
25
In the following, for each library, we describe the (main) symbols
defined in it.
MARCHE Claude's avatar
MARCHE Claude committed
26

MARCHE Claude's avatar
example    
MARCHE Claude committed
27
\section{Library \texttt{bool}}
MARCHE Claude's avatar
MARCHE Claude committed
28
29
30
31

\begin{description}

\item[Bool] boolean data type \verb|bool| with constructors \verb|True| and
32
  \verb|False|; operations \verb|andb|, \verb|orb|, \verb|xorb|, \verb|notb|.
MARCHE Claude's avatar
MARCHE Claude committed
33

34
\item[Ite] polymorphic if-then-else operator written as \verb|ite|.
MARCHE Claude's avatar
MARCHE Claude committed
35
36
37

\end{description}

MARCHE Claude's avatar
example    
MARCHE Claude committed
38
\section{Library \texttt{int}}
MARCHE Claude's avatar
MARCHE Claude committed
39
40
41

\begin{description}

42
\item[Int] basic operations \verb|+|, \verb|-| and \verb|*|; comparison
MARCHE Claude's avatar
MARCHE Claude committed
43
44
  operators \verb|<|, \verb|>|, \verb|>=| and \verb|<=|.

45
\item[Abs] absolute value written as \verb|abs|.
MARCHE Claude's avatar
MARCHE Claude committed
46
47

\item[EuclideanDivision] division and modulo, where division rounds
48
  down, written as \verb|div| and \verb|mod|.
MARCHE Claude's avatar
MARCHE Claude committed
49
50

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

53
\item[MinMax] \verb|min| and \verb|max| operators.
MARCHE Claude's avatar
MARCHE Claude committed
54
55
56

\end{description}

MARCHE Claude's avatar
example    
MARCHE Claude committed
57
\section{Library \texttt{real}}
MARCHE Claude's avatar
MARCHE Claude committed
58

MARCHE Claude's avatar
MARCHE Claude committed
59
\begin{description}
MARCHE Claude's avatar
docs    
MARCHE Claude committed
60

61
62
\item[Real] basic operations \verb|+|, \verb|-|, \verb|*| and \verb|/|;
  comparison operators.
MARCHE Claude's avatar
docs    
MARCHE Claude committed
63

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
72
\item[FromInt] operator \verb|from_int| to convert an integer to a real.
MARCHE Claude's avatar
MARCHE Claude committed
73

MARCHE Claude's avatar
MARCHE Claude committed
74
75
\item[Truncate] conversion operators from real to integers:
  \verb|truncate| rounds to 0, \verb|floor| rounds down and
76
  \verb|ceil| rounds up.
MARCHE Claude's avatar
MARCHE Claude committed
77

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

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

MARCHE Claude's avatar
MARCHE Claude committed
82
\item[Power] function \verb|pow| with two real parameters.
MARCHE Claude's avatar
docs    
MARCHE Claude committed
83

MARCHE Claude's avatar
MARCHE Claude committed
84
85
\item[Trigonometry] functions \verb|cos|, \verb|sin|, \verb|tan|, and
  \verb|atan|. Constant \verb|pi|.
MARCHE Claude's avatar
MARCHE Claude committed
86

MARCHE Claude's avatar
MARCHE Claude committed
87
88
\item[Hyperbolic] functions \verb|cosh|, \verb|sinh|, \verb|tanh|,
  \verb|acosh|, \verb|asinh|, \verb|atanh|.
MARCHE Claude's avatar
MARCHE Claude committed
89

MARCHE Claude's avatar
MARCHE Claude committed
90
\item[Polar] functions \verb|hypot| and \verb|atan2|.
MARCHE Claude's avatar
MARCHE Claude committed
91

MARCHE Claude's avatar
MARCHE Claude committed
92
93
\end{description}

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
94
\section{Library \texttt{floating\_point}}
MARCHE Claude's avatar
MARCHE Claude committed
95
96

This library provides a theory of IEEE-754 floating-point numbers. It
97
is inspired by~\cite{ayad10ijcar}.
MARCHE Claude's avatar
MARCHE Claude committed
98
99
100
101
102

\begin{description}
\item[Rounding] type \verb|mode| with 5 constants
  \verb|NearestTiesToEven|, \verb|ToZero|, \verb|Up|, \verb|Down| and
  \verb|NearTiesToAway|.
103
\item[SpecialValues] handling of infinities and NaN.
MARCHE Claude's avatar
MARCHE Claude committed
104
105
106
\item[GenFloat] generic floats parameterized by the maximal
  representable number. Functions \verb|round|, \verb|value|,
  \verb|exact|, \verb|model|, predicate \verb|no_overflow|.
107
108
\item[Single] instance of GenFloat for 32-bits single precision numbers.
\item[Double] instance of GenFloat for 64-bits double precision numbers.
MARCHE Claude's avatar
MARCHE Claude committed
109
110
111
\end{description}


MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
112
\section{Library \texttt{array}}
MARCHE Claude's avatar
MARCHE Claude committed
113
114

\begin{description}
MARCHE Claude's avatar
MARCHE Claude committed
115

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

MARCHE Claude's avatar
MARCHE Claude committed
122
123
\item[ArrayLength] arrays indexed by integers and holding their
  length. Function \verb|length|.
MARCHE Claude's avatar
MARCHE Claude committed
124

MARCHE Claude's avatar
MARCHE Claude committed
125
126
127
\item[ArrayRich] additional functions on arrays indexed by
  integers. Functions \verb|sub| and \verb|app| to extract a sub-array
  and append arrays.
MARCHE Claude's avatar
MARCHE Claude committed
128
129
130

\end{description}

MARCHE Claude's avatar
example    
MARCHE Claude committed
131
\section{Library \texttt{option}}
MARCHE Claude's avatar
MARCHE Claude committed
132
133
134
135
136
137
138

\begin{description}
\item[Option] data type \verb|option 'a| with constructors \verb|None| and
  \verb|Some|.
\end{description}


MARCHE Claude's avatar
example    
MARCHE Claude committed
139
\section{Library \texttt{list}}
MARCHE Claude's avatar
MARCHE Claude committed
140
141
142
143
144
145
146
147
148
149
150

\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.
151
152
153
154
\item[NumOcc] number of occurrences in a list.
\item[Permut] list permutations.
\item[Induction] structural induction on lists.
\item[Map] list map operator.
MARCHE Claude's avatar
MARCHE Claude committed
155
156
157
\end{description}


MARCHE Claude's avatar
MARCHE Claude committed
158
159


MARCHE Claude's avatar
docs    
MARCHE Claude committed
160
161
162
163
164
165

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