dafny中的指數法：不變式可能不會被維護

Question

我開始學習Dafny並學習了不變式。我有這樣的代碼：

function pot(m:int, n:nat): int 
{ 
    if n==0 then 1 
    else if n==1 then m 
    else if m==0 then 0 
    else pot(m,n-1) * m 
} 
method Pot(m:int, n:nat) returns (x:int) 
ensures x == pot(m,n) 
{ 
    x:=1; 
    var i:=0; 
    if n==0 {x:=1;} 
    while i<=n 
    invariant i<=n; 
    { 
    x:=m*x; 
    i:=i+1; 
    } 
} 

而給出的錯誤如下：「該循環不變量可能不被循環維護。」我想我可能需要另一個不變量，但我認爲我的代碼是正確的，除此之外（我猜）。任何幫助表示讚賞。提前致謝。

Answer 1

無論何時評估循環分支條件，循環不變都必須保持。但在循環的最後一次迭代中，i實際上是n+1，所以循環不變是不正確的。

將環路不變量更改爲i <= n + 1或將環路分支條件更改爲i < n將解決此特定問題。

之後，您仍然會做一些工作來完成證明方法的正確性。如果您遇到困難，請隨時提出進一步的問題。