我一直在尝试学习使用 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;
pragma Assertion_Policy (Check);
我的规格文件。