Dafny function-by-method fails to prove correct post-conditions

Question

My codes only contains function clauses, but I need travel some sets. According to the official documentation , I use the code to travel my set:

      var node_set := tree_nodes(t);
      var result := 0.0;
      while node_set != {}
        decreases |node_set|
        // some invariants here, omitted
      {
        // some statements here, omitted
      }

But I wanna keep my code with function type, so I use function-by-method from here. So that the code looks like

function tree_height(t: Tree) : (h: real)
// some ensures here, omitted
{
  match t
  case Empty => 0.0
  case Node(_, _, _, _, _) =>
    // code omitted here
}by method{
  match t
  case Empty =>
    {
      h := 0.0;
      return;
    }
  case Node(_, _, _, _, _) =>
    {
      // code to travel sets omitted here
      h := result;
      return;
    }
}

But dafny said the post-conditions cannot be maintained. However, I split the two parts(function body and method body) like

function tree_height(t: Tree) : (h: real)
// some ensures here, omitted
{
  match t
  case Empty => 0.0
  case Node(_, _, _, _, _) =>
    // code omitted here
}

And

method test(t: Tree) returns (h: real)
// some ensures here, omitted
{
  match t
  case Empty =>
    {
      h := 0.0;
      return;
    }
  case Node(_, _, _, _, _) =>
    {
      // code omitted here
      h := result;
      return;
    }
}

In this way, function and method both passed the verification. Statements in function body and method body are the same with those in function-by-method.

Someone knows why? Or some ways to travel sets in function body?

And now I find another simple example that shares the same problem:

function setToSequence(s: set<int>) : (r: seq<int>)
  ensures multiset(s) == multiset(r)
{
  []
} by method{
  var copy := s;
  r := [];
  while copy != {}
    decreases |copy|
  {
    var k: int :| k in copy;
    r := r + [k];
    copy := copy - {k};
  }
}

method t(s: set<int>) returns (r: seq<int>)
{
  var copy := s;
  r := [];
  while copy != {}
    decreases |copy|
  {
    var k: int :| k in copy;
    r := r + [k];
    copy := copy - {k};
  }
}

Answer 1

The by-method clause is meant to add an efficient implementation of the function (note that functions are by default non-ghost since Dafny 4). The function part and the method part should give the same result. This is what Dafny complains about. In setToSequence, the function part produces only [], which is in general not the same as the method part produces. This answers your question why it does not verify.

Does it have to do with your way of visiting all elements in the set (traveling the set)? Partly. Your technique with the :| operator is fine. It is, however, non-deterministic. The consequence is that the function and the method part of setToSequence will (almost) never give the same result. I don't think the function-by-method declaration can be used here. Unless you come up with a deterministic definition by, e.g., sorting the elements, but that will not be practical and the idea of an efficient method definition will be defeated. Instead, you can use the separate definitions and add a lemma stating that they produce the same multisets (but not the same sequences).

Regarding the larger example with the trees, this confuses me. The node_depth of a node may change when the tree is reflected. See for instance the following code, that verifies.

var u := Node(3, Empty, Empty);
var t := Node(1, Node(2, u, Empty), u);
assert node_depth(t, u) == 2.0;

var t' := Node(1, u, Node(2, u, Empty));
assert node_depth(t', u) == 1.0;

Since the max_depth_node of both trees is u, the tree height of t will be 2.0, whereas the height of t' will be 1.0. Which is not what one would expect of a tree height definition. Therefore, I have not further investigated this example.