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

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 编译器中运行它时，我得到以下信息：

后置条件可能不会在此返回路径上成立。（第 8 行）这是可能不成立的后置条件。（第 2 行）

Answer 1

问题是xandy可能相等，在这种情况下，bigandsmall也将相等。

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