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 是否以及如何与他们相关。