算术表达式的合成与优化技术

可在www.sciencedirect.com在线获取理论计算机科学电子笔记287（2012）3-16www.elsevier.com/locate/entcs准确评价算术表达式（特邀演讲）Matthieu Martela，b，c，1aUniversit'edePerpignanViaDomitia，Digits，ArchitecturesetLogicielsInformatiques52avenue Paul Alduy，F-66860，Perpignan，FrancebUniversit'eMontpellierIILaboratoirecCNRS，Laboratoire摘要在这篇文章中，我们专注于算术表达式的合成，可以有效地在计算机上进行评估，在这个意义上，他们不创建超过流，是准确的，不使用不必要的资源。我们考虑几个计算机算术的整数，浮点数和定点数和区间，我们展示了如何合成新的表达式，数学上等价于原来的和更有效的。我们的方法是基于抽象的解释。 我们引入了两个抽象来表示在多项式大小的数学等价表达式集。 然后，我们提取优化表达式通过在包含在抽象结构中的表达式中搜索最准确的表达式。我们专注于合成的正确性，其中包括显示，新的表达式不能区分源表达式时，使用观察抽象保留字：抽象解释，代码合成，计算机算术。1引言在过去的十年中，基于抽象解释的静态分析技术[2]已达到成熟的工业水平。如Astr'ee[8]、Clousot[9]或 Fluctuat [4]等已成功用于实际案例研究。这些工具能够计算代码的细微属性，例如浮点变量的精确范围。然而，当检测到程序的运行时错误或意外行为时，这些工具并不指示如何修复代码。然后，这项工作的一个自然扩展是向程序员提出错误更正这些技术1电子邮件：univ-perp.fr1571-0661© 2012 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.09.0024M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）3最近被提出来修复整数表达式和整数表达式之间的关系[10]，并提高浮点表达式的精度[11]。在这篇文章中，我们集中在表达式的合成非常适合于计算机运算的意义上，他们的评估是有效的，准确的，不增加运行时的错误。我们认为程序员在源代码中编写的表达式是数学公式，如果计算机使用精确的算术（数学整数或实数），则会返回预期的结果然后，我们合成新的表达式，这些表达式在数学上等价于原始表达式，并且在计算机算法中的评估引起较少的误差。我们考虑四种计算机算法：整数算法受到过流的影响，在某些情况下可以避免表达式的变换[10]。除了过舍入之外，由于运算的舍入，浮点运算[1，14]还存在精度问题。如果用数学上等价的表达式来代替表达式，可以提高表达式的精度[11，6]。在固定点算法[5]中，表达式的等价版本的求值可能需要更多或更少的资源，这取决于中间结果的大小。最后，区间算术[12]引入了过度近似，因为变量之间缺乏关系。在许多情况下，这些过度近似可以通过源表达式的变换来限制。我们的工作是基于P。和R.Cousot我们引入非标准的语义和观察抽象的整数，浮点，定点和区间算术。如果综合产生了一个新的表达式，当使用观察抽象时，它不能与源表达式区分开来，那么它就是因为通常存在太多数学上等价于源表达式的表达式，所以我们提出了等价表达式集合的两个抽象[11，6]。最后，合成包括从等价表达式的抽象集合中选择表达式这种选择是基于对这四种算法的非标准语义的抽象解释。本文的组织结构如下。在第2节中，我们介绍了计算机算法，并为每一个，我们讨论了如何合成一个新的等价表达式可能会提高评估。第3节是专门的合成的正确性。它介绍了非标准语义和观察抽象。在第4节中，我们描述了等价表达式集合的抽象。最后，第5节和第6节总结了合成本身。2计算机算术和表达式合成在本节中，我们将回顾几种计算机算法，并为每一种算法介绍如何合成可以有效计算的表达式。我们从最简单的算术开始，也就是整数算术。 然后讨论 最后，我们通过考察区间算术的情况来M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）35M<$（a+b−（m−1））如果a+bm33有符号整数运算使人们能够精确地表示最小值m和最大值M之间的任何整数。例如，在许多语言中，int格式对应于m= −231和M= 231− 1之间的整数。当某个操作的结果在区间[m，M]之外时，它会环绕这个区间。正如F. Logozzo和T. Ball提出了整数表达式和关系的代码修复[10]。形式上，基本操作定义为：b=⎧⎪⎨m⊕(a+b−(M+1))ifa+b>M中国a+b否则b=a<$（a<$（b−1））如果b≥1−a（a（−b−1））ifb 1（一）例如，对于32位有符号整数，如果x = 2 30且y = −215，则2 ×x+ y=−715860650， 2 ×x+ y = 715795114。这两个表达式在数学上是等价的，而最接近精确结果的整数是715795115。因为，在有符号整数算术中，当中间结果在范围[m，M]之外时可能出现错误，所以表达式的合成必须生成在数学上与原始表达式等价的表达式，并且其求值引入了绝对值最小的中间结果。浮点运算由IEEE754标准定义[1]。浮点数用于对实数进行编码.然而，由于它们是数学表兄弟的有限表示，因此在计算过程中会出现舍入误差，并且在某些情况下，这些近似值可能会严重伪造评估结果浮点数x定义为：x = s·（d0.d1. d p−1）·β e= s·m·β e−p+1（2）其中s∈ {− 1，1}是符号，m = d0d1. dp−1是尾数，数字0≤d i<β，0 ≤ i ≤ p − 1，p是精度，e是指数，e min≤ e ≤ e max。IEEE754标准通过提供p、β、e min和e max的特定值，指定了几种格式的浮点数。它还定义了一些舍入模式，以ds+∞，−∞，0和最接近。L让我们写<$+∞，<$−∞，<$0，◦除了舍入函数之外，IEEE 754标准通过以下方式定义了基本运算的语义：x②ry=<$r（x<$y）（3）其中，②r表示使用舍入模式r计算的浮点运算+、−、×或，表示精确运算。由于舍入误差，计算结果不准确。 例如，值e = 2。7182818 可以使用Bernouilli公式计算e= limn→+∞ n与n=一加一n，n≥ 0。在双精度中，u8= 2。718282，但精度随着n的增长而降低u14 = 2。716110，u16 = 3。0。35035和u17 = 1。0. 对于浮点运算，、Σn.6M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）3j=2Σ、、j=w−jx x x 6X 3 x 33，3 3，33，3 3，34，44，412.6公斤图1.一、x 2 − 6 x + 9的两个固定d-点实现，其中rex格式为105，3。表达式的合成在于生成数学上等于原始表达式并且使结果上的舍入误差最小化的表达式，即， 的距离|r−r|在精确结果r和近似结果r之间。目前还不存在与IEEE754标准相当的定点算法标准。固定点格式w，i取决于用于编码值的位w的总数以及固定点相对于最高有效位的位置[5]。一般来说，这些数字是使用二的补码和位序列b w-1.来编码的。 . b0表示值−bw−1·2i−1+bw−j·2i，两个连续数之间的距离为2 i−w。初等运算结果的格式w r，i r取决于其操作数的格式w1，i1和w2，i2：加法：wr=ir+max（w1−i1，w2−i2）ir=max（i1+<$s1<$s2，i2+<$s2<$s1）+1产品名称：wr=w1+w2ir=i1+i2（四）在等式（4）中，s1和s2表示操作数的符号。使用等式（4）的格式，运算是精确的并且不需要舍入为定点算术合成一个有效的表达式包括生成一个等价于原始表达式的表达式，它最小化实现的大小，或者换句话说，它最小化中间结果（运算符的输出）格式的大小w之和例如，图1显示了多项式x2−x +9的两种实现，其中x的格式为5，3。第一种方案对应于直接实现，需要68位来存储中间结果，而第二种方案实现等效公式（x −3）×（x − 3），只需要40位。我们最后的计算机算法是区间算术[12]。区间通常用来限定用离散点数进行计算的精确结果.给定两个区间[x，x]和[y，y]，其界是两个点5，3公斤5，3公斤4，4 4，410，6公斤9.7公斤12，8公斤95.5公斤13，9美元M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）37⎪⎩⎪⎭⎪⎩⎪⎦⎭−⎣数字，基本运算定义为：⎢⎡⎧⎪⎨x⊗−∞y⎫⎪⎬⎧⎪⎨x⊗+∞y⎫⎪⎬⎤⎥[x，x]<$[y，y]=[x<$−∞y，x<$+∞y][x，x]<$[y，y]=<$minx−∞y，maxx+∞y（五）x−∞yx−∞yx+∞yx+∞y区间算术支持从变量的decorellation（缺乏关系）和包装效果。例如，由于去相关，函数f（x）= x的 值 是[1. 当x=[3， 4]时，然而，函数x−22f在数学上等于g（x）= 1+x2和g（[3，4]）=[2，3]。虽然这两个结果如果是正确的，g（[3，4]）显然比f（[3，4]）更准确。然后，为区间算术合成高效表达式包括生成表达式，其评估产生小宽度的区间，以优化结果的准确性。3合成的正确性合成的表达式可能与原始表达式非常不同我们使用的程序转换的框架介绍了P和R。Cousot [3].在图2中，我们为表达式的求值引入了四种非标准的小步操作语义，其中，“代表任何基本操作。 这些语义记为→in t、→float t、→fixed和→[]，它们分别与整数、浮点、定点和区间算术有关。对于t中的i ntegerarithmetic→，非标准值是一对（v_n，v）∈int×Z，其中int表示计算机有符号整数的集合（例如32位或64位整数），Z表示有符号整数的集合。直观地说，一个valuee（v，v）g是由精确的value和它的计算机近似v alue组成的。的状态整数非标准语义的表达式e，m，ρ∈Expr×N×Envint由一个将变量映射到非标准值的表达式e，fntρ：Var→（int×Z）ofEnvint和一个非负整数m∈N组成，m ∈ N表示在表达式求值过程中遇到的绝对值的最大值。在合成新表达式的过程中，必须最小化整数m，以使中间结果保持在第2节中介绍的范围[m，M]内。对于浮点数→浮点数的迭代算法，非标准值是一对（v_i，v）∈float×R，其中float是浮点数的集合（IEEE754格式之一），R是实数的集合。在图2中，我们假设使用四舍五入模式进行浮点运算。的状态非标准浮点语义的εe，ρε由表达式e和环境ρ ∈ Var →（float × R）组成，环境ρ将变量映射到非标准值。直观地说，一个有效的浮点运算表达式的综合必须使数量最小化|v−v|，即， 计算机与精确结果之间的差异。对于不动点算术→nd，非标准值是一对（vw，i，v）∈fixed×R，其中fixed表示定点数的集合我们认为，在⎥8M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）312112（1）A =（1）A =（1）A=（|v|（m）x，m，ρ2019- 05 - 22 01：02：03 02：0302：04 03 02：03 0 |v1|、|v2|、|v|（m）<$（v<$1，v1）<$（v<$2，v2），m，ρ<$→int<$（v<$，v），mJ，ρ<$n=max（m，mJ），N= max（m，mJ）e1n = max（m，m），n=max（m，mJ），N= max（m，mJ）（vρ（x）=（v，v）x，ρE1，ρv=v1②v2v=v1v2（ve2，ρe1ρ（x）=（v<$w，i<$，v）x，W，ρvw，i=vw1，i1②vw2，i2v=v1<$v2WJ=W+w1+w2+w<$（v<$w1，i1<$$>，v1）<$（v<$w2，i2<$，v2），W，ρ<$→固定<$（v<$w，i<$，v）， WJ，ρ<$1 2e1，W，ρe1e2，W，ρ<$（v<$w1，i1<$，v1）<$e2，W，ρ<$→固定<$（v<$w1，i1<$，v1）<$eJ， WJ，ρ<$ρ（x）=（v，v）x，ρE1，ρv=v1v2v={xy：x∈v1，y∈v2}（vE2，ρe1图二、整 数 、浮点、定点和区间算术的非标准语义。固定，每个定点数都有自己的格式，如第节中所介绍的二、一个状态e，W，ρ∈ Expr ×N×Env固定由一个表达式e，一个非负整数W和一个环境ρ ∈ Var →（固定× R）映射变量组成非标准值。直观地说，W记录了在表达式求值期间表示所有中间结果所需的总位数。固定点算法的新表达式的合成必须使W最小化。最后，给出了整数算术的一个非标准 值（ v_∞，v ） ∈ （float×float）×v_∞（R），它是由一个有界的整数值v_∞和R的一个子集v构成的（v_∞（R）表示R的幂集）. 直观地说，v用于计算精确的M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）39属于输入区间的点的图像。换句话说，如果e（x，y）是依赖于两个变量x∈[a，b]和y∈[c，d]的表达式，我们的目标是在非标准语义中计算精确图像I={e（x，y）：a≤x≤b，c≤y≤d}10M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）3.Σ1212大肠对于区间算术，新表达式的合成必须使计算结果所对应的区间宽度给定一个n个整数的集合Θ，收集语义[e]]intΘ，[e]]floatΘ，[[e]]fixedθ和[[e]][]θ对应于从状态{e，0，ρ∈ θ}开始的最大迹的集合，对于整数算术，{e，ρ∈：ρ∈Θ}，对于浮点算术，{e，0，ρ∈：ρ∈θ}，对于定点算术，以及{εe，ρε：ρ∈Θ}为区间算术。为了定义综合的正确性，我们还引入了状态的观测抽象α O[3]。如果对于任何Θ，[e]] Θ = S，[[eJ]] Θ = SJ且{αO（s）：s∈S}={αO（sJ）：sJ∈SJ}，则用另一个表达式e j替换表达式e是正确的，其中[e]Θ是我们的四个收集语义之一。对于表达式的综合，观测抽象抛弃了状态的计算机结果，只保留数学结果。然后，如果新表达式总是返回与源表达式相同的数学结果，则合成是正确的在我们所有的语义中，v是对（v，v），其中v是在机器，V是数学值。 我们定义αO为第二投影，即αO（vθ，v） =v，对于一个非标准语义。 然后，抽象αO通过将值投影到表达式和环境中而扩展到状态4等价表达式一般来说，通过结合性、交换性、分配性和因子分解等价于原始表达式e的表达式的数量与e的大小成指数关系。例如，计算多项式的方法的数量（x−1）×.. . ×（x−1）等于2。3·10 6（n = 5和1）。3· 109，n= 6 [13]。在这一秒-`nttouimummesx的作用，我们介绍了两个抽象，多项式的大小，数学上的集合，等价表达式。第一个抽象包括识别语法树在深度k上相等的表达式。这种抽象是[11]中所介绍的抽象的简化版本在本文中，我们引入了等价表达式集的欠近似，而在[11]是数学等价表达式的完整覆盖因为我们把自己限制在语法树在深度上相等的表达式上k，应用代数定律如结合性、交换性等产生与用户定义的参数k相关的有限数量的表达式。我们首先引入一个特殊的表达式T ∈ Expr和函数。’v' k = v如果 k≥ 0e1e2' 0 = T若 k= 0x ' k = x如果k≥0ee' k = e ' k −1 e ' k −1如果k≥1（6）设RExpr× Expr是表达式集合上的二元关系我们使用R来识别数学上等价的表达式。例如，R可以包含M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）311××+++□C×B×+C b一一一+（a，a，b）.Σ×× c2图3.第三章。 表达式e=的APEG。（a+a）+c<$×c.结合性或分配性：. .e1+（e2+e3），（e1+e2）+e3∈：e1，e2，e3∈Expr∞R（7）.e1×（e2+ e3），e1× e2+ e1× e3 ：e1，e2，e3∈指数代数R（8）注意，我们不要求R是传递的。为了生成与源表达式e等效的表达式的子集，我们使用方程（9）的转换k，其将状态k ∈E，K∈E（Expr）×E（Expr）联系起来：e∈EeRe′e′E，K.（九）使用方程（9）和初始状态ε {e}，{ee1集合E是数学上等价于e的表达式集合的欠近似。第二个抽象是基于抽象程序等价图（Abstract Program Equivalence Graph，简称APEG）的概念。APEGs是R. Tate等人 [15，16]。APEG归纳定义如下：(i) 值v或变量x是APEG，(ii) 表达式p1<$p2是一个APEG，其中p1和p2是APEG，并且n是一个二元运算符，(iii) 一盒是一个APEG，其中，算子和pi，1≤i≤n，是APEG，(iv) 一个非空集合{p1，...，p n}是一个APEG，其中p i，1 ≤i≤n，本身不是一组APEG。 集合{p1，...，p n}称为等价类。图3给出了APEG的示例。当等价类（在图3中由虚线椭圆表示）包含许多APEGp1，.，p n那么其中一个p i可以选择1≤i≤n以构建表达式。 一盒（p1，.， pn）（p1，.， pn）12M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）3.- 是的- 是的Σ×××.- 是的- 是的Σ×× × ×.Σ，。- 是的Σ2表示表达式p 1的任何解析. 不规则的;从实现的角度来看，当几个等效表达式共享一个公共子表达式时，后者在APEG中仅表示一次。然后，APEG提供了一组等价表达式的紧凑表示，并且使得可以在唯一结构中表示非常不同形状的许多等价表达式。出于可读性的原因，在图3中，对应于变量a，b和c的叶子是重复的，而实际上，它们在结构中只定义了一次包含在APEGp中的表达式集合A（p）归纳定义如下：(i) 如果p是值v或变量x，则A（p）={v}或A（p）={x}，(ii) 如果p是一个表达式p1<$p2，则A（p）=e1∈A（p1），e2∈A（p2）e1<$e2，(iii) 如果p是一个盒子则A（p）包含e 1的所有解析. ∗en对所有的e1∈ A（p1），.，en∈ A（pn），(iv) 如果p是一个等价类{p1，...，pn}则A（p）=1 ≤i≤nA（pi）.例如，图3的APEGp表示以下所有表达式：A（p）=10000⎪（a + a）+bc，（a + b）+ac，（b+a）+a c，（2a）+b c，c（a+a）+b，c（a+b）+a，c×。（b+a）+a，c×. （2×a）+b，（a+a）×c+b×c，⎫⎪⎬⎪（十）（2×a）×c+b×c，b×c+（a+a）×c，b×c+（2×a）×c相比之下，与本节开始时介绍的第一个抽象相比，可以通过以下集合来近似等价于e=c×（a+a）+b和设置S1=.c×。（a+a）+b，c×（a+a）+c×b如果k=1，（11）S=（a + a）+b×c，a+（a + b） ×c，（a+a）×c+b×c，a×c+（a+b）×c，如果k = 2。（十二）在他们关于EPEG的文章中，R. Tate等人使用重写规则将结构扩展到饱和状态[15，16]。在我们的上下文中，这样的规则将包括在现有的APEGp中执行一些模式匹配，然后在p中添加新的节点，一旦模式被识别。例如，图4中给出了与分配性和盒子构造相对应的规则。APEG构造的替代技术是使用专用算法。这样的算法，在多项式时间内工作，已经在[6]中提出本节前面定义的抽象不会引入与源表达式在数学上不等价的表达式然后，对于综合，选择任何属于一组等价表达式的抽象的表达式是正确的第节讨论了合成时使用的选择标准五、 我们通过形式化抽象的正确性来结束这一节。设R Expr×Expr是本节前面介绍的表达式集上的二元关系，以确定数学上等价的表达式（参见等式（p1，.， pn）M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）31312n（p1，...，p n，p' 1，...，p' m）×+ p3+ p3× ×p1p2✳p1p2p1p3p2p3第3章p1p2图四、 用模式匹配法构造APEG的一些规则（7）和（8））。等价于原始表达式e的表达式集合可以通过以下规则生成：e∈EeRe′E→ {e′}E（十三）使用包含在R中的关系等价于e的表达式的集合E（e）使得转移序列{e}→ E（e）是最大的（即E（e）→EJ意味着EJ=E（e））。令A（p）是包含在例如使用图4的规则从e构建的APEG p内的表达式的集合则E和A（p）是E（e）的欠近似，并且在等价表达式集和它的抽象之间存在以下伽罗瓦联系：γ⊕℘(Expr),⊆⟩←−−α−1−→−⊕℘(Expr)×℘(Expr),⊆×⟩(14)γ⊕℘(Expr),⊆⟩←−−α−2−→−⊕Π,⊆Π⟩(15)在方程（14）和（15）中，×表示分量包含，表示APEG的集合，是APEG上的偏序。直觉上，如果A（p1）<$A（p2），则p 1 <$p 2。在[ 6 ]中给出了一个归纳的定义。抽象状态的具体化由以下函数定义：γ1（λE，Kλ）=E′和γ2（p）=E′。（十六）e∈E，{e}→E'e∈A（p），{e}→E'因此，抽象集合E、K和p不包含在数学上与其他集合不等价的表达式，并且E或A（p）中的任何表达式eJ 因为它不能用第3节介绍的观测抽象αO从e中推导出来。×+（p1，p2，p3）（p1，（p'1，，14M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）3intint1固定整数 2浮子1浮体2固定1固定2[]1[]2[]1[]2（[v（1）A =（1）A=（|v|、|v|（m）x，m，ρ[1][2][3][4][5][6][7][8][9][10][11|v1|、|v1|、|v2|、|v2|、|v|、|v|（m）n [v1，v1]n[v2，v2]，m，ρn →n [v，v]，mJ，ρne1，m，Ρe1e2，m，Ρn [v1，v1]n=2，m，ρn→intn [v1，v1]n=2，M，ρnρ（x）=（[v，v]，[v，v]）第1节，ρρ →eJ，ρx，ρe1eJ1[v，v]=[v1，v1][v2，v2][v，v]=[v1，v1]↓[v2，v2]e2，ρ（[vρ（x）=[v，v]w，ie1，W，ρeJ，WJ，ρx，W，ρe1eJ1[v，v]w，i=[v1，v1]w1，i1 固定[v2，v2]w2，i2WJ=W+w1+w2+w<$[v1，v1]<$w1，i1<$$>[v2，v2]<$w2，i2<$，W，ρ<$→<$[v，v]<$w，i<$， WJ，ρ<$固定e2，W，ρ[v1，v1]2ρ（x）= [v，v][v，v] = [v1，v1]参与[v2，v2]x，ρ第1节，ρρ →ej，ρe1eJ图五、整 数 、浮点、定点和区间算术的抽象语义。5新表达本节涉及合成的最后一步，包括在等效表达式的抽象表示首先，我们在图5中引入抽象语义，以比较数学上等价的表达式的质量。这些语义抽象了图2的非标准语义，其中数学值已被丢弃。抽象状态包含区间而不是标量值，因为我们的目标是合成针对大范围输入优化的M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）315intintintρint浮子↓ΣΣ浮子浮子ρρ固定固定固定2[][][]1int21int11111112221浮子2121固定11112固定抽象整数语义的值→是一个区间[v，v]∈int×int抽象状态是一个三重态e，m，ρ∈Expr×int×Env，其中Env是将变量映射到抽象整数值的环境集。操作员int表示整数区间之间的运算，不舍入在这种情况下是必需 表达式e1优于表达式e2，∗抽象环境ρ，记为ee，如果ee，0，ρ→[v，v]，m，ρ，e2，0，ρ [v2，v2]，m2，ρ，且m1≤m2.在第3节中，m给出2中间结果的最大值（绝对值），表达式的求值抽象的端点语义→的值是一对区间（[v，v]，[v，v]）∈（float×float）×（float×float）. 当然，第一个输入是具体值集合和第二区间的抽象是计算的精确结果的欠近似。因此，在图5的抽象语义中，第一个区间之间的操作是使用机器的标准舍入模式（通常是最接近的）进行的，而对于第二个区间，我们使用向内舍入模式，表示为。例如[v1，v1][v2，v2]=[v1v2，v1v2]（17）和[v1，v1]<$↓[v2，v2]=min（v1<$−∞v2，v1<$−∞v2），max（v1<$+∞v2，v1<$+∞v2）.（十八）一个抽象状态是一个对，ρ ∈E，ρ∈Expr×Env，其中Env表示将变量映射到抽象的浮点值的环境。一个表达式e1比特快列车e2好对于抽象环境ρ，d记为e1，浮动E2，如果ε1，ρε →ε（[vn（[v<$2，v<$2]，[v2，v2]），ρ和最大值（|v浮子-v的|、|v-v的|）≤max（|v1-v的|、|v浮体2-v的|）. 换句话说，如果在工作情况下，计算机与数学结果之间的误差较小对于E1，对于E2。关于固定点语义→，抽象值是所有固定点数都具有相同的格式。这样的区间记为[v，v]w，i。我们有：[v，v]（w，i）=.v（w，i）：v≤v≤v≠（19）抽象状态是一个三重态，W，ρ∈Expr×int×Env，其中Env是将变量映射到抽象定点值的环境集合。固定运算符表示其边界为不动点数的区间之间的运算。 运算精确，固定不需要舍入模式。对于抽象环境ρ，表达式e1优于表达式e2，表示为ee，如果εe，0，ρε→ε[v，v]<$w1，i1<$， W，ρ，e，0，ρ→<$[v2，v2]<$w2，i2<$，W2，ρ<$且W1≤W2. 在其他条件下，如果存储中间结果所需的比特数对于E1比对于E2更少。抽象区间语义的值→是区间[v，v]∈float×漂浮。 与第2节一样，运算符表示间隔之间四舍五入模式向外舍入的浮点数（参见公式（5）.）一 个抽象状态是一对εe，ρε ∈ Expr × Env其中Env表示所述ρ12固定16M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）3（p1，.， pn）ρρ1.Σ[]2[]1[]2将变量映射到浮动点值的区间的环境的表达e比表达式e对于抽象环境ρ，记为e你 好，若ρ∈1，r∈ →ρ∈（[v1，v1]），ρ∈，ρ ∈2，r∈ →ρ∈（[v2，v2]），ρ∈且v1−v1≤v2−v2，即，e1浮动e2如果从E1的评估得到的间隔的宽度小而不是由e2的计算得到的区间宽度。为了使用第4节的第一抽象来合成与源表达式e等效的新表达式，我们使用等式（9）的规则来计算集合E，使得{e}，{e'k}→kE，K}，并且我们使用图5的抽象语义来评估E的所有表达式，以用于期望的算术。 然后，我们选择表达式，其中h产生最小的结果，在意义上的in t，floa t，fixed或[]。关于APEGs，新表达式的合成需要特殊的技术来处理抽象框并在结构内部进行搜索。 对于盒子，已经提出了一种贪婪算法[6]。它包括选择在最佳运算pi∈pj，1≤i，j≤n，i/=j，在t中取最小值或在[]中取最小值，然后用box∗p1，...，p i−1，p i+1，.，p j−1，p j+1，.，pn，（p i<$p j）.对于通用APEGs，通过等价类，还提出了一种带记忆的有限深度搜索算法[6]。在其最简单的设置中，它包括在合成父等价类的表达式时只考虑子等价类的最佳表达式6结论在这篇文章中，我们已经提出了一个通用的框架，算术表达式的综合，可以通过计算机准确地评估，没有过度的我们已经考虑了整数，浮点，定点和区间算术和数学等价表达式的集合的两个抽象这篇文章的很大一部分致力于综合的正确性。大部分工作已在一个名为Sardana [7]的工具中实现，该工具接受浮点运算和定点运算，并实现APEG。许多实验已经进行了与Sardana和结果是令人信服的[6]。将来，我们希望将我们的方法推广到比简单算术表达式更复杂的代码片段。例如F. Logozzo和T. Ball研究了整数表达式之间的二元关系[10]。更一般地说，我们还旨在修改控制结构，如条件和循环。21M. Martel/Electronic Notes in Theoretical Computer Science 287（2012）317引用[1] ANSI/IEEE。 IEEE二进制浮点运算，std 754-2008版，2008年。[2] 帕特里克·库索和拉迪亚·库索 抽象解释：用于静态分析的统一格点模型通过构造固定点的近似来构造程序。在第四届ACM SIGPLAN-SIGACT编程语言原理研讨会会议记录中，第238- 239252. ACM Press，New York，NY，1977.[3] 帕特里克·库索和拉迪亚·库索通过抽象解释的程序转换框架的系统设计。第二十九届ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages会议记录，第178-190页。ACM Press，New York，NY，2002.[4] David Delmas、Eric Goubault、Sylvie Putot、Jean Souyris、Karim Tekkal和Franck Vedrine。 朝向在安全关键航空电子软件上的工业应用。工业关键系统的形式方法（FMICS'12），第53-69页，2009年[5] Mentor Graphics。MECHAMICCDatashees，软件版本2.6版，2011年。 http://www.mentor。com/esl/catapult/algorithmic.[6] Arnault Ioualalen和Matthieu Martel。一个新的表示数学等价表达式的抽象域。在静态分析研讨会（SASSpringer Verlag，2012.[7] Arnault Ioualalen和Matthieu Martel。Sardana：数值精度优化的自动工具。第15届GAMM-IMACS科学计算、计算机算术和验证数值计算国际研讨会（SCAN[8] DanielKüastner，StephanWilhelm，StefanaNen ova，Patri ckCousot，RadhiaCousot，J'erEscheromeFeret，AntoineMi n'e，Laure ntMau borgne，andX avierRi val. Ast r′ee：防止出现运行时间错误。嵌入式实时软件和系统（ERTSS 2011）。[9] 弗朗西斯科·洛戈佐。通过代码契约和抽象解释为工作程序员进行实际验证。在第12届验证、模型检查和抽象解释会议（VMCAI'11）的会议记录Springer Verlag，2011.[10] 弗朗西斯科·洛戈佐和汤姆·鲍尔 模块化和验证自动程序修复。 第27届ACM面向对象编程系统语言和应用国际会议（OOPSLAACM Press，New York，NY，2012.[11] 马蒂厄·马特尔基于语义的算术表达式转换。在静态分析研讨会（SASSpringer Verlag，2007年。[12] 拉蒙·E穆尔河，巴西-地贝克·基尔福特和迈克尔·克劳德。Introduction to Interval Analysis. SIAM，2009年。[13] 克里斯托夫·穆耶隆高效计算与结构矩阵和算术表达式。PhDthesis，Uni versi t'edeL yon-ENSdeLyon，November2011.[14] Jean-Mi chelMuller、NicolasBrisebarre 、Flore ntdeDine chin、Claude-PierreJeanner od、Vince ntLef`evre、GuillaumeMelquiond、NathalieRe vol、DamienSteh l'e和SergeTorres。 手簿的浮动点A算法。BirkhauserBoston，2010.[15] Ross Tate，Michael Stepp，Zachary Tatlock，and Sorin Lerner. 等式饱和：一种新方法到优化。在第36届ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages（POPL'09）中ACM Press，2009.[16] Ross Tate，Michael Stepp，Zachary Tatlock，and Sorin Lerner.相等饱和：一种新的优化方法。计算机科学，7（1），2011。