用于将输入计算机程序转换为输出计算机程序的方法和系统与流程
本公开涉及计算机程序开发，更具体地涉及一种用于将包括应用于浮点变量的数学函数的输入计算机程序转换为实现目标全局精度的输出计算机程序的方法和系统。目标全局精度对应于输出计算机程序所允许的全局误差的上界，其中，误差涉及数学函数近似和/或浮点舍入误差。
背景技术：
1、数值计算在需要它们的各种工业领域中无处不在，例如信号或图像处理、自动控制等。例如，这些数值计算广泛用于诸如汽车或核电站控制等的各种应用的嵌入式系统的计算机程序中。
2、然而，这些数值计算经受与进行近似有关的固有计算误差。
3、例如，由于计算机算法，特别是浮点算法的有限精度，例如嵌入式系统上运行的计算机程序经受舍入误差。实际上，这些计算机程序不使用实际实数，而是对应浮点近似，这些近似引入了误差。该误差在一些情况下可忽略，但是在计算机程序的执行期间也会累积，特别是在存在嵌套循环的情况下，并且变得不可忽略。
4、计算误差的另一来源对应于数学函数实现中进行的近似。例如，物理系统的数学函数实现依赖于近似，这是由于浮点算法，但是也由于物理系统的数学模型本身是近似的。例如，诸如余弦和正弦函数的三角函数通过例如多项式函数来近似，这些多项式函数在数值计算中引入了误差。另外，当物理系统通过例如微分方程来建模时，这种微分方程可通过数学函数(例如，通过龙格-库塔(runge-kutta)方法)来求解，但所提供的解仅是对物理系统建模的微分方程的实际解的近似。
5、这两个误差来源(即，浮点舍入误差和数学函数近似)特别难以预测和调试。当在计算机程序中使用诸如libm的数学函数库时尤其如此，因为数学函数的实际实现通常是黑盒并且依赖于架构。
6、然而，重要的是能够确定计算机程序固有的全局误差(即，浮点舍入误差和/或数学函数近似)，能够确保计算机程序的全局误差保持低于期望的目标上界。
7、目前的解决方案旨在验证计算机程序的数值精度。这些技术或者是经验性/随机性的，或者基于形式化验证方法。尽管前一类工具利用数学函数调用为任意计算机程序提供结果，但后一种工具不能用于无法静态验证精度的数学函数的黑盒实现。
8、因此，目前的解决方案使得在一些情况下可确定全局误差(但是当使用数学函数的黑盒实现时没有形式上证明它)，但无法确保由于浮点舍入误差和/或数学函数近似而引起的全局误差保持低于目标上界。
技术实现思路
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、另外，这些图中所表示的步骤顺序仅是为了例示目的而提供，并非意在限制本公开，本公开可通过以不同顺序执行的相同步骤来应用。
技术特征：
1.一种用于将输入计算机程序转换为实现目标全局精度的输出计算机程序的计算机实现的方法，所述输入计算机程序包括应用于浮点变量的数学函数，并且所述目标全局精度对应于由于数学函数近似和/或浮点舍入误差而引起的全局误差的界，所述方法包括以下步骤：
2.根据权利要求1所述的方法，该方法还包括基于所述目标全局精度来注释所述输出计算机程序并且通过使用形式化验证工具来验证所述输出计算机程序的所述注释。
3.根据权利要求2所述的方法，其中，基于所述数学函数的所述值范围并且基于所述合成数学函数的所述目标内部精度来进一步注释所述输出计算机程序。
4.根据权利要求2或3所述的方法，其中，所述形式化验证工具是演绎验证工具。
5.根据权利要求4所述的方法，其中，所述演绎验证工具使用自动定理证明器。
6.根据权利要求5所述的方法，其中，所述演绎验证工具针对与数学函数近似有关的证明义务和与浮点舍入误差有关的证明义务使用不同的自动定理证明器。
7.根据权利要求2至6中的任一项所述的方法，其中，当所生成的输出计算机程序没有实现所述目标全局精度时，所述方法还包括对以下步骤进行迭代，直至生成实现所述目标全局精度的输出计算机程序：
8.根据权利要求1至7中的任一项所述的方法，其中，针对在所述输入计算机程序中具有不同调用位置的同一数学函数合成不同的合成数学函数。
9.根据权利要求1至8中的任一项所述的方法，其中，所述值范围确定工具是抽象解释工具。
10.一种包括指令的计算机程序产品，所述指令在由至少一个处理器执行时将所述至少一个处理器配置为执行根据权利要求1至9中的任一项所述的方法。
11.一种包括指令的计算机可读存储介质，所述指令在由至少一个处理器执行时将所述至少一个处理器配置为执行根据权利要求1至9中的任一项所述的方法。
12.一种用于将输入计算机程序转换为具有目标全局精度的输出计算机程序的系统，所述输入计算机程序包括应用于浮点变量的数学函数，并且所述目标全局精度对应于由于数学函数近似和/或浮点舍入误差而引起的全局误差的界，所述系统包括至少一个处理器和至少一个存储器，其中，所述至少一个处理器被配置为执行根据权利要求1至9中的任一项所述的方法。
技术总结
本公开涉及一种用于将输入计算机程序转换为具有目标全局精度的输出计算机程序的计算机实现的方法，该方法包括：‑接收输入计算机程序中所包括的各个数学函数的目标内部精度；‑分析输入计算机程序以确定描述数学函数调用之间的依赖关系的依赖关系图，其中，针对各个处理的数学函数，通过以下步骤来根据依赖关系图处理数学函数：‑使用值范围确定工具以基于针对所处理的数学函数根据依赖关系图所依赖的数学函数获得的各个合成数学函数来生成所处理的数学函数的值范围；‑使用合成工具来生成具有目标内部精度的合成数学函数，其中，通过用对与各个数学函数对应的合成数学函数的调用替换各个数学函数调用来生成输出计算机程序。
技术研发人员：B·鲍耶尔,F·费索尔,G·梅尔基翁
受保护的技术使用者：三菱电机株式会社
技术研发日：
技术公布日：2024/9/23