[PPL-devel] [GIT] ppl/ppl(floating_point): Added some documentation.

[Fabio Bossi]

Module: ppl/ppl
Branch: floating_point
Commit: 4a1d25bd5a05e759dcc4d1f6a0b9f1204435bda7
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4a1d25bd5a05e759dcc4d1f6a0b9f1204435bda7

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Tue Sep  8 16:29:40 2009 +0200

Added some documentation.

---

 doc/definitions.dox |   71 +++++++++++++++++++++++++++++++++++++++++++++++++++
 doc/ppl.sty         |    1 -
 2 files changed, 71 insertions(+), 1 deletions(-)

diff --git a/doc/definitions.dox b/doc/definitions.dox
index ff19299..4da0008 100644
--- a/doc/definitions.dox
+++ b/doc/definitions.dox
@@ -2594,6 +2594,77 @@ to see that the widening operator is actually compatible with
 a given convergence certificate. If such a requirement is not met,
 then an extrapolation operator will be obtained.
 
+\section floating_point Analysis of floating point computations
+
+This section describes the PPL abstract domains that are used for
+approximating floating point computations in software analysis. We follow
+the approch described in \ref Min04 "[Min04]" and more detailedly in
+\ref Min05 "[Min05]". We will denote by \f$\cV\f$ the set of all floating
+point variables in the analyzed program. We will also denote by
+\f$\mathbb{F}_a\f$ the set of floating point numbers in the format used by the
+analyzer (that is, the machine running the PPL) and by \f$\mathbb{F}_t\f$
+the set of floating point numbers in the format used by the machine that is
+expected to run the analyzed program. Recall that floating point numbers
+include the infinities \f$-\infty\f$ and \f$+\infty\f$.
+
+\subsection interval_linear_forms Linear forms with interval coefficients
+
+Generic concrete <EM>floating point expressions</EM> on \f$\mathbb{F}_t\f$ are
+represented by the \link Parma_Polyhedra_Library::Floating_Point_Expression
+\c Floating_Point_Expression \endlink abstract class. Its concrete derivate
+classes are:
+  - \link Parma_Polyhedra_Library::Constant_Floating_Point_Expression \c
+    Constant_Floating_Point_Expression \endlink,
+  - \link Parma_Polyhedra_Library::Variable_Floating_Point_Expression \c
+    Variable_Floating_Point_Expression \endlink,
+  - \link Parma_Polyhedra_Library::Opposite_Floating_Point_Expression \c
+    Variable_Floating_Point_Expression \endlink, that is the negation
+    (unary minus) of a floating point expression,
+  - \link Parma_Polyhedra_Library::Sum_Floating_Point_Expression \c
+    Sum_Floating_Point_Expression \endlink, that is the sum of two floating
+    point expressions,
+  - \link Parma_Polyhedra_Library::Difference_Floating_Point_Expression \c
+    Difference_Floating_Point_Expression \endlink, that is the difference of
+    two floating point expressions,
+  - \link Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression \c
+    Multiplication_Floating_Point_Expression \endlink, that is the product of
+    two floating point expressions, and
+  - \link Parma_Polyhedra_Library::Division_Floating_Point_Expression \c
+    Division_Floating_Point_Expression \endlink, that is the division of
+    two floating point expressions.
+
+The set of all the possible values in \f$\mathbb{F}_t\f$ of a floating point
+expression at a given program point in a given abstract store can be
+overapproximated by a <EM>linear form</EM> with interval coefficients, that is
+a linear expression of this kind:
+
+\f[
+  i + \sum_{v \in \cV}i_{v}v,
+\f]
+
+where all \f$v\f$ are free floating point variables and \f$i\f$ and all
+\f$i_{v}\f$ are elements of \f$\mathbb{I}_a\f$, defined as the set of all
+intervals with boundaries in \f$\mathbb{F}_a\f$. This operation is called
+<EM>linearization</EM> and is performed by the method linearize of floating
+point expression classes.
+
+Even though the intervals may be open, we will always use closed intervals
+in the documentation for the sake of simplicity, with the exception of unbounded
+intervals that have \f$\infty\f$ boundaries. We denote the set of all linear
+forms on \f$\mathbb{F}_a\f$ by \f$\mathbb{L}_a\f$.
+
+A <EM>(composite) floating point abstract store</EM> is used to associate each
+floating point variable with its currently known approximation. The store is
+composed by two parts:
+  - an <EM>interval abstract store</EM> \f$\fund{\rho,\cV,\mathbb{I}_a}\f$
+    associating each variable with its current approximating interval, and
+  - a <EM>linear form abstract store</EM> \f$\fund{\rho,\cV,\mathbb{L}_a}\f$
+    associating each variable with its current approximating linear form.
+
+Both stores are represented by maps of the Standard Template Library and are
+needed for performing linearization. Please see the documentation of floating
+point expression classes for more information.
+
 \section use_of_library Using the Library
 
 \subsection A_Note_on_the_Implementation_of_the_Operators A Note on the Implementation of the Operators
diff --git a/doc/ppl.sty b/doc/ppl.sty
index 0015104..87b3207 100644
--- a/doc/ppl.sty
+++ b/doc/ppl.sty
@@ -191,4 +191,3 @@
 \newcommand*{\adlf}{\boxminus^{\#}_{\mathbf{f}}}
 \newcommand*{\adivlf}{\boxslash^{\#}_{\mathbf{f}}}
 \newcommand*{\amlf}{\boxtimes^{\#}_{\mathbf{f}}}
-