2

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

1 回答 1

2

在尝试设计循环不变量时,首先向后工作会很有帮助。循环终止后你需要知道什么?

对于此方法,一旦循环终止,您将需要建立后置条件n0 * m0 == res,因此这是我们循环不变量的起点。

由于res被循环改变,n0 * m0 == res它本身并不是一个不变量。相反,我们必须考虑循环如何朝着这个目标“取得进展”。粗略地说,这个循环通过添加mto 来取得进展res,总共这样做了几次。nn为 0 时,循环终止。

一个常见的模式在这里很有用:不变量应该谈论“到目前为止”已经完成的事情以及“剩下要做的事情”。在这种情况下,到目前为止所做res的是 ,剩下要做的n就是m. 循环的每次迭代都需要完成一项工作,并在保持不变的情况下完成它。

换句话说,这个循环的一个很好的不变量是res + n * m == n0 * m0.

此外,Dafny 教程有一个关于循环不变量的部分,这可能会有所帮助。

于 2017-12-19T18:14:36.210 回答