ada - 前置条件和后置条件是否取代了函数验证？

Question

我一直在尝试学习使用 SPARK 的基础知识，并且我对使用前置条件和后置条件有所了解，但我不确定它们是否可以代替验证？例如，除非所有门都关闭并锁定，否则飞机不会切换到起飞模式的功能。我是否需要在程序主体中添加代码来停止这种行为，或者前置条件和后置条件是否足够？我不清楚，因为我的类(class)教程实际上都没有这样做，但是当我测试程序时，我不受限制违反条件。

Answer 1

第一种:如果你使用 GNAT 编译器，你必须在编译器标志中添加标志 -gnata 或使用 GNAT 的配置文件和 pragma Assertion_Policy(Check); 来启用对前置条件和后置条件的检查。如果没有这些选项之一，所有检查都将被忽略。这就是为什么你可以违反它们。

先决条件发生在所选子程序执行之前。例如，函数声明为:

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;