[PPL-devel] [GIT] ppl/ppl(floating_point): More additions and corrections to the documentation.

Thu Sep 10 14:26:33 CEST 2009

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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Thu Sep 10 14:18:14 2009 +0200

More additions and corrections to the documentation.

---

 src/Difference_Floating_Point_Expression.defs.hh |    3 +-
 src/Opposite_Floating_Point_Expression.defs.hh   |   76 +++++++++++++++++-----
 src/Sum_Floating_Point_Expression.defs.hh        |    7 ++-
 3 files changed, 67 insertions(+), 19 deletions(-)

diff --git a/src/Difference_Floating_Point_Expression.defs.hh b/src/Difference_Floating_Point_Expression.defs.hh
index 29c923b..473d2d7 100644
--- a/src/Difference_Floating_Point_Expression.defs.hh
+++ b/src/Difference_Floating_Point_Expression.defs.hh
@@ -86,7 +86,8 @@ namespace Parma_Polyhedra_Library {
   follows:
   \f[
   \linexpr{e_{1} \ominus e_{2}}
-  \left \langle \rho^{\#}, \rho^{\#}_l \right \rangle =
+  \left \langle \rho^{\#}, \rho^{\#}_l \right \rangle
+  =
   \linexpr{e_{1}}\left \langle \rho^{\#}, \rho^{\#}_l \right \rangle
   \adlf
   \linexpr{e_{2}}\left \langle \rho^{\#}, \rho^{\#}_l \right \rangle
diff --git a/src/Opposite_Floating_Point_Expression.defs.hh b/src/Opposite_Floating_Point_Expression.defs.hh
index 16245bf..67dde22 100644
--- a/src/Opposite_Floating_Point_Expression.defs.hh
+++ b/src/Opposite_Floating_Point_Expression.defs.hh
@@ -45,13 +45,41 @@ namespace Parma_Polyhedra_Library {
 
 /*! \brief
   A generic Opposite Floating Point Expression.
+
   \ingroup PPL_CXX_interface
 
+  \par Template type parameters
+
   - The class template type parameter \p FP_Interval_Type represents the type
   of the intervals used in the abstract domain.
-  -  The class template type parameter \p FP_Format represents the format
-  of the floating point variable used in the concrete domain.
- */
+  - The class template type parameter \p FP_Format represents the floating
+  point format used in the concrete domain.
+
+  \par Linearization of opposite floating-point expressions
+
+  Let \f$i + \sum_{v \in \cV}i_{v}v \f$ be an interval linear form and
+  let \f$\adlf\f$ be a sound unary operator on linear forms such that:
+
+  \f[
+  \adlf
+  \left(i + \sum_{v \in \cV}i_{v}v\right)
+  =
+  \left(\adifp i\right) +
+  \sum_{v \in \cV}\left(\adifp i_{v} \right)v,
+  \f]
+
+  Given a floating point expression \f$\ominus e\f$ and a composite
+  abstract store \f$\left \langle \rho^{\#}, \rho^{\#}_l \right \rangle\f$,
+  we construct the interval linear form
+  \f$\linexpr{\ominus e}\left \langle \rho^{\#}, \rho^{\#}_l \right \rangle\f$
+  as follows:
+  \f[
+  \linexpr{\ominus e} \left \langle \rho^{\#}, \rho^{\#}_l \right \rangle
+  =
+  \adlf
+  \linexpr{e} \left \langle \rho^{\#}, \rho^{\#}_l \right \rangle.
+  \f]
+*/
 template <typename FP_Interval_Type, typename FP_Format>
 class Opposite_Floating_Point_Expression
   : public Floating_Point_Expression<FP_Interval_Type, FP_Format> {
@@ -74,12 +102,16 @@ public:
   Floating_Point_Expression<FP_Interval_Type, FP_Format>::
   FP_Interval_Abstract_Store FP_Interval_Abstract_Store;
 
+  /* \brief
+     Alias for the std::map<dimension_type, FP_Linear_Form> from
+     Floating_Point_Expression.
+  */
   typedef typename
   Floating_Point_Expression<FP_Interval_Type, FP_Format>::
   FP_Linear_Form_Abstract_Store FP_Linear_Form_Abstract_Store;
 
   /* \brief
-     Alias for the P_Interval_Type::boundary_type from
+     Alias for the FP_Interval_Type::boundary_type from
      Floating_Point_Expression.
   */
   typedef typename
@@ -87,7 +119,7 @@ public:
   boundary_type;
 
   /* \brief
-     Alias for the P_Interval_Type::info_type from Floating_Point_Expression.
+     Alias for the FP_Interval_Type::info_type from Floating_Point_Expression.
   */
   typedef typename
   Floating_Point_Expression<FP_Interval_Type, FP_Format>::info_type info_type;
@@ -95,9 +127,8 @@ public:
   //! \name Constructors and Destructor
   //@{
   /*! \brief
-    Constructor with a parameter: builds the opposite floating point
-    expression from \p op corresponding to the floating point expression
-    -\p op.
+    Constructor with one parameter: builds the opposite floating point
+    expression \f$\ominus\f$ \p op.
   */
   explicit Opposite_Floating_Point_Expression(
            Floating_Point_Expression<FP_Interval_Type, FP_Format>* const op);
@@ -107,14 +138,27 @@ public:
 
   //@} // Constructors and Destructor
 
-  /* \brief
-     Returns a linear form in the abstract store \p store that simply
-     represents the opposite of the operand linearization.
+  // FIXME: Modify documentation when exceptions are fixed
+  /*! \brief
+    Linearizes the expression in a given astract store.
+
+    Makes \p result become the linearization of \p *this in the given
+    composite abstract store.
+
+    \param int_store The interval abstract store.
+    \param lf_store The linear form abstract store.
+    \param result The modified linear form.
 
-     \param int_store The interval abstract store.
-     \param lf_store The linear form abstract store.
-     \param result The modified linear form.
+    \exception Parma_Polyhedra_Library::Linearization_Failed
+    Thrown if linearization fails for some reason.
 
+    Note that all variables occuring in the expression represented
+    by \p operand MUST have an associated value in \p int_store.
+    If this precondition is not met, calling the method
+    causes an undefined behavior.
+    
+    See the class description for a detailed explanation of how \p result
+    is computed.
   */
   void linearize(const FP_Interval_Abstract_Store& int_store,
                  const FP_Linear_Form_Abstract_Store& lf_store,
@@ -127,7 +171,7 @@ private:
 
   #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
   /*! \brief
-    Copy constructor: temporary inhibited.
+    Inhibited copy constructor.
   */
   #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
   Opposite_Floating_Point_Expression(
@@ -135,7 +179,7 @@ private:
 
   #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
   /*! \brief
-    Assignment operator: temporary inhibited.
+    Inhibited assignment operator.
   */
   #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
   Opposite_Floating_Point_Expression& operator=(
diff --git a/src/Sum_Floating_Point_Expression.defs.hh b/src/Sum_Floating_Point_Expression.defs.hh
index 9ae586e..22724ff 100644
--- a/src/Sum_Floating_Point_Expression.defs.hh
+++ b/src/Sum_Floating_Point_Expression.defs.hh
@@ -72,10 +72,13 @@ namespace Parma_Polyhedra_Library {
   Given an expression \f$e_{1} \oplus e_{2}\f$ and a composite
   abstract store \f$\left \langle \rho^{\#}, \rho^{\#}_l \right \rangle\f$,
   we construct the interval linear form
-  \f$\linexpr{e_{1} \oplus e_{2}}\left ( \rho^{\#}, \rho^{\#}_l \right )\f$
+  \f$\linexpr{e_{1} \oplus e_{2}}
+  \left \langle \rho^{\#}, \rho^{\#}_l \right \rangle\f$
   as follows:
   \f[
-  \linexpr{e_{1} \oplus e_{2}}\left ( \rho^{\#}, \rho^{\#}_l \right ) =
+  \linexpr{e_{1} \oplus e_{2}}
+  \left \langle \rho^{\#}, \rho^{\#}_l \right \rangle
+  =
   \linexpr{e_{1}}\left \langle \rho^{\#}, \rho^{\#}_l \right \rangle
   \aslf
   \linexpr{e_{2}}\left \langle \rho^{\#}, \rho^{\#}_l \right \rangle


