如何解决前置条件和后置条件是否代替了函数验证?
我一直在尝试学习使用 SPARK 的基础知识,并且我对使用前置和后置条件有所了解,但我不确定它们是否取代了验证?例如,除非所有门都关闭并锁定,否则飞机不会切换到起飞模式的功能。我是否需要向过程主体添加代码来阻止这种行为,或者前置和后置条件是否足够?我不清楚,因为我的课程教程实际上没有这样做,但是当我测试程序时,我没有违反条件。
解决方法
第一个:如果您使用 GNAT 编译器,则必须将标志 -gnata
添加到编译器标志或使用带有 pragma Assertion_Policy(Check);
的 GNAT 配置文件来启用对前置和后置条件的检查。如果没有这些选项之一,则所有检查都将被忽略。这就是为什么你可以违反它们。
先决条件发生在所选子程序执行之前之前。例如,函数声明为:
function Add(A,B: Positive) return Positive is (A + B) with
Pre => A < 10;
在执行函数之前会检查这个前提条件。例如:
I := Add(2,2);
Put_Line(Positive'Image(I)); -- prints 4 as expected
begin
I := Add(10,2); -- Crash,exception on violation of precondition
exception
when ASSERT_FAILURE =>
Put_Line(Positive'Image(I)); -- prints 4
end;
在子程序执行后检查后置条件。另一个例子:
procedure Increment(A: in out Positive) with
Post => A < 20 is
begin
A := A + 1;
end Increment;
和用法:
I := 2;
Increment(I);
Put_Line(Positive'Image(I)); -- prints 3
I := 19;
begin
I := Increment(I); -- Crash,exception on violation of postcondition
exception
when ASSERT_FAILURE =>
Put_Line(Positive'Image(I)); -- prints 19
end;
,
在许多情况下,可以在子程序内验证的 leu 中使用前置条件和后置条件。另一方面,有时子程序必须重复监视事件或条件,然后正确响应该事件或条件。在这些情况下,通常最好在子程序中执行该监控。
,我能够违反我的条件的原因是因为我需要启用thindil所述的条件断言。我通过添加解决了
pragma Assertion_Policy (Check);
到我的规范文件。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。