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)超えます。すでに私は、ここで Ada に関する私の限られた知識に反対しています。それを解決する一般的な方法はありますか？この特定のケースでの問題を回避するために、仕様を直観的ではないが同等のものに修正しました。Positive'LastNatural'Last
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]
ここでのエラーのほとんどは、私には基本的な意味があります。Natural'Last最初のオーバーフロー チェックから始めて、GNATprove はループが反復回数未満で終了すること(またはまったく終了しないこと) を証明できないため、I := I + 1オーバーフローしていないことを証明できません。Remainingが減少しているため、そうではないことがわかっています。ループ バリアントを追加してこれを表現しようとしましpragma Loop_Variant (Decreases => Remaining)たが、GNATprove はそのループ バリアントを証明できましたが、おそらく、ループがまったく終了することを証明することは、反復回数I := I + 1未満で終了することを証明することと同等ではないため、 の潜在的なオーバーフローは変更されていません。Positive'Lastより厳しい制約は、ループが最大Positive'Size反復で終了することを示しますが、それを証明する方法がわかりません。代わりに、追加して「強制」しましたpragma Assume (I <= Remaining'Size); これが悪い習慣であることは承知しています。ここでの意図は、この最初の問題を「隠ぺい」してどこまで到達できるかを確認することだけでした。予想どおり、この仮定により、証明者は実装ファイル内のすべての範囲チェックを証明できます。サブ質問 2:Iがこのループでオーバーフローしないことを証明する正しい方法は何ですか?
しかし、事後条件の証明に関してはまだ進歩がありません。ループ不変条件が明らかに必要です。ループの先頭で保持される 1 つのループ不変条件は、次のとおりです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) 補題が提供されない限り GNAT がそれを知ることはないと思います。(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;
これは私にとって直感的ではない実装です。この 2 番目の実装についてはあまり詳しく説明しませんでしたが、試したことを示すためにここに残します。主な質問に対する他の解決策の潜在的な手段を提供する。追加のサブ質問を提起します。
ここでのアイデアは、終了と範囲を明示的にすることで、I のオーバーフローと終了条件に関する証明の一部をバイパスすることでした。少し驚いたことに、証明者は式のオーバーフロー チェックで最初に窒息しました2**I。2**(X'Size - 1)私は証明できる範囲内にあると予想していましたX-- しかし、繰り返しますが、私は Ada の知識の限界に直面しています。サブ質問 4:この式は実際に Ada でオーバーフローがないのでしょうか? また、それをどのように証明できますか?
これは長い質問であることが判明しました...しかし、私が提起している質問は、ほとんど自明な例のコンテキストで、比較的一般的であり、私のようにしようとしている他の人に役立つ可能性が高いと思います. Spark が彼らに関連しているかどうか、またどのように関連しているかを理解します。