/usr/share/doc/libapron-dev/html/apron_5.html is in libapron-dev 0.9.10-6.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 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 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 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 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html401/loose.dtd">
<html>
<!-- Created on December 25, 2013 by texi2html 1.82
texi2html was written by:
Lionel Cons <Lionel.Cons@cern.ch> (original author)
Karl Berry <karl@freefriends.org>
Olaf Bachmann <obachman@mathematik.uni-kl.de>
and many others.
Maintained by: Many creative people.
Send bugs and suggestions to <texi2html-bug@nongnu.org>
-->
<head>
<title>APRON 0.9.10: Functionalities of the interface at level 0</title>
<meta name="description" content="APRON 0.9.10: Functionalities of the interface at level 0">
<meta name="keywords" content="APRON 0.9.10: Functionalities of the interface at level 0">
<meta name="resource-type" content="document">
<meta name="distribution" content="global">
<meta name="Generator" content="texi2html 1.82">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css">
<!--
a.summary-letter {text-decoration: none}
blockquote.smallquotation {font-size: smaller}
pre.display {font-family: serif}
pre.format {font-family: serif}
pre.menu-comment {font-family: serif}
pre.menu-preformatted {font-family: serif}
pre.smalldisplay {font-family: serif; font-size: smaller}
pre.smallexample {font-size: smaller}
pre.smallformat {font-family: serif; font-size: smaller}
pre.smalllisp {font-size: smaller}
span.roman {font-family:serif; font-weight:normal;}
span.sansserif {font-family:sans-serif; font-weight:normal;}
ul.toc {list-style: none}
-->
</style>
</head>
<body lang="en" bgcolor="#FFFFFF" text="#000000" link="#0000FF" vlink="#800080" alink="#FF0000">
<a name="Functionalities-of-the-interface-at-level-0"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="apron_4.html#General-choices" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="apron_6.html#Functionalities-of-the-interface-at-level-1" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="apron_3.html#APRON-Rationale-and-Functionalities" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="apron_3.html#APRON-Rationale-and-Functionalities" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="apron_7.html#APRON-Guidelines" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="apron.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[Contents]</td>
<td valign="middle" align="left">[<a href="apron_42.html#Appendices" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="apron_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Functionalities-of-the-interface-at-level-0-1"></a>
<h2 class="section">Functionalities of the interface at level 0</h2>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Representation-of-an-abstract-value">• Representation of an abstract value</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Semantics-of-an-abstract-value">• Semantics of an abstract value</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Dimensions">• Dimensions</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Other-datatypes">• Other datatypes</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Control-of-internal-representation">• Control of internal representation</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Printing">• Printing</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Serializaton_002fDeserialization">• Serializaton/Deserialization</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Constructors">• Constructors</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Tests">• Tests</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Property-extraction">• Property extraction</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Lattice-operations">• Lattice operations</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Assignement-and-Substitutions">• Assignement and Substitutions</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Operations-on-dimensions">• Operations on dimensions</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Other-operations">• Other operations</a></td><td> </td><td align="left" valign="top">
</td></tr>
</table>
<a name="Representation-of-an-abstract-value"></a>
<a name="Representation-of-an-abstract-value-1"></a>
<h4 class="subsubheading">Representation of an abstract value</h4>
<p>At the level 0 of the interface, an abstract value is a structure
</p><pre class="verbatim">struct ap_abstract0_t {
ap_manager_t *manager; /* Explicit context */
void *value; /* Abstract value representation
(only known by the underlying library) */
}
</pre><p>The context is allocated by the underlying library, and contains an
array of function pointers pointing to the function of the underlying
library. Hence, it indicates the effective type of an abstract value.
</p>
<p>The validity of the arguments of the functions called through the
interface is checked before the call to effective functions. In case
of problem, an <code>invalid_argument</code> exception is raised.
</p>
<a name="Semantics-of-an-abstract-value"></a>
<a name="Semantics-of-an-abstract-value-1"></a>
<h4 class="subsubheading">Semantics of an abstract value</h4>
<p>The semantics of an abstract value is a subset
</p><blockquote><p>X of N^p x R^q
</p></blockquote>
<p>Abstract values are typed according to their dimensionality
(p,q).
</p>
<a name="Dimensions"></a>
<a name="Dimensions-1"></a>
<h4 class="subsubheading">Dimensions</h4>
<p>Dimensions are numbered from 0 to p+q-1 and are typed either as
integer or real, depending on their rank w.r.t. the dimensionality of
the abstract value.
</p>
<blockquote><p><b>Note:</b> Taking into account or not the fact that some dimensions are integers
is left to underlying libraries. Treating them as real is still a
correct approximation. The behaviour of the libraries in this regard
may also depend on some options.
</p></blockquote>
<a name="Other-datatypes"></a>
<a name="Other-datatypes-1"></a>
<h4 class="subsubheading">Other datatypes</h4>
<p>In addition to abstract values, the interface also manipulates the
following main datatypes:
</p><dl compact="compact">
<dt> <em>scalar (number)</em></dt>
<dd><p>Either GMP multiprecision rationals or C <code>double</code>.
</p></dd>
<dt> <em>interval</em></dt>
<dd><p>composed of 2 scalar numbers. With rationals, plus (resp minus) infinity is represented by 1/0 (resp -1/0). With <code>double</code>, the IEEE754 is assumed and the corresponding standard representation is used.
</p></dd>
<dt> <em>coefficient</em></dt>
<dd><p>which is either a scalar or an interval.
</p></dd>
<dt> <em>(interval) linear expression</em></dt>
<dd><p>The term linear is used even if the proper term should rather be
affine. A linear expression is a linear expression in the common
sense, using only scalar numbers. A quasi-linear expression is a
linear expression where the constant coefficient is an interval. An
interval linear expression is a linear expression where any
coefficient may be an interval. In order to have a unique datatype for
these variations, we introduced the notion of coefficient described
above.
</p></dd>
<dt> <em>“linear” constraints</em> </dt>
<dd><p>“Linear” constraints includes proper linear constraints, linear
constraints in which the expression can be possibly an interval linear
expression, linear equalities modulo a number, and linear disequalities.
</p></dd>
<dt> <em>generators</em></dt>
<dd><p>A generator system for a subset of <em>X\subseteq R^n</em> is a finite
set of vectors, among which one distinguishes <em>points</em>
<em>p_0,\ldots,p_m</em> and <em>rays</em> <em>r_0,\ldots,r_n</em>, that
generates <em>X</em>:
</p><blockquote><p>X = { lambda0 p0 +...+ lambdaM pM + mu0 r0 +...+ muN rN | lambda0 +...+ lambdaN = 1 and forall J : muJ >= 0 }
</p></blockquote>
<p>The APRON datatype for generators distinguishes points (sum of
coefficients equal to one), rays (positive coefficients), lines (or
bidirectional rays, with unconstrainted coefficients), integer rays
(integer positive coefficients) and integer lines (integer
coefficients).
</p></dd>
</dl>
<a name="Control-of-internal-representation"></a>
<a name="Control-of-internal-representation-1"></a>
<h4 class="subsubheading">Control of internal representation</h4>
<p>We identified several notions:
</p>
<ul>
<li>
Canonical form
</li><li>
Minimal form (in term of space)
</li><li>
Approximation notion left to the underlying library (taking into
account integers or not, ...).
</li></ul>
<a name="Printing"></a>
<a name="Printing-1"></a>
<h4 class="subsubheading">Printing</h4>
<p>There are two printing operations:
</p>
<ul>
<li>
Printing of an abstract value;
</li><li>
Printing the difference between two abstract values.
</li></ul>
<p>The printing format is library dependent. However, the conversion of
abstract values to constraints (see below) allows a form of
standardized printing for abstract values.
</p>
<a name="Serializaton_002fDeserialization"></a>
<a name="Serializaton_002fDeserialization-1"></a>
<h4 class="subsubheading">Serializaton/Deserialization</h4>
<p>Serialization and deserialization of abstract values to a memory
buffer is offered. It is entirely managed by the underlying
library. In particular, it is up to it to check that a value read from
the memory buffer has the right format and has not been written by a
different library.
</p>
<p>Serialization is done to a memory buffer instead of to a file
descriptor because this mechanism is more general and is needed for
interfacing with languages like <small>OCAML</small>.
</p>
<a name="Constructors"></a>
<a name="Constructors-1"></a>
<h4 class="subsubheading">Constructors</h4>
<p>Four basic constructors are offered:
</p>
<ul>
<li>
bottom (empty) and top (universe) values (with a specified dimensionality);
</li><li>
abstraction of a bounding box;
</li><li>
abstraction of conjunction of linear constraints (in the broad sense).
</li></ul>
<a name="Tests"></a>
<a name="Tests-1"></a>
<h4 class="subsubheading">Tests</h4>
<p>Predicates are offered for testing
</p><ul>
<li>
emptiness and universality of an abstract value:
</li><li>
inclusion and equality of two abstract values;
</li><li>
inclusion of a dimension into an interval given an abstract value;
</li><li>
satisfaction of a linear constraint by the abstract value.
</li></ul>
<a name="Property-extraction"></a>
<a name="Property-extraction-1"></a>
<h4 class="subsubheading">Property extraction</h4>
<p>Some properties may be inferred given an abstract values:
</p>
<ul>
<li> Interval of variation of a dimension in an abstract value;
</li><li> Interval of variation of a linear expression in an abstract value;
</li><li> Conversion to a bounding box
</li><li> Conversion to a set of linear constraints (in the broad sense).
</li></ul>
<p>Notice that the second operation implements linear programming if it
is exact. The third operation is not minimal, as it can be implemented
using the first one, but it was convenient to include it. But the
fourth operation is minimal and cannot be implemented using the second
one, as the number of linear expression is infinite.
</p>
<a name="Lattice-operations"></a>
<a name="Lattice-operations-1"></a>
<h4 class="subsubheading">Lattice operations</h4>
<ul>
<li>
Least upper bound and greatest lower bound of two abstract values, and of arrays of abstract values;
</li><li>
Intersection with one or several linear constraints;
</li><li>
Addition of rays (for instance for implement generalized time elapse
operator in linear hybrid systems).
</li></ul>
<a name="Assignement-and-Substitutions"></a>
<a name="Assignement-and-Substitutions-1"></a>
<h4 class="subsubheading">Assignement and Substitutions</h4>
<ul>
<li>
of a dimension by a (interval) linear expression
</li><li>
in parallel of several dimensions by several (interval) linear expressions
</li></ul>
<p>Parallel assignement and substitution ar enot minimal operations, but
for some abstract domains implementing them directly results in more
efficient or more precise operations.
</p>
<a name="Operations-on-dimensions"></a>
<a name="Operations-on-dimensions-1"></a>
<h4 class="subsubheading">Operations on dimensions</h4>
<ul>
<li>
Projection/Elimination of one or several dimensions with constant
dimensionality;
</li><li>
Addition/Removal/Permutation of dimensions with corresponding change
of dimensionality (with the exception of permutation). These
operations allows to resize abstract values, and reorganize
dimensions.
</li><li>
Expansion and folding of dimensions. This is useful for the
abstraction of arrays, where a dimension may represent several
variables.
</li></ul>
<a name="Other-operations"></a>
<a name="Other-operations-1"></a>
<h4 class="subsubheading">Other operations</h4>
<p>Widening, either simple or with threshold, is offered. A generic
widening with threshold function is offered in the interface.
</p>
<p>Topological closure (i.e., relaxation of strict inequalities) is
offered.
</p>
<hr size="6">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="apron_4.html#General-choices" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="apron_6.html#Functionalities-of-the-interface-at-level-1" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="apron_3.html#APRON-Rationale-and-Functionalities" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="apron_3.html#APRON-Rationale-and-Functionalities" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="apron_7.html#APRON-Guidelines" title="Next chapter"> >> </a>]</td>
</tr></table>
<p>
<font size="-1">
This document was generated on <i>December 25, 2013</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
</font>
<br>
</p>
</body>
</html>
|