library.tex 4.84 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
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
described. For more details, one should directly read the
corresponding file, or alternatively, use the \verb|why3| with option \verb|-T| and a qualified theory name, \eg
\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}

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

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

\begin{description}

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

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

\end{description}

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

\begin{description}

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

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

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

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

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

\end{description}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\begin{description}
\item[Rounding] type \verb|mode| with 5 constants
  \verb|NearestTiesToEven|, \verb|ToZero|, \verb|Up|, \verb|Down| and
  \verb|NearTiesToAway|.
102
\item[SpecialValues] handling of infinities and NaN.
MARCHE Claude's avatar
MARCHE Claude committed
103
104
105
\item[GenFloat] generic floats parameterized by the maximal
  representable number. Functions \verb|round|, \verb|value|,
  \verb|exact|, \verb|model|, predicate \verb|no_overflow|.
106
107
\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
108
109
110
\end{description}


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

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
124
125
126
\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
127
128
129

\end{description}

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

\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
138
\section{Library \texttt{list}}
MARCHE Claude's avatar
MARCHE Claude committed
139
140
141
142
143
144
145
146
147
148
149

\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.
150
151
152
153
\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
154
155
156
\end{description}


MARCHE Claude's avatar
MARCHE Claude committed
157
158


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

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