程序转换: 去除平方根和除法的精确计算方法

可在www.sciencedirect.com在线获取理论计算机科学电子笔记317（2015）117-131www.elsevier.com/locate/entcs一个证明平方根和除法消元法Pierre Neron1T.U.荷兰代尔夫特摘要本文介绍了一种程序转换的实现，它可以从函数程序中去掉平方根和除法，而不需要递归，从而产生可以精确计算的代码。这种转换接受不同的语言子集作为输入，当目标语言是PVS时，它提供了一种证明机制。在这种情况下，我们提供了输出代码中的每个函数定义与输入代码中对应的函数定义之间的关系，该关系指定了生成函数相对于输入函数的行为。 这种转换已经在OCaml中实现并经过测试NASA ACCoRD项目的不同算法关键词：程序变换;实数计算;证明变换;语义保持1引言关键的嵌入式系统，例如在航空领域，需要非常高的安全性。产生可以满足这种所需安全级别的代码的一种方法是在证明助手（诸如PVS.嵌入式系统不运行PVS代码，但从证明的PVS规范中，我们可以提取对应于该规范的真实语言中的相应程序（参见[6]的提取示例）。然而，这些嵌入式系统也可以是信息物理系统，因此具有对不能精确计算的实数的数学运算的扩展使用。特别地，如果我们旨在满足嵌入式系统的通常要求，即，有界内存和有界循环事实上，已经开发了一些方法来精确计算实数（见[2，17，18]）或使用惰性评估（见[13]）的足够精度，但这些技术通常涉及无界行为。对于嵌入式1电子邮件：p.j.m. tudelft.nlhttp://dx.doi.org/10.1016/j.entcs.2015.10.0121571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。118P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）117√（Ⅲ）系统，通常依赖于有限表示和通过抽象解释或区间算术对舍入误差的分析[3，5]。或者，人们可能希望直接证明正确性属性，而不是在实数上，而是在系统使用的有效实现上，例如，证明点数[1]，但在这种情况下，证明变得非常困难，因为任何数学直觉都失去了。例如，航空嵌入式系统在冲突检测和解决算法中使用平方根和除法。这些操作不能在有限内存中精确计算，因为它们可能产生有限的数字序列。这不是加法和乘法的情况。这些运算只产生有限的数字序列，因此它们可以使用某些固定点表示来精确计算。在只有有界循环的嵌入式系统中，确定此固定点表示所需的大小相对容易。本文提出了一种程序转换工具，它消除了这些平方根和除法，这种转换使提取的代码能够准确地计算。转换还提供了一个证明机制[16]来证明语义保持。本文重点介绍了系统的描述和实现方面。这项工作的理论方面在[9- 11 ]中介绍本文的结构如下。第二节重点介绍了OCaml 第3节描述了嵌入的子集pvs提供认证过程。第4节介绍了转换的一些技术细节和功能。第5节介绍了这种转换在ACCoRD2框架中的冲突检测算法中2OCaml转换2.1语言程序转换是在OCaml中定义的，并在一种名为MiniPVS的语言上运行，这种语言是一种类型化的函数语言，包含数值（R）和布尔常量、测试（如果否则）、对、常用的算术运算符+、−、×，/，，比较=，/=，>，≥，，≤，布尔运算符（，，<$），变量函数定义及应用。图1将语言的OCaml定义为抽象数据类型，其中uvar是变量标识符的集合。这种语言的语义非常简单。表达式Letin x body scope被解释为let x = body inscope，Letfun f（v，tv）t body scope是函数的定义，该函数将v作为类型tv的参数并返回类型t的元素，即，让f（v：tv）：t =作用域中主体;它们的语义使用按值调用。 这种语言的详细语义可以在[11]中找到，3和4我们将环境Env中程序p的语义表示为pEnv。函数和变量定义允许多变量定义（例如，令f（x，y）= x + y），但不允许部分应用。该语言可以表示许多编程语言的子集，并且用这样的子集编写的程序可以2http://shemesh.larc.nasa.gov/people/cam/ACCoRD/P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）117119类型程序=||||||||||值关于Uvarunop编程的常量Uop的ConstBOp比诺普∗prog电子邮件FSTSnd对的prog电子邮件的prog的prog类型联合国内罗毕办事处=|如果的prog∗prog电子邮件App的乌瓦尔电子邮件莱廷的var∗prog电子邮件Letfunof uvar（v a r types）typesprogprog类型binop =|Sqrt|Umin| Neg|加上|倍|Div|和| Or类型var =| Neq|EQ|GT| Geq|Lt| Leq| 乌 瓦尔的乌瓦尔|对瓦尔Fig. 1. 迷你P与抽象P通过构建输入和输出接口（即，一个解析器和一个漂亮的打印机）。2.2转换规范这种转换的目标是从这种语言定义的程序中删除平方根和除法。程序的转换依赖于两个不同的步骤。第一个是所有变量定义和函数的转换，以确保可能出现在表达式中的变量或函数调用的值这种转换依赖于反统一算法来部分内联变量和函数定义，如以下示例所示：−→由Reynolds [15]和Plotkin独立引入的反统一问题[14] 1970年是统一问题的对偶。给定两个项t1和t2，反统一算法计算项t和两个替换σ1和σ2，即t σ1=t1和tσ2=t2。 在该示例中，项（x1+x2）/x3（表示为t）是a+b·c+d和e·f/（g+h）的模板，因为我们有若F则a+<$b·c+d在SC设x =否则e·f/（g+h）let（x1，x2，x3）=若F则（a，b·c+d，1）在SC中[x：=（x1+x2）/x3]else（e·f，0，g+h）√120P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）117（Ⅲ） （）（）（）以下等式：t[x1<$→a;x2→<$t[x1<$→e·f;x2b·c+d;x3<$→ 1]=a+<$b·c+d0;x3<$→（g+f）]=e·f/（g+f）转换的第二步是消除布尔表达式中的平方根和除法。它依赖于简单的转换规则的广泛应用，用于消除所有平方根和除法的算术表达式之间的比较这些规则依赖于这种比较的通常等价性，例如：p·q=rp·r≥ 0p2·q =r2a/b>cb>0a>b·cb0ab·c当然，我们不能从所有程序中删除平方根和除法（例如，程序sqrt（2）将仍然必须返回舍入值2）。然而当从所有布尔表达式和所有定义中消除了平方根和除法，可以精确计算这种转换程序的布尔值。因此，程序的控制流程受到保护，不受任何舍入的影响。避免程序控制流程中的舍入错误可以防止程序行为的发散。if then else语句的条件中的错误可以引起程序的完全不同的语法部分的执行，从而引起效果和预期结果之间的巨大错误。例如，如果执行一个标准的浮点数实现，下面的程序将返回1000：如果22>2则1000否则0如果决定程序控制流程的布尔表达式被精确计算，这种发散就不再可能布尔表达式的转换在[10]中描述，使用反统一和部分内联的定义转换在[9]中描述。这种转换在每一种环境中保留了程序的语义，在这种环境中，语义不会由于除以零或平方根或负数而失败。定义2.1语义保持设tr是程序变换变换，pEnv是环境Env中p的语义（环境将标识符映射为值）;tr保持语义当且仅当对于所有程序p和pEnv，pEnv/=失败=我们不考虑输入程序失败的情况，因为我们不想在输入程序中抛出由于除以零而导致的显式错误，这些错误在输出中没有意义。此外，我们的转换目标程序已经被证明没有这样的错误（在PVS中，如果不证明x是正数，就不允许写sqrt（x）P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）117121提取（PVSio +MiniPVS预处理打印机（OCamlMiniPVSPVSthy-elim.pvsTTY转换（OCaml）图二. PVS理论转换对于布尔表达式变换，在PVS中已经证明了语义保持，但是反统一性没有得到证明，因此变量和函数定义变换也没有然而，虽然反统一算法不容易被证明是正确的，但它的结果很容易检查，所以我们可以使用这个属性来定义一个证明变换。而不是正式证明，ING的转换算法是正确的，我们提供了每个转换程序，证明这个程序是等效的输入程序。3Pvs规格在本节中，我们将介绍如何在图1中描述的语言上使用OCaml中定义的转换，即，MiniPVS，转换PVS规格。PVS语言比MiniPVS复杂得多，但是这种语言嵌入了足够的结构来表示PVS语言的子集，包括非递归函数定义和实值表达式。因此，转换的第一步是将PVSspecification转换为OCaml的prog类型。特别是，我们必须删除大部分的逻辑部分， P与规范，使其适合prog类型。 我们不感兴趣的所有在PVS函数的类型中编码的子类型谓词。该过程类似于证明助手中的代码的通常提取（例如，[7]）。这种提取产生了一个具体语法对应于MiniPVS的程序，OCaml程序能够将其作为输入处理。转换的第一步是使用PVSio实用程序实现的，P与[8]。PVSio是一个软件包，它扩展了地面评估器，命令式编程语言特性的最终库，例如边对象、无界循环、输入/输出操作、浮点运算、异常处理、漂亮打印和解析。这个包允许我们访问表示PVS代码的底层Lisp结构，因此可以在MiniPVS中打印相应的程序，这些程序可以由OCaml实现解析。图2给出了P对理论的转换方案122P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）117f（x：real）：real =（x - 1）/（x +1）...f（c+sqrt（d））然而，有一个微妙的区别，PVS 迷你PVS. 一另一方面，在MiniPVS中，每个定义都有一个作用域，因此每个程序都是完整的。这允许我们通过声明这样一个程序的语义被保留来指定转换是正确的，如定义2.1所述。 另侧PVS 文件是变量、函数和引理的定义序列而没有任何允许我们声明语义保留的作用域。在[9]中，在这个程序转换中引入的转换定义的机制提供了每个输入定义与输出程序中相应定义之间的正确性关系因此，我们通过添加一个构造函数来扩展MiniPVS语言，该构造函数将子类型谓词添加到每个转换的定义中。：|莱特夫斯特的乌瓦尔∗（v a r∗类型）（v a r∗类型（prog）电子邮件电子邮件这个构造函数必须以下面的方式解释，Letfstf（u，tu）（u，tu，pu）bodyscope表示函数定义：let f（v：tv）：{u：tu| P（v，u）}=作用域中的主体也就是说，一个函数接受类型为tv的参数v并返回类型为tu的元素，使得P（v，f（v））。 {x：T |P（x）}表示满足P的元素的T的子类型。这种表示法类似于子类型的PVS语法。因此，子类型谓词将用于编码输出程序的定义与输入程序的相应定义例3.1下面的PVS函数及其调用：转换为以下代码：f_e（x1，x2：real）：{ z1，z2，z3：real|（z1 + sqrt（z2））/（z3 + sqrt（z2））= f（x1 + sqrt（x2））} =（x1 - 1， x2， x1 + 1）... f_e（c，d）在更一般的方式中，P与函数定义的转换具有以下形式：f（x：T1| P（x））：{ y：T2| Q（y）}= ...转化为相应的定义：f_e（x '：T 1 '）：{ y '：T 2'| g_o（y'）= f（g_ i（x '））} =.谓词g o（y'）= f in（g i（x'））是指定输出函数（f out）相对于输入函数（f in）的行为的关系。g i（出现在谓词中的函数f将输入程序导入到变换后的程序中，以验证变换的正确性。 的变量P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）117123在输入程序中定义的子类型仅用于子类型谓词，而不用于转换程序的可执行部分。可以注意到，通常输入和输出函数的输入和输出类型不匹配。然而，布尔函数的转换不会改变输出类型，在这种情况下，转换将具有以下形状：例3.2给定PVS函数返回布尔表达式：f（x：T1 |Q（y）} =.|Q(y) } = ...其相应的变换定义具有以下形式：f_e（x '：T 1 '）：{ y '：boo l|y' = f（g_ i（x '））} =.输入类型仍然可以被转换，因为输入可以是数值，因此该函数可以应用于平方根或除法，这将强制改变输入类型。为每个变换后的定义嵌入一个正确性引理，使我们能够变换由定义序列组成的通常的PVS理论，并证明等价性，而不需要返回表达式（该定义的范围），因为它是MiniPVS语言所需要的（在这种语言中，每个定义都有一个范围）。在一个真正的PVS规范中没有作用域的问题可以通过使用一个简单的新鲜变量作为相应的MiniPVS程序的作用域定义被转换，正确性独立于作用域转换而建立，作用域转换只是恒等式（一个自由变量被转换成它自己），因此当我们打印输出PVS程序时，我们可以擦除这个人工作用域形式上验证转换后的程序是否正确的唯一步骤是证明输出程序中生成的子类型谓词对应的引理。P VS已经分解了可能出现在函数体中的不同情况（对应于if thenelse表达式），因此我们需要证明的唯一引理是包含平方根和除法的算术表达式的等式，例如，例3.3例3.1中的子类型谓词的证明依赖于以下等式：((x1- 1）+sqrt（x2））/（（x1+ 1）+sqrt（x2））=f（x1+sqrt（x2））在大多数情况下，一个简单的算术PVS策略就足够了，比如（grind-reals）。更复杂的情况可能需要首先消除出现在这些谓词中的平方根和除法。这可以使用PVS策略（elim-sqrt）来完成，该策略在PVS的证明上下文中消除了不等式的平方根和除法。这种策略是从证明消除平方根和除布尔表达式中描述的[12]。该工具通过允许直接处理变量和函数定义并对其进行验证，将这种转换提升到程序级别。转换代码的一般原理已经概述，现在让我们关注OCaml转换的不同特性124P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）1174MiniPvs的转型转换的OCaml实现嵌入了一些选项，旨在减少某些特定情况下生成代码的大小4.1布尔表达式如前所述，程序转换依赖于布尔表达式中的平方根和除法消除。这种消除在[10]中描述，但在某些地方，不同的规则可以是首选的。例如，可以使用大小写区分或使用分母的平方来消除比较中的除法，例如，例4.1假设B/= 0，下列等式成立：A/B > C（B >0A>B×C）（B0AB×C）（1）A/B>CA×B> C×B×B（2）消元法（1）产生更小的算术项，因此用+、×、−进行精确计算的定点表示的大小更小，而规则（2）产生更少的比较和更小的公式。根据其目标，用户可能更喜欢一种消除方案而不是另一种消除方案，因此规则的选择是转换的一个选项。以类似的方式，平方根的消除可以使用布尔表达式中的变量定义但是，用户可能希望仅对使用布尔运算符和算术运算符构建的表达式使用转换，并将转换限制为此类表达式语言。因此，该变换提供了两种消除平方根的方案4.2比较算子的变换消除具有指数复杂性的布尔表达式中的平方根和除法，变换后的表达式大大降低了输出代码的可读性，这些消除产生大型布尔表达式。为了解决这个问题，我们建议通过定义模板特定的比较表达式来处理不同文件中的复杂性。使用反单位化的函数变换在产生的代码的大小方面是有效的，并且等价引理使用（elim-sqrt）策略相对容易证明。因此，我们决定使用这个函数变换，以便因式分解由布尔消除平方根产生的大型布尔表达式。这是通过在应用转换之前首先将输入程序中的比较运算符替换为具有相同语义的函数来完成的，例如，图3中的程序被转换成图4中的程序。P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）117125gt1（ gt1l， gt1r： real）：bool =gt1l>gt1r gt2（ gt2l， gt2r： real）：bool=gt2l> gt2rf（x1，y1：posreal）：bool=gt1（x1 +sqrt（y1）* y1，0）g（x，y，z： posreal）：real=如果gt2（z +sqrt（y +x），1）或f（y，z）则yELSEsqrt（x）+f（x1，y1：posreal）：bool = x1 + sqrt（y1）* y1 > 0g（x，y，z：posreal）：real =如果z +sqrt（ y +x）> 1或f（y，z）则yELSEsqrt（x）+yENDIF图三. 使用>运算符编程见图4。 将>声明为函数的这种预处理为程序中使用的每个比较运算符生成一个比较函数这个过程需要产生比较函数，其规格与所需的用途完全匹配，而仅创建一个比较函数将产生转换函数，其规格必须匹配所有用例。布尔函数的转换是代码大小爆炸的原因，我们希望避免这样一个通用函数，它将具有巨大的定义体。然而，由于我们为输入程序中的每个比较运算符创建了一个新函数，因此引入了一些冗余。 在图3的程序中，比较应用于仅使用一个平方根的表达式。因此，这两个比较都具有以下形式：t +u。其中t、u和v为平方根和除法自由表达式。因此，对应于gt1和gt2的变换函数将具有相同的规范和定义（模α等价），因此我们只能使用其中一个，并且程序被重构以仅使用其中一个等价函数。我们的转换生成了图5中的程序，它只包含一个比较函数，即带有四个参数的gt0 e此函数具有以下规范编码在其类型：gt0e（x，y，z，sq）优惠x+y优惠sq> z该函数的定义体比输入函数的定义体大得多（即，x > y），但是现在计算结果时不使用任何平方根或是组织因此，布尔表达式与函数的这种转换仅需要转换的自动预处理和后处理• 在 应 用 主 变 换 之 前 ， 用 一 个 定 义 为 该 运 算 符 的 函 数 来 替 换 所 有 出 现 的combination运算符• 应用主变换。• 对于对应于比较运算符的所有变换函数，对具有相同规格的函数进行因子化126P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）117Xygt0_e（gt0_1_1， gt0_1_2， gt0_2， sq_2： real）：{ res：bool|res= gt0_1_1+ gt0_1_2 * sqrt（sq_2）>gt0_2 }=LET（at_p， at_r， at_rel， at_neq）=（gt0_1_2 > 0， gt0_1_1 - gt0_2 > 0，gt0_1_2 * gt0_1_2 * sq_2-（gt0_1_1 - gt0_2）*（gt0_1_1 - gt0_2）> 0，gt0_1_2 * gt0_1_2 * sq_2-（gt0_1_1-gt0_2）*（gt0_1_1-gt0_2）/=0）在at_p和 at_r或 at_p和at_rel或at_r和不at_rel和at_neqf_e（x1，y1：real）：{res：bool|res = f（（x1，y1））}= gt0_e（（x1，y1，0，y1））g_e（x，y，z：real）：{ g_1，g_2，sq_0：real |g_1 + g_2 * sqrt（sq_0）= g（（x，y，z））} =如果gt0_e（（z，1，1，y +x））或f_e（（y，z））则（y，0，0）否则（y，1，x）ENDIF图五、具有比较功能的转换程序这种转换大大减少了输出文件的大小，因为与布尔表达式转换相对应的大表达式现在被分解为函数。此外，这些新的比较函数也可以在一个单独的文件中生成，然后导入到转换后的程序中，并在不同的转换后的程序之间共享。通过这种方式，转换后的程序具有与输入程序完全相同的结构为了在一个真实的例子上说明我们的变换，我们在第5节中给出了一个真实的PVS程序的变换，用于二维的冲突检测5应用一个完整的PVS规范可以通过与PVSio链接的转换在本节中，我们介绍了一个冲突检测算法的转换，即cd2d，这是由NASA在ACCoRD框架中开发的。该算法的目的是在一个二维空间中检测两个飞行器之间的分离损失。在[4]中已经提出了这种近似点算法的形式验证，该算法在该论文中进行了描述，但我们回顾了它的主要特征。飞机的坐标是相对的，因此，给定飞机在二维中的位置s1=（x1，y1）和s2=（x2，y2），s=（x1-x2，y1-y2）表示这些飞机之间的相对距离。假设飞机在至少一个前瞻时间内具有恒定的速度，并且它们的速度也在二维空间v=（vx1-vx2，vy1-vy2）中相对地表示。给定距离D，当飞机太近时会发生分离损失，这意味着它们的距离小于D：loss？（s）不公平。s2+s2D当分离损失将在结束前发生时，P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）117127cd2d：理论开始进口reals@sqrt、以琳zero_vect2？（zerov：[ real， real]）：bool =零v=0AND Dzerovdet（sdet，vdet： [ real， real ]）：real= sdet水平损失？（bool：[ real，real]，bool：real）：bool=horizv<'1 * ho r i z v ' 1 + ho r i z v ' 2 * ho r i z v ' 2 horiz D * horizDminmax（maxv1，maxv2，minv：real）：real=LETmaxi= IFmaxv1> maxv2THE Nmaxv1ELSEmaxv2ENDIFINIFmaxi minvTHENmaxiELSE minvENDIFmaxmin（ minv1， minv2， maxv：real）：real =LETmini= IF最小值1< minv2THE Nminv1ELSEminv2ENDIFINIFmini >maxvTHEN miniELSE maxvENDIFDelta（sDelt，vDelt：[real，real]，DDelt：real）：real=（DDelt*DDelt）*（vDelt *vDelt+vDeltTheta_D（sThe，nzvThe：[real，real]，eps，Dthe：real）：real=LETa=（nzvThe *nzvThe+nzvThe *nzvTheB= sThe *nzvThe+sThec=（sThe sThe+ *（Dthe*Dthe在（-b + eps*sqrt（（b*b）-a*c））/a;dtct_2D（s，v：[real，real]， B， T， D，entry，Exit：real）：[real，real]=IFzero_vect2？（v）ANDDhorizontal_los？（s，D）THEN（B，T）ELSIF测量a（s，v，D）>0然 后LETtin= Theta_D（s，v，Entry，D），tout=Theta_D（s，v，Exit，D）在 （minmaxx（t，B，T），maxmin（t， T，B））ELSE（B，B）ENDIFdetect？（st，vt：[real，real]，Bt，Tt，Dt，Entryt，Ent：real）：bool=LET（tint，toutt）=dtct_2D（st，vt，Bt，Tt，Dt，见图6。 cd2d连接检测程序先行时间T：冲突？（s，v）损失t≤T，损失？（s+t·v）其中+和·是R2中常见的加法和常数乘法。在cd2d中定义了一个名为dtct2D的函数，它计算分离丢失发生的时间间隔，如图7中的谓词所描述的，这些谓词已经在PVS中得到了证明。为了能够转换原始程序，我们必须清除所有的引理和定理，只保留计算部分。ACCoRD系统中定义的冲突检测算法的P与规范如图6所示。该程序的唯一平方根和除法在ThetaD函数中，但是在dtct2D函数的主体中，ThetaD的结果然后由128P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）117dtct_2D_correct：定理LET（tin， tout）=dtct_2D（s，v）INtin 0，则LET（Theta_D_n_1，Theta_D_n_2，Theta_D_d，sq_0）=Theta_D_e（（s，v，Entry，D））在LET（new_Theta_D_n_1，new_Theta_D_n_2，new_Theta_D_d，new_sq_0）=Theta_D_e（（s，v， 出口，D））在LET（maxmin_n_1，maxmin_n_2，maxmin_d，sq_3）=maxmin_e（（new_Theta_D_n_1，new_Theta_D_n_2，new_Theta_D_d，T，B，new_sq_0））在LET（minmax_n_1，minmax_n_2，minmax_d，sq_6）=minmax_e（（Theta_D_n_1，Theta_D_n_2，Theta_D_d，B，T，sq_0））IN（minmax_n_1，minmax_n_2，minmax_d，maxmin_n_1，maxmin_n_2，maxmin_d，sq_3，sq_6）ELSE（ B，0，1，B，0，1，0，0）ENDIFENDIFdetect？_e（st，vt ：[real，real]，Bt，Tt，Dt，Entryt，退出t：real）：{res：bool|res=detect？（（st，vt，Bt，Tt，Dt，Entryt，Exitt））}=LET（dtct_2D1_n_1，dtct_2D1_n_2，dtct_2D1_d，dtct_2D2_n_1，dtct_2D2_n_2，dtct_2D2_d，sq_7，sq_8）=dtct_2D_e（（st，vt，Bt，Tt，Dt，Entryt，Exitt））INlt3_e（（ dtct_2D1_n_1， dtct_2D1_n_2， dtct_2D1_d，dtct_2D2_n_1， dtct_2D2_n_2， dtct_2D2_d， sq_8，sq_7））端cd2d_elim见图9。 转化的cd2dPt. 2用诸如在minmax和maxmin函数中使用的gt0 e或lt1 e的函数来代替isons。 它们的使用是因式分解的，因为minmax e和maxmin e使用相同的比较函数。这些比较函数在一个单独的文件中定义，即cd2d operators.pvs，如4.2节所介绍的。可以注意到，输出程序中的行数是输入程序长度的两倍多然而，这主要是由于与转换后的函数相关联的子类型谓词的长度。所有这些子类型谓词都可以通过首先展P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）117131开输入程序的函数，然后使用（grind-reals）策略来证明。132P. Neron/Electronic Notes in Theoretical Computer Science 317（2015）117因此，根据嵌入在函数类型中的类型谓词，这个转换后的程序等价于输入程序，并且除了这些谓词之外，它不再使用平方根或除法。特别是，最后一个功能，检测？e，返回一个布尔值不仅具有相同的签名，而且具有相同的行为，然后相应的输入函数，即检测？，但其结果不依赖于任何平方根或除法计算。因此，能够构建具有加法、减法和乘法的实数计算的精确实现将使该程序能够精确执行。结论我们提出了一种程序转换，消除平方根和divisions从直线程序，以便允许精确的计算与加法和乘法。这种转换嵌入了一种证明机制，用于证明输入和输出程序的定义之间的语义保持。在证明助手中消除平方根和除法也允许使用一些决策过程，这些决策过程最初并不处理这些操作。这种转换的未来工作包括扩展这种转换所适用的语言，包括循环和更一般的反统一和内联方法不支持的某种递归。通过将输入程序的PVS子类型谓词转换为关于定义的等价谓词，也可以改进PVS类型的转换的输出程序。确认我要感谢塞萨尔·穆恩诺兹对这个项目进行了有益的讨论。这项工作得到了兰利研究中心NASA航空安全计划的飞行关键系统保证项目的支持，该项目引用[1] S. 博尔多和J. - C. 把它装满。 并行点程序的规范化验证 体育教学 Kornerup 和J. - M. Muller，编辑，Proceedings of the 18 th IEEE Symposium on Computer Arithmetic，第187-194页， Montpellier，France，2007年6月。[2] C. 科恩Coq中实代数数的构造在洛