合同关键软件的 Ada 设计

Question

我有一个与在关键环境中应用合同相关的问题。

想象我有以下函数要除法：

function div (dividend, divisor : Float) return Float
with Pre => divisor /= 0;

好吧，对我来说，先决条件是函数签名的一部分，每个客户端都必须了解合约，如果客户端将零传递给除数参数，则是其错误，因为他违反了合约，因此也违反了函数将失败。在测试中，激活先决条件后，代码将无法显示合同违规，而在生产中，如果先决条件已停用，则代码将无法引发约束。

由于约束错误在关键环境中是不可接受的，这就是客户要求我实现的，调用管理不一致的模块：

function div (dividend, divisor : Float) return Float is
begin
  if divisor = 0 then
    InconsistencyManager.inconsistency ("Some Log"); --It firstly logs a message and then does an infinite loop
  end;

  return dividend / divisor; --If everything is ok, return the division
end div;

对我来说，函数的这种副作用非常奇怪，对我来说，违反合同就像将错误的类型传递给子程序一样，不同之处在于，这种错误是在编译时捕获的，并且违反了合同，如果有的话没有足够的测试，可能会在已经安装时停止程序的执行。

你真的需要防范这样的人类愚蠢行为吗？你真的必须惩罚函数的执行吗？

Answer 1

您的客户要求您做的事情——检查子程序中的先决条件，然后调用“不一致管理器”——在我看来是老式的方式。如果出现不一致并导致无限循环，“关键系统”会发生什么情况？崩溃和燃烧？或者是否有一个冗余系统可以接管？这并不总是有效，例如 Ariane 501 发射失败，两台热冗余计算机都遇到了相同的“不一致”，并且可以预见如此。

老式的方法对于完全覆盖来说也是一种野兽。

IMO 今天要走的路是有一个前提条件，就像在第一个代码示例中一样，然后使用证明者——CodePeer、SPARK、GNATprove——在执行之前一劳永逸地证明前提条件永远不会违反（除非出现硬件错误，但如果您预计出现硬件错误，则您的关键系统会出现更大的问题）。

但是，如果您的实际代码确实具有浮点参数，请注意，测试除数（完全）等于零 (0.0) 并不能防止所有溢出。您需要一些更智能的数值分析来检查前提条件实际上应该是什么，同时考虑除数和被除数。

Answer 2

您不需要使用先决条件来实现您的预期目标。您可以使用 static_predicate 定义除数参数的子类型。

with Ada.Text_IO; use Ada.Text_IO;

procedure subtype_test is
   subtype divisor_type is float with
     static_predicate => divisor_type /= 0.0;
   function div (dividend : float; divisor : divisor_type) return float is
   begin
      return dividend / divisor;
   end div;
   
   divisors : array (1 ..2) of float := (0.1, 0.0);   
   dividend : float := 10.0;

begin
   for value of divisors loop
      if value in divisor_type then
         Put_Line("Result: " & float'Image(div(dividend, value)));
      else
         Put_Line("Logging error -> Divisor equals 0.0");
      end if;
   end loop;
end subtype_test;

在这种情况下，调用子程序必须检查除数的正确性并执行错误记录，而不是调用 div 函数。如上所示使用子类型可以让调用子程序在调用 div 函数之前轻松检查参数的有效性。