寻找最大和最小数

输入两个整数，返回两个值，它们经过+/-运算后较大的数和较小的数。

我们在函数体中定义较大值为两者加和，较小值为两者相减。

在返回值returns里我们可以定义变量more，less，以便在函数体中使用它们。

method Maxmin(x:int, y:int) returns (more:int, less:int)    
ensures y > 0 ==> less < x < more
ensures y < 0 ==> more < x < less  
{
    more := x + y;
    less := x - y;
}

其中，ensures代表后置条件，这里需要确保第二个数大于0时，较大数大于第一个数；第二个数小于0时，较小数大于第一个数。由于我们在函数体中定义较大值为两者加和，较小值为两者相减，显然在y < 0时是不成立的，利用这两个限定条件可以帮助Dafny判断该程序的正确性。