Exponentielle Methode in Dafny: Invariante möglicherweise nicht beibehalten

Question

Ich fing an, Dafny zu lernen, und ich habe gerade Invarianten gelernt. Ich habe diesen Code bekam:

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; 
    } 
} 

und der gegebenen Fehler ist folgende: „Diese Schleifeninvariante möglicherweise nicht durch die Schleife aufrechterhalten werden“ Ich denke, ich könnte eine andere Invariante brauchen, aber ich denke mein Code ist anders als das (denke ich). Jede Hilfe wird geschätzt. Danke im Voraus.

Answer 1

Eine Schleifeninvariante muss immer dann gültig sein, wenn die Schleifenverzweigungsbedingung ausgewertet wird. Aber bei der letzten Iteration Ihrer Schleife wird i tatsächlich n+1 sein, also ist die Schleifeninvariante dann nicht wahr.

Durch Ändern der Schleifeninvariante nach i <= n + 1 oder Ändern der Schleifenzweigbedingung in i < n wird dieses spezielle Problem behoben.

Danach haben Sie noch etwas zu tun, um die korrekte Methode zu beweisen. Fühlen Sie sich frei, weitere Fragen zu stellen, wenn Sie nicht weiterkommen.