Dafny的按方法进行的函数无法证明正确的后置条件。

huangapple go评论105阅读模式
英文:

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

问题

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 the function body and method body are the same as 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};
  }
}
英文:

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 =&gt; 0.0
  case Node(_, _, _, _, _) =&gt;
    // code omitted here
}by method{
  match t
  case Empty =&gt;
    {
      h := 0.0;
      return;
    }
  case Node(_, _, _, _, _) =&gt;
    {
      // 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 =&gt; 0.0
  case Node(_, _, _, _, _) =&gt;
    // code omitted here
}

And

method test(t: Tree) returns (h: real)
// some ensures here, omitted
{
  match t
  case Empty =&gt;
    {
      h := 0.0;
      return;
    }
  case Node(_, _, _, _, _) =&gt;
    {
      // 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&lt;int&gt;) : (r: seq&lt;int&gt;)
  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&lt;int&gt;) returns (r: seq&lt;int&gt;)
{
  var copy := s;
  r := [];
  while copy != {}
    decreases |copy|
  {
    var k: int :| k in copy;
    r := r + [k];
    copy := copy - {k};
  }
}

答案1

得分: 1

以下是您要翻译的内容:

“by-method”子句旨在为函数添加一个高效的实现(请注意,自 Dafny 4 起,函数默认为非幽灵函数)。函数部分和方法部分应该产生相同的结果。这就是 Dafny 抱怨的原因。在“setToSequence”中,函数部分仅产生 [],这通常与方法部分产生的结果不同。这回答了您为什么无法验证的问题。

这是否与您遍历集合中所有元素的方式有关?部分是的。您使用的“:|”操作符的技巧是正确的。但它是非确定性的。结果是,“setToSequence”的函数部分和方法部分几乎永远不会产生相同的结果。我认为在这里不能使用函数-方法声明。除非您提出一个确定性的定义,例如通过对元素进行排序,但那将不实际,而且高效方法定义的想法将被打败。相反,您可以使用单独的定义,并添加一个引理,说明它们产生相同的多重集(但不是相同的序列)。

至于更大的涉及树的示例,这让我感到困惑。树的节点深度在树被反射时可能会改变。例如,看下面的代码,可以验证。

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;

由于这两棵树的“max_depth_node”都是“u”,因此“t”的树高度将为2.0,而“t'”的高度将为1.0。这不符合人们对树高度定义的期望。因此,我没有进一步研究这个示例。

英文:

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 Dafny的按方法进行的函数无法证明正确的后置条件。 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&#39; := Node(1, u, Node(2, u, Empty));
assert node_depth(t&#39;, 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.

huangapple
  • 本文由 发表于 2023年8月9日 13:57:14
  • 转载请务必保留本文链接:https://go.coder-hub.com/76864933-2.html
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定