function method pow(m:int, n: int):int
requires n>=0
{
if n==0 then 1
else if n==1 then m
else if n%2!=0 then m*pow(m,n-1)
else pow(m,n/2)*pow(m,n/2)
}
method check_even_power(x:int, y: int)
requires y>=0;
requires y % 2 == 0;
ensures pow(x, y / 2) * pow(x, y / 2) == pow(x, y);
{
}
method check_power(x:int, y: int)
requires y%2!=0
requires y>=0
ensures pow(x, y) == x * pow(x, y - 1);
{}
method power_binary(m:int, n: int) returns (Result: int)
requires n >= 0;
ensures Result == pow(m, n);
{
var x, y: int;
Result := 1;
x := m;
y := n;
while (y != 0)
invariant y >= 0;
invariant pow(m, n) == Result * pow(x, y) ;
{
if (y % 2 == 0)
{
check_even_power(x, y);
x := x * x;
y := y / 2;
}
else
{
check_power(x, y);
Result := Result * x;
y := y - 1;
}
}
}
我知道为什么编译器提到我这个循环不变可能不会由循环维护。我尝试得到反例，它得到m = 1，n = 20733，y = 20733，为什么代码得到while(y！=0)，y变成20730，如何解决它？
以下是调试此类内容的方法。
我建议您首先将失败的不变量复制到每个if分支的末尾，因为这可以让您查看哪个分支(或两个分支)有问题。循环中的if语句如下所示：
if y % 2 == 0 {
check_even_power(x, y);
x := x * x;
y := y / 2;
assert pow(m, n) == Result * pow(x, y);
} else {
check_power(x, y);
Result := Result * x;
y := y - 1;
assert pow(m, n) == Result * pow(x, y);
}
对于第一个断言，您将收到错误，但第二个断言不会收到错误报告。这很好，因为它告诉你把注意力集中在"然后"分支上。
接下来，如果你想在赋值a := E;之后证明条件X，那么你在赋值之前必须证明的条件是X，但每次出现a都被E替换。在您的情况下，断言之前有两个赋值，因此应用这些替换会使您的"then"分支如下所示：
check_even_power(x, y);
assert pow(m, n) == Result * pow(x * x, y / 2); // (2)
x := x * x;
assert pow(m, n) == Result * pow(x, y / 2); // (1)
y := y / 2;
assert pow(m, n) == Result * pow(x, y); // (0)
验证者现在抱怨 (2)，但不抱怨 (1) 或 (0)。这意味着如果你能证明(2)，其他一切都会证明。
为了证明(2)，你必须多做一点工作。我认为找出这里出了什么问题的最佳技术是使用证明计算，您可以使用calc语句进行计算。首先将 (2) 的相等性添加到您放在断言 (2) 之前的calc语句中：
check_even_power(x, y);
calc {
pow(m, n);
== // error
Result * pow(x * x, y / 2);
}
assert pow(m, n) == Result * pow(x * x, y / 2);
验证者现在将抱怨它无法证明calc中的步骤。我在上面写了// error，以表明验证者在哪里抱怨。有了这个calc声明，验证者不再抱怨断言(2)。这很好，因为现在您需要做的就是完成calc。
让我们从calc的顶部开始.你对pow(m, n)了解多少？好吧，您可以在进入循环时使用循环不变性。因此，您可以将以下步骤添加到计算中：
check_even_power(x, y);
calc {
pow(m, n);
== // the invariant on entry
Result * pow(x, y);
== // error
Result * pow(x * x, y / 2);
}
接下来，如何让中线的pow(x, y)更像最后一行的pow(x * x, y / 2)？使用从check_even_power(x, y)获得的属性：
check_even_power(x, y);
calc {
pow(m, n);
== // the invariant on entry
Result * pow(x, y);
== // check_even_power(x, y)
Result * (pow(x, y / 2) * pow(x, y / 2));
== // error
Result * pow(x * x, y / 2);
}
我把括号放在(pow(x, y / 2) * pow(x, y / 2))周围，因为我想确保乘法不会以某种方式重新关联。事实证明，用于证明目的的乘法是左关联的，因此您不需要括号。我的建议是，您首先添加括号以确保证明步骤正在执行您期望的功能。然后，如果可行，请尝试删除括号或根据自己的喜好清理公式。您还可以在校样计算的附加步骤中进行清理。
现在让我插入一个提示：您已将check_even_power和check_power声明为方法。这有效，但可以改进。这两种方法只是为了帮助证明，所以我建议你用lemma而不是method来声明它们。这也意味着您可以在证明计算的提示中引用它们，这使您的证明看起来不错，并将引理属性的使用隔离到计算中的该步骤。结果如下所示：
calc {
pow(m, n);
== // the invariant on entry
Result * pow(x, y);
== { check_even_power(x, y); }
Result * (pow(x, y / 2) * pow(x, y / 2));
== // error
Result * pow(x * x, y / 2);
}
现在，如果你能证明最后一步，你就完成了。但是证明pow(a, b) * pow(a, b)等于pow(a * a, b)需要归纳证明。因此，您需要做的是定义另一个引理，该引理声明此属性。然后，将我的注释// error替换为对新引理的适当调用。引理调用将位于提示中，就像对check_even_power的调用一样，因此您需要将其放在大括号中。
当证明通过时，您可以根据自己的口味清理东西。例如，您可以删除我上面添加的一些assert语句，以便调试问题。