Do use the notation "[l, u]" to denote the closed interval with boundaries `l' and `u'.

13 files changed, 79 insertions, 79 deletions

diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh
index f9f517a77..22d719bb8 100644
--- a/src/BD_Shape.templates.hh
+++ b/src/BD_Shape.templates.hh
@@ -4255,7 +4255,7 @@ void BD_Shape<T>
   if (w_id == var_id) {
     // True if `b' is in [b_mlb, b_ub] and that is [0, 0].
     bool is_b_zero = (b_mlb == 0 && b_ub == 0);
-    // Here `lf' is of the form: [+/-1;+/-1] * v + b.
+    // Here `lf' is of the form: [+/-1, +/-1] * v + b.
     if (is_w_coeff_one) {
       if (is_b_zero)
         // The transformation is the identity function.
@@ -4274,7 +4274,7 @@ void BD_Shape<T>
       }
     }
     else {
-      // Here `w_coeff = [-1;-1].
+      // Here `w_coeff = [-1, -1].
       // Remove the binary constraints on `var'.
       forget_binary_dbm_constraints(var_id);
       using std::swap;
@@ -4293,7 +4293,7 @@ void BD_Shape<T>
   }
   else {
     // Here `w != var', so that `lf' is of the form
-    // [+/-1;+/-1] * w + b.
+    // [+/-1, +/-1] * w + b.
     // Remove all constraints on `var'.
     forget_all_dbm_constraints(var_id);
     // Shortest-path closure is preserved, but not reduction.
@@ -4328,7 +4328,7 @@ void BD_Shape<T>
 // General case.
 // Either t == 2, so that
 // lf == i_1*x_1 + i_2*x_2 + ... + i_n*x_n + b, where n >= 2,
-// or t == 1, lf == i*w + b, but i <> [+/-1;+/-1].
+// or t == 1, lf == i*w + b, but i <> [+/-1, +/-1].
 template <typename T>
 template <typename Interval_Info>
 void BD_Shape<T>
@@ -4514,8 +4514,8 @@ BD_Shape<T>::left_inhomogeneous_refine(const dimension_type& right_t,
   typedef Interval<T, Interval_Info> FP_Interval_Type;
 
   if (right_t == 1) {
-    // The constraint has the form [a-;a+] <= [b-;b+] + [c-;c+] * x.
-    // Reduce it to the constraint +/-x <= b+ - a- if [c-;c+] = +/-[1;1].
+    // The constraint has the form [a-, a+] <= [b-, b+] + [c-, c+] * x.
+    // Reduce it to the constraint +/-x <= b+ - a- if [c-, c+] = +/-[1, 1].
       const FP_Interval_Type& right_w_coeff =
 	                      right.coefficient(Variable(right_w_id));
       if (right_w_coeff == 1) {
@@ -4554,8 +4554,8 @@ BD_Shape<T>
   typedef Interval<T, Interval_Info> FP_Interval_Type;
 
     if (right_t == 0) {
-      // The constraint has the form [b-;b+] + [c-;c+] * x <= [a-;a+]
-      // Reduce it to the constraint +/-x <= a+ - b- if [c-;c+] = +/-[1;1].
+      // The constraint has the form [b-, b+] + [c-, c+] * x <= [a-, a+]
+      // Reduce it to the constraint +/-x <= a+ - b- if [c-, c+] = +/-[1, 1].
       const FP_Interval_Type& left_w_coeff =
 	left.coefficient(Variable(left_w_id));
 
@@ -4580,10 +4580,10 @@ BD_Shape<T>
       }
     }
     else if (right_t == 1) {
-      // The constraint has the form:
-      // [a-;a+] + [b-;b+] * x <= [c-;c+] + [d-;d+] * y.
+      // The constraint has the form
+      // [a-, a+] + [b-, b+] * x <= [c-, c+] + [d-, d+] * y.
       // Reduce it to the constraint +/-x +/-y <= c+ - a-
-      // if [b-;b+] = +/-[1;1] and [d-;d+] = +/-[1;1].
+      // if [b-, b+] = +/-[1, 1] and [d-, d+] = +/-[1, 1].
       const FP_Interval_Type& left_w_coeff =
                               left.coefficient(Variable(left_w_id));
 
@@ -4844,7 +4844,7 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf,
     if (curr_lb != 0 || curr_ub != 0) {
       assign_r(curr_var_ub, dbm[0][n_var], ROUND_NOT_NEEDED);
       neg_assign_r(curr_minus_var_ub, dbm[n_var][0], ROUND_NOT_NEEDED);
-      // Optimize the most commons cases: curr = +/-[1;1]
+      // Optimize the most commons cases: curr = +/-[1, 1].
       if (curr_lb == 1 && curr_ub == 1) {
         add_assign_r(result, result, std::max(curr_var_ub, curr_minus_var_ub),
                      ROUND_UP);
diff --git a/src/Cast_Floating_Point_Expression.defs.hh b/src/Cast_Floating_Point_Expression.defs.hh
index cc171e9db..bb5186177 100644
--- a/src/Cast_Floating_Point_Expression.defs.hh
+++ b/src/Cast_Floating_Point_Expression.defs.hh
@@ -79,7 +79,7 @@ swap(Cast_Floating_Point_Expression<FP_Interval_Type, FP_Format>& x,
   \varepsilon_{\mathbf{f}}\left(\linexprenv{e}{\rho^{\#}}{\rho^{\#}_l}
   \right)
   \aslf
-  mf_{\mathbf{f}}[-1;1]
+  mf_{\mathbf{f}}[-1, 1]
   \f]
   where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the linear form computed by
   calling method <CODE>Floating_Point_Expression::relative_error</CODE>
diff --git a/src/Constant_Floating_Point_Expression.defs.hh b/src/Constant_Floating_Point_Expression.defs.hh
index 4726aaba0..7dfa8b4ba 100644
--- a/src/Constant_Floating_Point_Expression.defs.hh
+++ b/src/Constant_Floating_Point_Expression.defs.hh
@@ -54,7 +54,7 @@ void swap(Constant_Floating_Point_Expression<FP_Interval_Type, FP_Format>& x,
 
   The linearization of a constant floating point expression results in a
   linear form consisting of only the inhomogeneous term
-  \f$\left[ l;u \right]\f$, where \f$l\f$ and \f$u\f$ are the lower
+  \f$[l, u]\f$, where \f$l\f$ and \f$u\f$ are the lower
   and upper bounds of the constant value given to the class constructor.
 */
 template <typename FP_Interval_Type, typename FP_Format>
diff --git a/src/Difference_Floating_Point_Expression.defs.hh b/src/Difference_Floating_Point_Expression.defs.hh
index e49188ac6..00cfa2457 100644
--- a/src/Difference_Floating_Point_Expression.defs.hh
+++ b/src/Difference_Floating_Point_Expression.defs.hh
@@ -90,7 +90,7 @@ swap(Difference_Floating_Point_Expression<FP_Interval_Type, FP_Format>& x,
   \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}
   \right)
   \aslf
-  mf_{\mathbf{f}}[-1;1]
+  mf_{\mathbf{f}}[-1, 1]
   \f]
   where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the linear form computed by
   calling method <CODE>Floating_Point_Expression::relative_error</CODE>
diff --git a/src/Division_Floating_Point_Expression.defs.hh b/src/Division_Floating_Point_Expression.defs.hh
index 5caba4ce9..623b9e67e 100644
--- a/src/Division_Floating_Point_Expression.defs.hh
+++ b/src/Division_Floating_Point_Expression.defs.hh
@@ -72,28 +72,28 @@ void swap(Division_Floating_Point_Expression<FP_Interval_Type, FP_Format>& x,
   \left(i \adivifp i'\right)
   + \sum_{v \in \cV}\left(i_{v} \adivifp i'\right)v.
   \f]
-  Given an expression \f$e_{1} \oslash [a;b]\f$ and a composite
+  Given an expression \f$e_{1} \oslash [a, b]\f$ and a composite
   abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
   \rrbracket\f$,
   we construct the interval linear form
   \f$
-  \linexprenv{e_{1} \oslash [a;b]}{\rho^{\#}}{\rho^{\#}_l}
+  \linexprenv{e_{1} \oslash [a, b]}{\rho^{\#}}{\rho^{\#}_l}
   \f$
   as follows:
   \f[
-  \linexprenv{e_{1} \oslash [a;b]}{\rho^{\#}}{\rho^{\#}_l}
+  \linexprenv{e_{1} \oslash [a, b]}{\rho^{\#}}{\rho^{\#}_l}
   =
   \left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l}
   \adivlf
-  [a;b]\right)
+  [a, b]\right)
   \aslf
   \left(\varepsilon_{\mathbf{f}}\left(
   \linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l}
   \right)
   \adivlf
-  [a;b]\right)
+  [a, b]\right)
   \aslf
-  mf_{\mathbf{f}}[-1;1],
+  mf_{\mathbf{f}}[-1, 1],
   \f]
   given an expression \f$e_{1} \oslash e_{2}\f$ and a composite
   abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
diff --git a/src/Float.defs.hh b/src/Float.defs.hh
index 9d177c47d..5a3c54d6e 100644
--- a/src/Float.defs.hh
+++ b/src/Float.defs.hh
@@ -468,7 +468,7 @@ bool is_less_precise_than(Floating_Point_Format f1, Floating_Point_Format f2);
   \param analyzed_format The floating point format used by the analyzed
   program.
 
-  \return The interval \f$[-\omega; \omega]\f$ where \f$\omega\f$ is the
+  \return The interval \f$[-\omega, \omega]\f$ where \f$\omega\f$ is the
   smallest non-zero positive number in the less precise floating point
   format between the analyzer format and the analyzed format.
 */
diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh
index 7250089a5..1ed58c533 100644
--- a/src/Floating_Point_Expression.defs.hh
+++ b/src/Floating_Point_Expression.defs.hh
@@ -119,7 +119,7 @@ public:
   /*! \brief
     Absolute error.
 
-    Represents the interval \f$[-\omega; \omega]\f$ where \f$\omega\f$ is the
+    Represents the interval \f$[-\omega, \omega]\f$ where \f$\omega\f$ is the
     smallest non-zero positive number in the less precise floating point
     format between the analyzer format and the analyzed format.
 
@@ -150,13 +150,13 @@ public:
     on the linear form \p lf. This function is defined
     such as:
     \f[
-    \varepsilon_{\mathbf{f}}\left([a;b]+\sum_{v \in \cV}[a_{v};b_{v}]v\right)
+    \varepsilon_{\mathbf{f}}\left([a, b]+\sum_{v \in \cV}[a_{v}, b_{v}]v\right)
     \defeq
-    (\textrm{max}(|a|,|b|) \amifp [-\beta^{-\textrm{p}};\beta^{-\textrm{p}}])
+    (\textrm{max}(|a|, |b|) \amifp [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}])
     +
     \sum_{v \in \cV}(\textrm{max}(|a_{v}|,|b_{v}|)
     \amifp
-    [-\beta^{-\textrm{p}};\beta^{-\textrm{p}}])v
+    [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}])v
     \f]
     where p is the fraction size in bits for the format \f$\mathbf{f}\f$ and
     \f$\beta\f$ the base.
@@ -193,7 +193,7 @@ private:
     Static helper method that is used to compute the value of the public
     static field <CODE>absolute_error</CODE>.
 
-    \return The interval \f$[-\omega; \omega]\f$ corresponding to the value
+    \return The interval \f$[-\omega, \omega]\f$ corresponding to the value
     of <CODE>absolute_error</CODE>
   */
   static FP_Interval_Type compute_absolute_error();
diff --git a/src/Linear_Form.defs.hh b/src/Linear_Form.defs.hh
index 8c10b71e3..ec64ef7d5 100644
--- a/src/Linear_Form.defs.hh
+++ b/src/Linear_Form.defs.hh
@@ -348,13 +348,13 @@ public:
     obtained by evaluating the function \f$\varepsilon_{\mathbf{f}}(l)\f$
     on the linear form. This function is defined as:
     \f[
-    \varepsilon_{\mathbf{f}}\left([a;b]+\sum_{v \in \cV}[a_{v};b_{v}]v\right)
+    \varepsilon_{\mathbf{f}}\left([a, b]+\sum_{v \in \cV}[a_{v}, b_{v}]v\right)
     \defeq
-    (\textrm{max}(|a|,|b|) \amifp [-\beta^{-\textrm{p}};\beta^{-\textrm{p}}])
+    (\textrm{max}(|a|, |b|) \amifp [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}])
     +
     \sum_{v \in \cV}(\textrm{max}(|a_{v}|,|b_{v}|)
     \amifp
-    [-\beta^{-\textrm{p}};\beta^{-\textrm{p}}])v
+    [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}])v
     \f]
     where p is the fraction size in bits for the format \f$\mathbf{f}\f$ and
     \f$\beta\f$ the base.
diff --git a/src/Multiplication_Floating_Point_Expression.defs.hh b/src/Multiplication_Floating_Point_Expression.defs.hh
index f5b744b2b..fde4c27eb 100644
--- a/src/Multiplication_Floating_Point_Expression.defs.hh
+++ b/src/Multiplication_Floating_Point_Expression.defs.hh
@@ -73,35 +73,35 @@ swap(Multiplication_Floating_Point_Expression<FP_Interval_Type, FP_Format>& x,
   \left(i \amifp i'\right)
   + \sum_{v \in \cV}\left(i \amifp i'_{v}\right)v.
   \f]
-  Given an expression \f$[a;b] \otimes e_{2}\f$ and a composite
+  Given an expression \f$[a, b] \otimes e_{2}\f$ and a composite
   abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
   \rrbracket\f$, we construct the interval linear form
-  \f$\linexprenv{[a;b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}\f$
+  \f$\linexprenv{[a, b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}\f$
   as follows:
   \f[
-  \linexprenv{[a;b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}
+  \linexprenv{[a, b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}
   =
-  \left([a;b]
+  \left([a, b]
   \amlf
   \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}\right)
   \aslf
-  \left([a;b]
+  \left([a, b]
   \amlf
   \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}
   \right)\right)
   \aslf
-  mf_{\mathbf{f}}[-1;1].
+  mf_{\mathbf{f}}[-1, 1].
   \f].
 
-  Given an expression \f$e_{1} \otimes [a;b]\f$ and a composite
+  Given an expression \f$e_{1} \otimes [a, b]\f$ and a composite
   abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
   \rrbracket\f$, we construct the interval linear form
-  \f$\linexprenv{e_{1} \otimes [a;b]}{\rho^{\#}}{\rho^{\#}_l}\f$
+  \f$\linexprenv{e_{1} \otimes [a, b]}{\rho^{\#}}{\rho^{\#}_l}\f$
   as follows:
   \f[
-  \linexprenv{e_{1} \otimes [a;b]}{\rho^{\#}}{\rho^{\#}_l}
+  \linexprenv{e_{1} \otimes [a, b]}{\rho^{\#}}{\rho^{\#}_l}
   =
-  \linexprenv{[a;b] \otimes e_{1}}{\rho^{\#}}{\rho^{\#}_l}.
+  \linexprenv{[a, b] \otimes e_{1}}{\rho^{\#}}{\rho^{\#}_l}.
   \f]
 
   Given an expression \f$e_{1} \otimes e_{2}\f$ and a composite
diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh
index 11da999de..1544ab9b5 100644
--- a/src/Octagonal_Shape.templates.hh
+++ b/src/Octagonal_Shape.templates.hh
@@ -557,8 +557,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality(
     }
 
     if (right_t == 1) {
-      // The constraint has the form [a-;a+] <= [b-;b+] + [c-;c+] * x.
-      // Reduce it to the constraint +/-x <= b+ - a- if [c-;c+] = +/-[1;1].
+      // The constraint has the form [a-, a+] <= [b-, b+] + [c-, c+] * x.
+      // Reduce it to the constraint +/-x <= b+ - a- if [c-, c+] = +/-[1, 1].
       const FP_Interval_Type& right_w_coeff =
 	                      right.coefficient(Variable(right_w_id));
       if (right_w_coeff == 1) {
@@ -592,8 +592,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality(
   }
   else if (left_t == 1) {
     if (right_t == 0) {
-      // The constraint has the form [b-;b+] + [c-;c+] * x <= [a-;a+]
-      // Reduce it to the constraint +/-x <= a+ - b- if [c-;c+] = +/-[1;1].
+      // The constraint has the form [b-, b+] + [c-, c+] * x <= [a-, a+]
+      // Reduce it to the constraint +/-x <= a+ - b- if [c-, c+] = +/-[1, 1].
       const FP_Interval_Type& left_w_coeff =
 	                      left.coefficient(Variable(left_w_id));
       if (left_w_coeff == 1) {
@@ -626,10 +626,10 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality(
     }
 
     if (right_t == 1) {
-      // The constraint has the form:
-      // [a-;a+] + [b-;b+] * x <= [c-;c+] + [d-;d+] * y.
+      // The constraint has the form
+      // [a-, a+] + [b-, b+] * x <= [c-, c+] + [d-, d+] * y.
       // Reduce it to the constraint +/-x +/-y <= c+ - a-
-      // if [b-;b+] = +/-[1;1] and [d-;d+] = +/-[1;1].
+      // if [b-, b+] = +/-[1, 1] and [d-, d+] = +/-[1, 1].
       const FP_Interval_Type& left_w_coeff =
                               left.coefficient(Variable(left_w_id));
       const FP_Interval_Type& right_w_coeff =
@@ -2131,8 +2131,8 @@ Octagonal_Shape<T>::relation_with(const Generator& g) const {
       : g.coefficient(x);
     if (is_additive_inverse(m_i_ii, m_ii_i)) {
       // The constraint has form ax = b.
-      // To satisfy the constraint it's necessary that the scalar product
-      // is not zero. The scalar product has the form:
+      // To satisfy the constraint it is necessary that the scalar product
+      // is not zero. The scalar product has the form
       // 'denom * g_coeff_x - numer * g.divisor()'.
       numer_denom(m_ii_i, numer, denom);
       denom *= 2;
@@ -2166,7 +2166,7 @@ Octagonal_Shape<T>::relation_with(const Generator& g) const {
         else
           // If the generator is not a line it's necessary to check
           // that the scalar product sign is not positive and the scalar
-          // product has the form:
+          // product has the form
           // '-denom * g.coeff_x - numer * g.divisor()'.
           if (product > 0)
             return Poly_Gen_Relation::nothing();
@@ -2187,7 +2187,7 @@ Octagonal_Shape<T>::relation_with(const Generator& g) const {
         else
           // If the generator is not a line it's necessary to check
           // that the scalar product sign is not positive and the scalar
-          // product has the form:
+          // product has the form
           // 'denom * g_coeff_x - numer * g.divisor()'.
           if (product > 0)
             return Poly_Gen_Relation::nothing();
@@ -5227,8 +5227,8 @@ Octagonal_Shape<T>::affine_form_image(const Variable var,
 
   // `w' is the variable with index `w_id'.
   // Now we know the form of `lf':
-  // - If t == 0, then lf == [lb;ub];
-  // - If t == 1, then lf == a*w + [lb;ub], where `w' can be `v' or another
+  // - If t == 0, then lf == [lb, ub];
+  // - If t == 1, then lf == a*w + [lb, ub], where `w' can be `v' or another
   //   variable;
   // - If t == 2, the `lf' is of the general form.
 
@@ -5238,7 +5238,7 @@ Octagonal_Shape<T>::affine_form_image(const Variable var,
   neg_assign_r(b_mlb, b.lower(), ROUND_NOT_NEEDED);
 
   if (t == 0) {
-    // Case 1: lf = [lb;ub];
+    // Case 1: lf = [lb, ub].
     forget_all_octagonal_constraints(var_id);
     mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_UP);
     mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_UP);
@@ -5260,9 +5260,9 @@ Octagonal_Shape<T>::affine_form_image(const Variable var,
     // True if `w_coeff' is in [-1, -1].
     bool is_w_coeff_minus_one = (w_coeff == -1);
     if (is_w_coeff_one || is_w_coeff_minus_one) {
-      // Case 2: lf = w_coeff*w + b, with w_coeff = [+/-1;+/-1].
+      // Case 2: lf = w_coeff*w + b, with w_coeff = [+/-1, +/-1].
       if (w_id == var_id) {
-        // Here lf = w_coeff*v + b, with w_coeff = [+/-1;+/-1].
+        // Here lf = w_coeff*v + b, with w_coeff = [+/-1, +/-1].
         if (is_w_coeff_one && is_b_zero)
           // The transformation is the identity function.
           return;
@@ -5308,7 +5308,7 @@ Octagonal_Shape<T>::affine_form_image(const Variable var,
       }
       else {
         // Here `w != var', so that `lf' is of the form
-        // [+/-1;+/-1] * w + b.
+        // [+/-1, +/-1] * w + b.
         // Remove all constraints on `var'.
         forget_all_octagonal_constraints(var_id);
         const dimension_type n_w = 2*w_id;
@@ -5344,7 +5344,7 @@ Octagonal_Shape<T>::affine_form_image(const Variable var,
   // General case.
   // Either t == 2, so that
   // expr == i_1*x_1 + i_2*x_2 + ... + i_n*x_n + b, where n >= 2,
-  // or t == 1, expr == i*w + b, but i <> [+/-1;+/-1].
+  // or t == 1, expr == i*w + b, but i <> [+/-1, +/-1].
 
   // In the following, strong closure will be definitely lost.
   reset_strongly_closed();
@@ -5446,7 +5446,7 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf,
       div_2exp_assign_r(curr_var_ub, curr_var_ub, 1, ROUND_UP);
       neg_assign_r(curr_minus_var_ub, matrix[n_var][n_var + 1], ROUND_NOT_NEEDED);
       div_2exp_assign_r(curr_minus_var_ub, curr_minus_var_ub, 1, ROUND_DOWN);
-      // Optimize the most common case: curr = +/-[1;1].
+      // Optimize the most common case: curr = +/-[1, 1].
       if (curr_lb == 1 && curr_ub == 1) {
         add_assign_r(result, result, std::max(curr_var_ub, curr_minus_var_ub),
                      ROUND_UP);
diff --git a/src/Sum_Floating_Point_Expression.defs.hh b/src/Sum_Floating_Point_Expression.defs.hh
index 2704d8270..fd0d4113a 100644
--- a/src/Sum_Floating_Point_Expression.defs.hh
+++ b/src/Sum_Floating_Point_Expression.defs.hh
@@ -84,7 +84,7 @@ void swap(Sum_Floating_Point_Expression<FP_Interval_Type, FP_Format>& x,
   \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}
   \right)
   \aslf
-  mf_{\mathbf{f}}[-1;1]
+  mf_{\mathbf{f}}[-1, 1]
   \f]
   where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the linear form computed by
   calling method <CODE>Floating_Point_Expression::relative_error</CODE>
diff --git a/src/Variable_Floating_Point_Expression.defs.hh b/src/Variable_Floating_Point_Expression.defs.hh
index 53491fb20..9c7c8d1b0 100644
--- a/src/Variable_Floating_Point_Expression.defs.hh
+++ b/src/Variable_Floating_Point_Expression.defs.hh
@@ -58,7 +58,7 @@ void swap(Variable_Floating_Point_Expression<FP_Interval_Type, FP_Format>& x,
   \rrbracket\f$, we construct the interval
   linear form \f$\linexprenv{v}{\rho^{\#}}{\rho^{\#}_l}\f$ as
   \f$\rho^{\#}_l(v)\f$ if it is defined; otherwise we construct it as
-  \f$[-1;1]v\f$.
+  \f$[-1, 1]v\f$.
 */
 template <typename FP_Interval_Type, typename FP_Format>
 class Variable_Floating_Point_Expression
diff --git a/src/linearize.hh b/src/linearize.hh
index ec24bb566..9e8de89a3 100644
--- a/src/linearize.hh
+++ b/src/linearize.hh
@@ -90,7 +90,7 @@ namespace Parma_Polyhedra_Library {
   \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}
   \right)
   \aslf
-  mf_{\mathbf{f}}[-1;1]
+  mf_{\mathbf{f}}[-1, 1]
   \f]
   where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the relative error
   associated to \f$l\f$ (see method <CODE>relative_error</CODE> of
@@ -196,7 +196,7 @@ add_linearize(const Binary_Operator<Target>& bop_expr,
   \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}
   \right)
   \aslf
-  mf_{\mathbf{f}}[-1;1]
+  mf_{\mathbf{f}}[-1, 1]
   \f]
   where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the relative error
   associated to \f$l\f$ (see method <CODE>relative_error</CODE> of
@@ -284,35 +284,35 @@ sub_linearize(const Binary_Operator<Target>& bop_expr,
   \left(i \amifp i'\right)
   + \sum_{v \in \cV}\left(i \amifp i'_{v}\right)v.
   \f]
-  Given an expression \f$[a;b] \otimes e_{2}\f$ and a composite
+  Given an expression \f$[a, b] \otimes e_{2}\f$ and a composite
   abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
   \rrbracket\f$, we construct the interval linear form
-  \f$\linexprenv{[a;b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}\f$
+  \f$\linexprenv{[a, b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}\f$
   as follows:
   \f[
-  \linexprenv{[a;b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}
+  \linexprenv{[a, b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}
   =
-  \left([a;b]
+  \left([a, b]
   \amlf
   \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}\right)
   \aslf
-  \left([a;b]
+  \left([a, b]
   \amlf
   \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}
   \right)\right)
   \aslf
-  mf_{\mathbf{f}}[-1;1].
+  mf_{\mathbf{f}}[-1, 1].
   \f].
 
-  Given an expression \f$e_{1} \otimes [a;b]\f$ and a composite
+  Given an expression \f$e_{1} \otimes [a, b]\f$ and a composite
   abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
   \rrbracket\f$, we construct the interval linear form
-  \f$\linexprenv{e_{1} \otimes [a;b]}{\rho^{\#}}{\rho^{\#}_l}\f$
+  \f$\linexprenv{e_{1} \otimes [a, b]}{\rho^{\#}}{\rho^{\#}_l}\f$
   as follows:
   \f[
-  \linexprenv{e_{1} \otimes [a;b]}{\rho^{\#}}{\rho^{\#}_l}
+  \linexprenv{e_{1} \otimes [a, b]}{\rho^{\#}}{\rho^{\#}_l}
   =
-  \linexprenv{[a;b] \otimes e_{1}}{\rho^{\#}}{\rho^{\#}_l}.
+  \linexprenv{[a, b] \otimes e_{1}}{\rho^{\#}}{\rho^{\#}_l}.
   \f]
 
   Given an expression \f$e_{1} \otimes e_{2}\f$ and a composite
@@ -474,28 +474,28 @@ mul_linearize(const Binary_Operator<Target>& bop_expr,
   \left(i \adivifp i'\right)
   + \sum_{v \in \cV}\left(i_{v} \adivifp i'\right)v.
   \f]
-  Given an expression \f$e_{1} \oslash [a;b]\f$ and a composite
+  Given an expression \f$e_{1} \oslash [a, b]\f$ and a composite
   abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
   \rrbracket\f$,
   we construct the interval linear form
   \f$
-  \linexprenv{e_{1} \oslash [a;b]}{\rho^{\#}}{\rho^{\#}_l}
+  \linexprenv{e_{1} \oslash [a, b]}{\rho^{\#}}{\rho^{\#}_l}
   \f$
   as follows:
   \f[
-  \linexprenv{e_{1} \oslash [a;b]}{\rho^{\#}}{\rho^{\#}_l}
+  \linexprenv{e_{1} \oslash [a, b]}{\rho^{\#}}{\rho^{\#}_l}
   =
   \left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l}
   \adivlf
-  [a;b]\right)
+  [a, b]\right)
   \aslf
   \left(\varepsilon_{\mathbf{f}}\left(
   \linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l}
   \right)
   \adivlf
-  [a;b]\right)
+  [a, b]\right)
   \aslf
-  mf_{\mathbf{f}}[-1;1],
+  mf_{\mathbf{f}}[-1, 1],
   \f]
   given an expression \f$e_{1} \oslash e_{2}\f$ and a composite
   abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right