Editing Abstract interpretation (section)

===Numerical abstract domains===

One can assign to each variable <math>x</math> available at a given program point an interval <math>[L_{x}, H_{x}]</math>. A state assigning the value <math>v(x)</math> to variable <math>x</math> will be a concretization of these intervals if, for all <math>x</math>, we have <math>v(x) \in [L_{x}, H_{x}]</math>. From the intervals <math>[L_{x}, H_{x}]</math> and <math>[L_{y}, H_{y}]</math> for variables <math>x</math> and <math>y</math>, respectively, one can easily obtain intervals for <math>x + y</math> (namely, <math>[L_{x}+L_{y}, H_{x}+H_{y}]</math>) and for <math>x - y</math> (namely, <math>[L_{x} - H_{y}, H_{x} - L_{y}]</math>); note that these are ''exact'' abstractions, since the set of possible outcomes for, say, <math>x+y</math>, is precisely the interval <math>[L_{x}+L_{y}, H_{x}+H_{y}]</math>. More complex formulas can be derived for multiplication, division, etc., yielding so-called [[interval arithmetic]]s.<ref>{{cite book |first1=Patrick |last1=Cousot  |first2=Radhia |last2=Cousot | contribution=Static determination of dynamic properties of programs | title=Proceedings of the Second International Symposium on Programming | publisher=Dunod, Paris, France | pages=106–130 | year=1976 |contribution-url=https://www.di.ens.fr/~cousot/COUSOTpapers/publications.www/CousotCousot-ISOP-76-Dunod-p106--130-1976.pdf}}</ref>

Let us now consider the following very simple program:
<pre>
y = x;
z = x - y;
</pre>
{| style="float:right"
| [[File:Combination of abstract domains.svg|thumb|Combination of [[interval arithmetic]] ({{color|#00ff00|green}}) and congruence mod 2 on integers ({{color|#00ffff|cyan}}) as abstract domains to analyze a simple piece of [[C (programming language)|C]] code ({{color|#ff8080|red}}: concrete sets of possible values at runtime). Using the congruence information ({{color|#00ffff|0}}=even, {{color|#00ffff|1}}=odd), a [[Zero division#In computer arithmetic|zero division]] can be excluded. (Since only one variable is involved, relational vs. non-relational domains is not an issue here.)]]
|}
{| style="float:right"
| [[File:3dpoly.svg|thumb|A 3-dimensional convex example polyhedron describing the possible values of 3 variables at some program point. Each of the variables may be zero, but all three can't be zero simultaneously. The latter property cannot be described in the interval arithmetics domain.]]
|}
With reasonable arithmetic types, the result for {{samp|z}} should be zero. But if we do interval arithmetic starting from {{samp|x}} in [0, 1], one gets {{samp|z}} in [−1, +1]. While each of the operations taken individually was exactly abstracted, their composition isn't.

The problem is evident: we did not keep track of the equality relationship between {{samp|x}} and {{samp|y}}; actually, this domain of intervals does not take into account any relationships between variables, and is thus a ''non-relational domain''. Non-relational domains tend to be fast and simple to implement, but imprecise.

Some examples of ''relational'' numerical abstract domains are:
* [[congruence relation#Basic example|congruence relations]] on integers<ref>{{cite journal |first=Philippe |last=Granger | title=Static Analysis of Arithmetical Congruences | journal=International Journal of Computer Mathematics | volume=30 |issue=3–4 | pages=165–190 | year=1989 | doi=10.1080/00207168908803778}}</ref><ref>{{cite book | author=Philippe Granger | contribution=Static Analysis of Linear Congruence Equalities Among Variables of a Program |editor-first=S. |editor-last=Abramsky |editor2-first=T.S.E. |editor2-last=Maibaum | title=Proc. Int. J. Conf. on Theory and Practice of Software Development (TAPSOFT) | publisher=Springer | series=Lecture Notes in Computer Science | volume=493 | pages=169–192 | year=1991 }}</ref>
* convex [[polyhedra]]<ref>{{cite book |first1=Patrick |last1=Cousot |first2=Nicolas |last2=Halbwachs | contribution=Automatic Discovery of Linear Restraints Among Variables of a Program | title=Conf. Rec. 5th ACM Symp. on Principles of Programming Languages (POPL) | pages=84–97 | contribution-url=https://www.di.ens.fr/~cousot/publications.www/CousotHalbwachs-POPL-78-ACM-p84--97-1978.pdf | date=January 1978 }}</ref> (cf. left picture) – with some high computational costs
* difference-bound matrices<ref>{{cite book |first=Antoine |last=Miné | chapter=A New Numerical Abstract Domain Based on Difference-Bound Matrices
| title=Programs as Data Objects, Second Symposium, (PADO)|date=2001 | volume=2053| pages=155–172| publisher=Springer |editor-first=Olivier |editor-last=Danvy |editor2-first=Andrzej |editor2-last=Filinski |series=Lecture Notes in Computer Science | arxiv=cs/0703073}}</ref>
* "octagons"<ref>{{cite thesis | type=Ph.D. thesis |first=Antoine |last=Miné | title=Weakly Relational Numerical Abstract Domains | institution=Laboratoire d'Informatique de l'École Normale Supérieure | url=https://www.di.ens.fr/~mine/these/these-color.pdf | date=Dec 2004 }}</ref><ref>{{cite journal | author=Antoine Miné | title=The Octagon Abstract Domain | journal=Higher Order Symbol. Comput. | volume=19 | number=1 | pages=31–100 | year=2006 | doi=10.1007/s10990-006-8609-1| arxiv=cs/0703084 }}</ref><ref>{{cite journal |first1=Robert |last1=Clarisó |first2=Jordi |last2=Cortadella |author2-link=Jordi Cortadella| title=The Octahedron Abstract Domain | journal=Science of Computer Programming | volume=64 | pages=115–139 | year=2007 | doi=10.1016/j.scico.2006.03.009| hdl=10609/109823 | hdl-access=free }}</ref>
* linear equalities<ref>{{cite journal | author=Michael Karr | title=Affine Relationships Among Variables of a Program | journal=Acta Informatica | volume=6 | issue=2 | pages=133–151 | year=1976 | doi=10.1007/BF00268497| s2cid=376574 }}</ref>
and combinations thereof (such as the reduced product,<ref name="CCPOPL79"/> cf. right picture).

When one chooses an abstract domain, one typically has to strike a balance between keeping fine-grained relationships, and high computational costs.