此Q3
方法通过将 m0 添加到 res |n0| 来对 n0 * m0 进行通勤。次。如果 n0 为负数,我们将 n0 和 m0 反转,因为 n0*m0 = -n0* -m0 成立。
我遇到的问题是我不完全知道我的不变量应该是什么样子,因为不变量需要是布尔类型。谁能告诉我不变的布尔条件可能是什么样的?我想了想Abs((n0)-n)*m == res
,但这行不通。
method Q3(n0 : int, m0 : int) returns (res : int)
ensures n0*m0 == res
{
var n, m : int;
res := 0;
if (n0 >= 0)
{n,m := n0, m0;}
else
{n,m := -n0, -m0;}
while (0 < n)
invariant Abs((n0)-n)*m
{
res := res + m;
n := n - 1;
}
}
function Abs(x: int): int
{
if x < 0 then -x else x
}