library.tex 4.8 KB
 MARCHE Claude committed Oct 28, 2010 1 2 3 \chapter{Standard Library} \label{chap:library}  MARCHE Claude committed Dec 15, 2010 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 committed Dec 15, 2010 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 committed Dec 15, 2010 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 committed Dec 15, 2010 50  zero, also written as \verb|div| and \verb|mod|  MARCHE Claude committed Dec 15, 2010 51 52 53 54 55 56 57  \item[MinMax] \verb|min| and \verb|max| operators \end{description} \section{Library real}  MARCHE Claude committed Dec 13, 2010 58 \begin{description}  MARCHE Claude committed Oct 28, 2010 59   MARCHE Claude committed Dec 15, 2010 60 61 \item[Real] basic operations \verb|+|, \verb|-|, \verb|*| and \verb|/| ; comparison operators  MARCHE Claude committed Oct 28, 2010 62   MARCHE Claude committed Dec 15, 2010 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 committed Oct 28, 2010 66   MARCHE Claude committed Dec 15, 2010 67 \item[Abs] absolute value written as \verb|abs|  MARCHE Claude committed Oct 28, 2010 68   MARCHE Claude committed Dec 15, 2010 69 \item[MinMax] \verb|min| and \verb|max| operators  MARCHE Claude committed Oct 28, 2010 70   MARCHE Claude committed Dec 15, 2010 71 \item[FromInt] operator \verb|from_int| to convert an integer to a real.  MARCHE Claude committed Dec 13, 2010 72   MARCHE Claude committed Dec 15, 2010 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 committed Dec 13, 2010 76   MARCHE Claude committed Dec 15, 2010 77 \item[Square] operators \verb|sqr| and \verb|sqrt| for square and square root  MARCHE Claude committed Dec 13, 2010 78   MARCHE Claude committed Dec 15, 2010 79 \item[ExpLog] functions \verb|exp|, \verb|log|, \verb|log2|, and \verb|log10|  MARCHE Claude committed Oct 28, 2010 80   MARCHE Claude committed Dec 15, 2010 81 \item[Power] function \verb|pow| with two real parameters.  MARCHE Claude committed Oct 28, 2010 82   MARCHE Claude committed Dec 15, 2010 83 84 \item[Trigonometry] functions \verb|cos|, \verb|sin|, \verb|tan|, and \verb|atan|. Constant \verb|pi|.  MARCHE Claude committed Dec 13, 2010 85   MARCHE Claude committed Dec 15, 2010 86 87 \item[Hyperbolic] functions \verb|cosh|, \verb|sinh|, \verb|tanh|, \verb|acosh|, \verb|asinh|, \verb|atanh|.  MARCHE Claude committed Dec 13, 2010 88   MARCHE Claude committed Dec 15, 2010 89 \item[Polar] functions \verb|hypot| and \verb|atan2|.  MARCHE Claude committed Dec 13, 2010 90   MARCHE Claude committed Dec 15, 2010 91 92 \end{description}  MARCHE Claude committed Dec 17, 2010 93 \section{Library \texttt{floating\_point}}  MARCHE Claude committed Dec 15, 2010 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 committed Dec 17, 2010 111 \section{Library \texttt{array}}  MARCHE Claude committed Dec 15, 2010 112 113  \begin{description}  MARCHE Claude committed Dec 13, 2010 114   MARCHE Claude committed Dec 15, 2010 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 committed Dec 13, 2010 120   MARCHE Claude committed Dec 15, 2010 121 122 \item[ArrayLength] arrays indexed by integers and holding their length. Function \verb|length|.  MARCHE Claude committed Dec 13, 2010 123   MARCHE Claude committed Dec 15, 2010 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 committed Dec 13, 2010 127 128 129  \end{description}  MARCHE Claude committed Dec 15, 2010 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 committed Dec 13, 2010 157 158   MARCHE Claude committed Oct 28, 2010 159 160 161 162 163 164  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: