Commit 2cc3c176 authored by MARCHE Claude's avatar MARCHE Claude

doc of stdlib

parent 2103b6b8
\chapter{Standard Library}
\label{chap:library}
We provide here a short description of logic symbols defined in the
standard library. Only the most general-purpose ones are
described. For more details, one shoudl directly read the
corresponding file.
For each library, we describe the symbols of each theories.
\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
zero, alsos written as \verb|div| and \verb|mod|
\item[MinMax] \verb|min| and \verb|max| operators
\end{description}
\section{Library real}
\begin{description}
\item[algebra]
\item[Real] basic operations \verb|+|, \verb|-|, \verb|*| and \verb|/| ;
comparison operators
\item[int]
\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.
division: Euclidean versus Computer
\item[Abs] absolute value written as \verb|abs|
\item[MinMax] \verb|min| and \verb|max| operators
\item[array]
\item[FromInt] operator \verb|from_int| to convert an integer to a real.
\item[bool]
\item[Truncate] conversion operators from real to integers:
\verb|truncate| rounds to 0, \verb|floor| rounds down and
\verb|ceil| rounds up
\item[comparison]
\item[Square] operators \verb|sqr| and \verb|sqrt| for square and square root
\item[floating\_point]
\item[ExpLog] functions \verb|exp|, \verb|log|, \verb|log2|, and \verb|log10|
\cite{ayad10ijcar}
\item[Power] function \verb|pow| with two real parameters.
\item[graph]
\item[Trigonometry] functions \verb|cos|, \verb|sin|, \verb|tan|, and
\verb|atan|. Constant \verb|pi|.
\item[list]
\item[Hyperbolic] functions \verb|cosh|, \verb|sinh|, \verb|tanh|,
\verb|acosh|, \verb|asinh|, \verb|atanh|.
\item[option]
\item[Polar] functions \verb|hypot| and \verb|atan2|.
\item[real]
\end{description}
\section{Library floating\_point}
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}
\section{Library Array}
\begin{description}
\item[relations]
\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.
\item[set]
\item[ArrayLength] arrays indexed by integers and holding their
length. Function \verb|length|.
\item[sum]
\item[ArrayRich] additional functions on arrays indexed by
integers. Functions \verb|sub| and \verb|app| to extract a sub-array
and append arrays.
\end{description}
\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}
......
......@@ -20,9 +20,9 @@ theory TestInt
goal Test2: forall x:int. x*x >= 0
goal Test3: 1<>0
goal Test3: 1<>0
goal Test4: 1=2 -> 3=4
goal Test4: 1=2 -> 3=4
goal Test5: forall x:int. x <> 0 -> x*x > 0
......
......@@ -9,7 +9,7 @@ theory Length
use import int.Int
use import List
logic length (l : list 'a) : int =
logic length (l : list 'a) : int =
match l with
| Nil -> 0
| Cons _ r -> 1 + length r
......@@ -23,7 +23,7 @@ end
theory Mem
use export List
logic mem (x: 'a) (l : list 'a) = match l with
| Nil -> false
| Cons y r -> x = y or mem x r
......@@ -35,7 +35,7 @@ theory Nth
use export List
use export option.Option
use import int.Int
logic nth (n : int) (l : list 'a) : option 'a = match l with
| Nil -> None
| Cons x r -> if n = 0 then Some x else nth (n - 1) r
......@@ -63,7 +63,7 @@ theory HdTl "head and tail"
use import int.Int
lemma Nth_tl :
forall l1 l2 : list 'a. tl l1 = Some l2 ->
forall l1 l2 : list 'a. tl l1 = Some l2 ->
forall i : int. nth i l2 = nth (i+1) l1
lemma Nth0_head:
......@@ -80,8 +80,8 @@ theory Append
| Cons x1 r1 -> Cons x1 (append r1 l2)
end
lemma Append_assoc :
forall l1 l2 l3 : list 'a.
lemma Append_assoc :
forall l1 l2 l3 : list 'a.
append l1 (append l2 l3) = append (append l1 l2) l3
lemma Append_l_nil :
......@@ -106,7 +106,7 @@ theory Reverse
end
use import Length
lemma Reverse_length :
forall l : list 'a. length (reverse l) = length l
......@@ -116,16 +116,16 @@ theory Sorted
use export List
use import int.Int
inductive sorted (l : list int) =
| Sorted_Nil :
| Sorted_Nil :
sorted Nil
| Sorted_One :
| Sorted_One :
forall x:int. sorted (Cons x Nil)
| Sorted_Two :
forall x y : int, l : list int.
| Sorted_Two :
forall x y : int, l : list int.
x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
use import Mem
lemma Sorted_mem :
......@@ -135,12 +135,12 @@ theory Sorted
end
theory NumOcc
use import int.Int
use import List
(* number of occurence of x in l *)
logic num_occ (x : 'a) (l : list 'a) : int =
logic num_occ (x : 'a) (l : list 'a) : int =
match l with
| Nil -> 0
| Cons y r -> (if x = y then 1 else 0) + num_occ x r
......@@ -148,7 +148,7 @@ theory NumOcc
use import Mem
lemma Mem_Num_Occ :
lemma Mem_Num_Occ :
forall x:'a, l:list 'a. mem x l <-> num_occ x l > 0
end
......@@ -158,23 +158,23 @@ theory Permut
use import NumOcc
use import List
logic permut (l1 : list 'a) (l2 : list 'a) =
logic permut (l1 : list 'a) (l2 : list 'a) =
forall x : 'a. num_occ x l1 = num_occ x l2
lemma Permut_refl : forall l : list 'a. permut l l
lemma Permut_sym : forall l1 l2 : list 'a. permut l1 l2 -> permut l2 l1
lemma Permut_trans :
lemma Permut_trans :
forall l1 l2 l3 : list 'a. permut l1 l2 -> permut l2 l3 -> permut l1 l3
lemma Permut_cons :
forall x : 'a, l1 l2 : list 'a.
lemma Permut_cons :
forall x : 'a, l1 l2 : list 'a.
permut l1 l2 -> permut (Cons x l1) (Cons x l2)
lemma Permut_swap :
lemma Permut_swap :
forall x y : 'a, l : list 'a. permut (Cons x (Cons y l)) (Cons y (Cons x l))
use import Mem
lemma Permut_mem :
......@@ -194,7 +194,7 @@ theory Induction
logic p (list elt)
axiom Induction :
axiom Induction :
p (Nil : list elt) ->
(forall x:elt. forall l:list elt. p l -> p (Cons x l)) ->
forall l:list elt. p l
......@@ -203,12 +203,12 @@ end
theory Map
use import List
type a
type b
type b
logic f a : b
logic map(l : list a) : list b =
logic map(l : list a) : list b =
match l with
| Nil -> Nil
| Cons x r -> Cons (f x) (map r)
......
......@@ -329,13 +329,13 @@ theory Hyperbolic
logic cosh (x : real) : real = 0.5 * (exp x + exp (-x))
logic tanh (x : real) : real = sinh x / cosh x
logic arsinh (x : real) : real = log (x + sqrt (sqr x + 1.0))
logic arcosh (x : real) : real
axiom Arcosh_def:
forall x:real. x >= 1.0 -> arcosh x = log (x + sqrt (sqr x - 1.0))
logic artanh (x : real) : real
axiom Artanh_def:
forall x:real. -1.0 < x < 1.0 -> artanh x = 0.5 * log ((1.0+x)/(1.0-x))
logic asinh (x : real) : real = log (x + sqrt (sqr x + 1.0))
logic acosh (x : real) : real
axiom Acosh_def:
forall x:real. x >= 1.0 -> acosh x = log (x + sqrt (sqr x - 1.0))
logic atanh (x : real) : real
axiom Atanh_def:
forall x:real. -1.0 < x < 1.0 -> atanh x = 0.5 * log ((1.0+x)/(1.0-x))
end
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment