Dafny：BST 的 GetMax 方法验证

Question

为了验证以二叉树为输入并返回整数的 GetMax 方法的正确性，我想确保返回值确实是二叉树中存在的最大整数。我不明白 dafny 是如何接受返回值的。

datatype Tree = Empty | Node(left: Tree, value: int, right: Tree)

predicate BinarySearchTree(tree: Tree)
  decreases tree
{
  match tree
  case Empty => true
  case Node(_,_,_) =>
    (tree.left == Empty || tree.left.value < tree.value)
    && (tree.right == Empty || tree.right.value > tree.value)
    && BinarySearchTree(tree.left) && BinarySearchTree(tree.right)
    && maxValue(tree.left, tree.value)
}

predicate maxValue(tree: Tree, max: int)
  decreases tree
{
  match tree
  case Empty => true
  case Node(left,v,right) => (max > v) && maxValue(left, max) && maxValue(right, max)
}


method GetMax(tree: Tree) returns (res: int)
  requires BinarySearchTree(tree)

{
  match tree {
    case Empty => res := 0;
    case Node (Empty, value, Empty) => res := tree.value;
    case Node (left, value, Empty) => res := tree.value;
    case Node (left, value, right) =>
      var minval := tree.value;
      minval := GetMax(tree.right);
      var tmp := Node(tree.left, minval, tree.right);

      res := tmp.value;
      assert minval == tree.value;
      assert res >= minval;
      assert res >= tmp.value;
      assert tree.value <= res;
      assert Node(tree.left, tree.value, tree.right) == Node(tree.left,res,tree.right);
      assert maxValue(tree, tree.value) == maxValue(tree, res);
      assert forall x :: maxValue(tree, x) && x > value ==> tree.value <= res;
  }
}

所以它断言

assert forall x :: maxValue(tree, x) && x > value ==> tree.value <= res;

但我不知道如何确保返回值