简单方法后置条件可能不成立

Question

我在 Dafny 中使用这个简单的方法时遇到问题，我不知道为什么它不起作用。由于没有调试器，而且我是这种语言的新手，我希望有人能提供帮助。我认为规范不完整..

method Q2(x : int, y : int) returns (big : int, small : int) 
  ensures big > small;
{
  if (x > y)
    {big, small := x, y;}
  else
    {big, small := y, x;}
}

当我在 Microsoft dafny 编译器中运行它时，我得到以下信息：

此 return 路径可能不支持后置条件。（8 号线）这是可能不成立的后置条件。（第 2 行）

Answer 1

问题是 x 和 y 可能相等，在这种情况下，big 和 small 也将相等。

您可以通过将其更改为 big >= small 来修复后置条件。或者，您想禁止调用者传递等于 x 和 y，您可以添加一个前提条件，要求 x != y.

简单方法后置条件可能不成立

simple method postcondition might not hold

methods

dafny