We give a process for verifying numerical programs against their functional specifications. Our implementation is capable of automatically verifying programs against tight error bounds featuring common elementary functions. We demonstrate and evaluate our implementation on several examples, yielding the first fully verified SPARK implementations of the sine and square root functions. The process integrates existing tools using a series of transformations and derivations, building on the proving process in SPARK where Why3 produces Verification Conditions (VCs) and tools such as SMT solvers attempt to verify them. We add steps aimed specifically at VCs that contain inequalities with both floating-point operations and exact real functions. PropaFP is our open-source implementation of these steps. The steps include symbolic simplifications, deriving bounds via interval arithmetic, and safely replacing floating-point operations with exact operations, utilizing tools such as FPTaylor or Gappa to bound the compound rounding errors of expressions. Finally, the VCs are passed to provers such as dReal, MetiTarski or LPPaver which attempt to complete the proof or suggest possible counter-examples.
翻译:我们根据功能规格对数字程序进行核查。 我们的执行能够自动核查程序, 防止具有共同基本功能的严格错误界限。 我们通过几个例子来展示和评估我们的执行情况, 产生第一批经充分核实的 SPARK 执行正弦和正方根函数的 SPARK 执行过程。 这一过程利用一系列变换和衍生工具整合现有工具, 在 SPARK 的验证过程的基础上, Wh3 产生核查条件( VC ), 以及 SMT 解答器等工具试图核查这些条件。 我们添加了专门针对VC 的步骤, 后者包含浮点操作和精确真实功能的不平等。 PropaFP是这些步骤的开放源执行。 这些步骤包括象征性简化、 通过间距算取界限, 以及安全地用精确操作取代浮动点操作, 使用 FPTaylor 或 Gappa 等工具来约束复合圆形表达错误。 最后, VC 被传递给像 dReal、 MetiTarski 或 LPPPaver 这样的验证器, 试图完成证据或建议可能的反形标。