ada - 在 Spark 中证明 Floor_Log2

Question

Spark 的新手，Ada 的新手，所以这个问题可能过于宽泛。但是，作为理解 Spark 的尝试的一部分，它是真诚地询问的。除了直接回答以下问题外，我还欢迎对风格、工作流程等提出批评。

作为我第一次涉足 Spark，我选择尝试实现（简单）并证明正确性（迄今为止不成功）该功能。

问题：实现和证明此功能正确性的正确方法是什么？

我从以下开始util.ads：

package Util is
   function Floor_Log2(X : Positive) return Natural with
     Post => 2**Floor_Log2'Result <= X and then X < 2**(Floor_Log2'Result + 1);    
end Util;

我没有先决条件，因为输入的范围完全表达了唯一有趣的先决条件。我根据数学定义写的后置条件；但是，我在这里有一个直接的担忧。如果X是Positive'Last，则2**(Floor_Log2'Result + 1)超过Positive'Last和Natural'Last。我已经在这里反对我对 Ada 的有限知识，所以：子问题 1：后置条件中子表达式的类型是什么，这是溢出问题吗？有没有通用的方法来解决它？为了避免这种特殊情况下的问题，我将规范修改为不太直观但等效的：

package Util is
   function Floor_Log2(X : Positive) return Natural with
     Post => 2**Floor_Log2'Result <= X and then X/2 < 2**Floor_Log2'Result;
end Util;

有很多方法可以实现这个功能，我现在并不特别关心性能，所以我对其中任何一种都很满意。我认为“自然”实现（鉴于我特定的 C 背景）类似于以下内容util.adb：

package body Util is
   function Floor_Log2 (X : Positive) return Natural is
      I : Natural := 0;
      Remaining : Positive := X;
   begin
      while Remaining > 1 loop
         I := I + 1;
         Remaining := Remaining / 2;
      end loop;
      return I;
   end Floor_Log2;
end Util;

正如预期的那样，尝试在没有循环不变量的情况下证明这一点会失败。结果（此结果和所有结果均为 GNATprove 级别 4，从 GPS 调用为gnatprove -P%PP -j0 %X --ide-progress-bar -u %fp --level=4 --report=all）：

util.adb:6:13: info: initialization of "Remaining" proved[#2]
util.adb:7:15: info: initialization of "I" proved[#0]
util.adb:7:17: medium: overflow check might fail[#5]
util.adb:8:23: info: initialization of "Remaining" proved[#1]
util.adb:8:33: info: range check proved[#4]
util.adb:8:33: info: division check proved[#8]
util.adb:10:14: info: initialization of "I" proved[#3]
util.ads:3:14: medium: postcondition might fail, cannot prove 2**Floor_Log2'Result <= X[#7]
util.ads:3:15: medium: overflow check might fail[#9]
util.ads:3:50: info: division check proved[#6]
util.ads:3:56: info: overflow check proved[#10]

这里的大多数错误对我来说都是基本的。从第一次溢出检查开始，GNATprove 无法证明循环在少于Natural'Last迭代次数（或根本没有？）内终止，因此它无法证明I := I + 1没有溢出。我们知道情况并非如此，因为Remaining正在减少。我试图通过添加循环变体来表达这一点pragma Loop_Variant (Decreases => Remaining)，并且 GNATprove 能够证明循环变体，但潜在的溢出I := I + 1没有改变，推测是因为证明循环完全终止并不等于证明它在少于Positive'Last迭代中终止。更严格的约束将表明循环最多在Positive'Size迭代中终止，但我不确定如何证明这一点。相反，我通过添加一个“强迫它”pragma Assume (I <= Remaining'Size); 我知道这是不好的做法，这里的目的纯粹是为了让我看看我能在第一期“被掩盖”的情况下走多远。正如预期的那样，这个假设让证明者可以证明实现文件中的所有范围检查。子问题2：证明I在这个循环中不溢出的正确方法是什么？

但是，我们在证明后置条件方面仍然没有取得任何进展。显然需要循环不变量。保持在循环顶部的一个循环不变量是pragma Loop_Invariant (Remaining * 2**I <= X and then X/2 < Remaining * 2**I); 除了为真之外，该不变量还有一个很好的特性，即当循环终止条件为真时，它显然等同于后置条件。然而，正如预期的那样，GNATprove 无法证明这个不变量：medium: loop invariant might fail after first iteration, cannot prove Remaining * 2**I <= X[#20]. 这是有道理的，因为这里的归纳步骤是不明显的。通过对实数进行除法，可以想象一个简单的引理说明for all I, X * 2**I = (X/2) * 2**(I+1)，但是（a）我不希望 GNATprove 在没有提供引理的情况下知道这一点，并且（b）整数除法更加混乱。那么，子问题 3a：这是尝试用来证明此实现的适当循环不变量吗？子问题 3b：如果是这样，证明它的正确方法是什么？从外部证明一个引理并使用它？如果是这样，那究竟是什么意思？

在这一点上，我想我会探索一个完全不同的实现，只是看看它是否会导致不同的地方：

package body Util is
   function Floor_Log2 (X : Positive) return Natural is
   begin
      for I in 1 .. X'Size - 1 loop
         if 2**I > X then
            return I - 1;
         end if;
      end loop;
      return X'Size - 1;
   end Floor_Log2;
end Util;

这对我来说是一个不太直观的实现。我没有过多地探索第二个实现，但我把它留在这里展示我尝试了什么；为主要问题的其他解决方案提供潜在途径；并提出额外的子问题。

这里的想法是通过明确终止和范围来绕过 I 和终止条件溢出的一些证明。令我惊讶的是，证明者首先在溢出检查表达式时窒息2**I。我曾期望2**(X'Size - 1)可以证明在范围内X——但我又一次遇到了我的 Ada 知识的限制。子问题 4：这个表达式在 Ada 中实际上是无溢出的吗？如何证明？

事实证明这是一个很长的问题......但我认为我提出的问题，在一个几乎微不足道的例子的背景下，是相对普遍的，并且可能对像我一样试图尝试的其他人有用了解 Spark 是否以及如何与他们相关。

标签： adaformal-verificationada2012spark-2014

Answer 1

我无法回答您的 SPARK 问题，但我可以回答您的一些子问题。

子问题 1：由于您使用"<"的是整数，子表达式也将是整数类型。对于Positive'Last( 2 ** 31 - 1with GNAT)，你的函数结果应该是 30，子表达式会溢出。（这是从 SPARK 的角度来看的；编译器在评估表达式时允许使用更大范围的类型以获得数学/逻辑上正确的结果，即使子表达式会溢出，并且 GNAT 将对 -gnato 的某些值执行此操作。 )

子问题4：2 ** (X'Size - 1)可以溢出。原因与 2 个含义有关'Size：Positive'Size是存储子类型 Positive 的值所需的最小位数；X'Size是分配给 X 的实际位数。由于您使用的是 GNAT，

Integer'Last = Positive'Last = 2 ** 31 - 1. X'Size = 32. Positive'Size = 31.

所以，2 ** (X'Size - 1) = 2 ** 31 > Positive'Last。您可能想使用Positive'Size而不是X'Size.

（同样，从 SPARK 的角度来看；编译器可以得到逻辑上正确的结果。）

除了：短路形式and then，or else只应在实际需要时使用。现代处理器在机器代码级别进行各种优化，这些优化必须关闭才能进行短路评估。尽管它们可能看起来像优化，但实际上它们往往相反。

HTH。

（您可能想用 [ada] 标记它。我只看到它是因为您在 clada 中引用了它。）