将 Dafny 中的两个整数与不变量相乘的简单方法答案

【问题标题】：Simple method to multiply two ints in Dafny with invariant将 Dafny 中的两个整数与不变量相乘的简单方法
【发布时间】：2018-05-28 15:56:29
【问题描述】：

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
}

【问题讨论】：

标签： methods dafny

【解决方案1】：

在尝试设计循环不变量时，首先向后工作会很有帮助。循环结束后你需要知道什么？

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

由于res 被循环改变，n0 * m0 == res 本身并不是一个不变量。相反，我们必须考虑循环如何朝着这个目标“取得进展”。这个循环通过将m 添加到res 来取得进展，大致来说，总共这样做了n 次。当n为0时，循环终止。

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

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

另外，Dafny Tutorial 有一个关于循环不变量的部分，这可能会有所帮助。

【讨论】：