library.tex 4.8 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
23
24
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}

In the following, for each library, we describe the (main) symbols of
each theories defined
MARCHE Claude's avatar
MARCHE Claude committed
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49

\section{Library 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[Ite] polymorphic if-then-else operator written as \verb|ite|

\end{description}

\section{Library int}

\begin{description}

\item[Int] basic operations \verb|+|, \verb|-| and \verb|*| ; comparison
  operators \verb|<|, \verb|>|, \verb|>=| and \verb|<=|.

\item[Abs] absolute value written as \verb|abs|

\item[EuclideanDivision] division and modulo, where division rounds
  down, written as \verb|div| and \verb|mod|

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

\item[MinMax] \verb|min| and \verb|max| operators

\end{description}

\section{Library real}

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
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
75
\item[Truncate] conversion operators from real to integers:
  \verb|truncate| rounds to 0, \verb|floor| rounds down and
  \verb|ceil| rounds up
MARCHE Claude's avatar
MARCHE Claude committed
76

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

MARCHE Claude's avatar
MARCHE Claude committed
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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110

This library provides a theory of IEEE-754 floating-point numbers. It
is inspired from~\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}


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
MARCHE Claude committed
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
\section{Library option}

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


\section{Library 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}


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: