作为我第一次接触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.adbpackage 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是否与他们相关的人有用。
type Big is mod 2 ** Integer'Size;并将您的条件更改为2 ** Floor_Log2'Result <= Big (X) and Big (X) < 2 ** (Floor_Log2'Result + 1)等等，以避免溢出警告。 - Jeffrey R. Carter