如何在SPARK中為遞回函式制定前、后條件？

下面的例子說明了這些整數在后置條件中的用法。

一些最后的注釋：

• Subprogram_Variant方面只需要證明一個遞回子程式最終會終止。這樣的終止證明必須通過向函式添加注解來明確要求（也顯示在下面的例子中，并在評論中由@egilhh指出的SPARK檔案中討論）。然而，對于你最初的目的來說，Subprogram_Variant方面是不需要的：證明某個尾部遞回求和函式的結果等于某個值N的特定遞回求和函式的結果。

• 要編譯一個使用新的Ada 202x標準庫中的函式的程式，使用編譯器選項-gnat2020。

• 雖然我使用子型別來約束N的允許值范圍，但你也可以使用一個前提條件。這不應該有任何區別。然而，在SPARK（也包括Ada）中，一般認為盡可能使用（子）型別來表達約束是一種最佳做法。

• 將反例視為可能的線索而不是事實。它們可能有意義，也可能沒有意義。反例是由一些求解器選擇性地生成的，可能沒有意義。參見SPARK用戶指南中的7.2.6節。

main.adb

用Ada.Numerics.Big_Numbers.Big_Integers;

帶有SPARK_Mode的程序Main是
   
   包BI重命名Ada.Numerics.Big_Numbers.Big_Integers。
   使用型別BI.Valid_Big_Integer。
   
   -- 轉換函式。
   function To_Big (Arg : Integer) return BI.Valid_Big_Integer 重命名BI.To_Big_Integer。
   function To_Int (Arg : BI.Valid_Big_Integer) return Integer 重命名BI.To_Integer。
      
   子型別Domain是自然范圍0 ... 2**16 - 1。
   
   函式 Sum (N : Domain) 回傳 Natural 是
     (如果N=0則為0，否則N Sum(N-1))
       與
         Post => Sum'Result = To_Int (To_Big (N) * (1   To_Big (N)) / 2),
         Subprogram_Variant => (Decreases => N);
   
   -- 要求證明Sum對所有可能的N值都會終止。
   pragma Annotate (GNATprove, Terminating, Sum);
   
開始
   null。
結束主。

輸出（gnatprove）

$ gnatprove -Pdefault.gpr --output=oneline --report=all --level=1-prover=z3
第2階段：生成全球合同 ...
第2階段：流程分析和證明 ...
main.adb:13:13: 資訊：子程式 "Sum "將終止，終止注釋已被證明。
main.adb:14:30: 資訊：溢位檢查已證明
main.adb:14:32: 資訊：子程式變體已被證明
main.adb:14:39: 資訊：范圍檢查已證明
main.adb:16:18: 資訊：后置條件已證明
main.adb:16:31: 資訊：范圍檢查已證明。
main.adb:16:53: 資訊: 謂詞檢查已證明
main.adb:16:69: 資訊：證明了除法檢查。
main.adb:16:71: 資訊: 謂詞檢查已證明
摘要登錄[...]/gnatprove.out

補充說明（針對評論）

因此，你可以將后置條件添加為遞回函式，但這對證明不存在溢位沒有幫助；你仍然必須對函式結果提供一些上限，以便說服驗證者，運算式N Sum (N - 1)不會導致溢位。

為了檢查加法程序中是否存在溢位，驗證者將考慮Sum根據其規范可能回傳的所有可能的值，并查看這些值中是否至少有一個可能導致加法溢位。在后置條件中沒有明確的約束，Sum可能根據其回傳型別，回傳Natural'Range范圍內的任何值。這個范圍包括Natural'Last，這個值肯定會導致溢位。因此，驗證器將報告說加法可能溢位。事實上，Sum在其允許的輸入值下從未回傳該值，這與此無關（這就是為什么它報告might）。因此，我們需要一個關于回傳值的更精確的上限值。

如果精確的上界不可用，那么你通常會退回到一個更保守的邊界，例如，在這種情況下，N * N（或者使用飽和數學，如SPARK用戶手冊中的斐波那契例子所示，5.2.7節，但是這種方法會改變你的函式，可能不可取）。

這里有一個替代的例子：

example.ads

package Example的SPARK_Mode是

   子型別Domain是自然范圍0 ... 2**15。

   函式Sum (N : Domain) 回傳Natural
     with Post => 
       Sum'Result = (if N = 0 then 0 else N   Sum (N - 1)) and
       Sum'Result <= N * N; -- 保守的上界，如果封閉形式的
                              -- 遞回函式的封閉形式的解將
                              --不存在。
結束示例。

example.adb

帶有SPARK_Mode的package body Example是

   函式 Sum (N : Domain) 回傳 Natural 是
   開始
      如果N=0，那么
         回傳N。
      否則
         回傳 N   Sum (N - 1)。
      end if;
   結束Sum。

結束示例。

output (gnatprove)

$ gnatprove -Pdefault.gpr --output=oneline --report=all
第2階段：生成全球合同 ...
第2階段：流程分析和證明 ...
example.adb:8:19: 資訊：溢位檢查已被證明
example.adb:8:28: 資訊：范圍檢查已證明
example.adb:7:08: 資訊：后置條件被證明。
example.adds:7:45: 資訊：溢位檢查已證明
example.adds:7:54: 資訊：范圍檢查已證明
摘要登錄[...]/gnatprove.out

uj5u.com熱心網友回復：

我找到了一些有時能起作用的東西，我認為這對于關閉標題問題來說已經足夠了：

函式Sum(sum)()()

function Sum (n : in Natural) return Natural
是
  (如果n = 0，那么0，否則n   Sum(n - 1))
    與
      Pre => (n in 0 ... 10), -- 與--prover=z3一起作業，不是Default (CVC4)
      -- Pre => (n in 0 ... 100), -- 不作業 -- "溢位檢查可能失敗，例如當n = 2時"
      Subprogram_Variant => (Decreases => n),
      Post => ((n = 0 and then Sum'Result = 0)
               或（n > 0然后Sum'Result = n   Sum(n - 1)））。
      -- Contract_Cases => (n = 0 => Sum'Result = 0,
      -- n > 0 => Sum'Result = n   Sum(n - 1)); -- 警告：在其后置條件中呼叫 "Sum "會導致無限遞回。
      -- Contract_Cases => (n = 0 => Sum'Result = 0,
      -- n > 0 => n   Sum(n - 1) = Sum'Result); -- 有效
      -- Contract_Cases => (n = 0 => Sum'Result = 0。
      -- n > 0 => Sum'Result = n * (n   1) / 2); -- 有效，并對高n給出了良好的溢位反例，但并不是真正的遞回