ada - 在 Ada Spark 中无法证明看似微不足道的平等
问题描述
所以我有这两个文件。
testing.ads
package Testing with
SPARK_Mode
is
function InefficientEuler1Sum2 (N: Natural) return Natural;
procedure LemmaForTesting with
Ghost,
Post => (InefficientEuler1Sum2(0) = 0);
end Testing;
和 testing.adb
package body Testing with
SPARK_Mode
is
function InefficientEuler1Sum2 (N: Natural) return Natural is
Sum: Natural := 0;
begin
for I in 0..N loop
if I mod 3 = 0 then
Sum := Sum + I;
end if;
if I mod 5 = 0 then
Sum := Sum + I;
end if;
if I mod 15 = 0 then
Sum := Sum - I;
end if;
end loop;
return Sum;
end InefficientEuler1Sum2;
procedure LemmaForTesting
is
begin
null;
end LemmaForTesting;
end Testing;
当我运行 SPARK -> Prove File 时,我收到这样的消息:
GNATprove
E:\Ada\Testing SPARK\search\src\testing.ads
10:14 medium: postcondition might fail
cannot prove InefficientEuler1Sum2(0) = 0
为什么呢?我误解了什么或做错了什么?提前致谢。
解决方案
为了证明平凡的等式,您需要确保它被函数的后置条件覆盖。如果是这样,您可以使用一个简单的Assert
语句来证明相等性,如下例所示。此时不需要引理。
但是,后置条件不足以证明不存在运行时错误 (AoRTE):给定函数的允许输入范围,对于 的某些值,求和可能会N
溢出。为了缓解这个问题,您需要绑定 的输入值N
并向证明者显示,Sum
使用循环不变量的值在循环期间保持有界(有关循环不变量的一些背景信息,请参见此处、此处和此处)。出于说明目的,我选择了 的保守界限(2 * I) * I
,这将严格限制输入值的允许范围,但确实允许证明者证明示例中不存在运行时错误。
testing.ads
package Testing with SPARK_Mode is
-- Using the loop variant in the function body, one can guarantee that no
-- overflow will occur for all values of N in the range
--
-- 0 .. Sqrt (Natural'Last / 2) <=> 0 .. 32767
--
-- Of course, this bound is quite conservative, but it may be enough for a
-- given application.
--
-- The post-condition can be used to prove the trivial equality as stated
-- in your question.
subtype Domain is Natural range 0 .. 32767;
function Inefficient_Euler_1_Sum_2 (N : Domain) return Natural
with Post => (if N = 0 then Inefficient_Euler_1_Sum_2'Result = 0);
end Testing;
测试.adb
package body Testing with SPARK_Mode is
-------------------------------
-- Inefficient_Euler_1_Sum_2 --
-------------------------------
function Inefficient_Euler_1_Sum_2 (N : Domain) return Natural is
Sum: Natural := 0;
begin
for I in 0 .. N loop
if I mod 3 = 0 then
Sum := Sum + I;
end if;
if I mod 5 = 0 then
Sum := Sum + I;
end if;
if I mod 15 = 0 then
Sum := Sum - I;
end if;
-- Changed slightly since initial post, no effect on Domain.
pragma Loop_Invariant (Sum <= (2 * I) * I);
end loop;
return Sum;
end Inefficient_Euler_1_Sum_2;
end Testing;
主文件
with Testing; use Testing;
procedure Main with SPARK_Mode is
begin
pragma Assert (Inefficient_Euler_1_Sum_2 (0) = 0);
end Main;
输出
$ gnatprove -Pdefault.gpr -j0 --level=1 --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
main.adb:5:19: info: assertion proved
testing.adb:13:15: info: division check proved
testing.adb:14:24: info: overflow check proved
testing.adb:16:15: info: division check proved
testing.adb:17:24: info: overflow check proved
testing.adb:19:15: info: division check proved
testing.adb:20:24: info: overflow check proved
testing.adb:20:24: info: range check proved
testing.adb:23:33: info: loop invariant preservation proved
testing.adb:23:33: info: loop invariant initialization proved
testing.adb:23:42: info: overflow check proved
testing.adb:23:46: info: overflow check proved
testing.ads:17:19: info: postcondition proved
Summary logged in /obj/gnatprove/gnatprove.out
推荐阅读
- python - Python3从txt文件中的URL下载csv文件
- html - XML 解析错误:格式不正确的“第 1 行,第 2 列”
- c# - POST 请求重定向,但是 AllowAutoRedirects = false 给出 302 异常,如何避免呢?
- python - TypeError:“PhotoImage”对象不可迭代
- python - 如何将默认参数添加到单击选项python
- windows - Ansible:Windows 归档模块
- android - 如何修复模拟器:在 127.0.0.1:8554 错误处启动 GRPC 服务器?
- php - Youtube Echo 输出错误,为什么?
- ios - 在 Swift 中以编程方式选择表格单元格
- css - 为什么将 CSS 文件添加到 Shiny navbarPage 会创建一个空白选项卡?