dafny - 我如何编写关于读取堆的函数的 Dafny 公理？

Question

有没有一种方法可以对读取堆并返回与堆无关的快照的函数进行编码？这对于我想开发的实验编码非常有用。

例如，我尝试编写一个名为 edges 的 Dafny 函数，我打算仅将其用于规范。它应该采用一组 Node 对象并返回一组 Edge 对象。

class Node {
  var next: Node
  var val: int
  constructor (succ: Node, x: int) 
  {
    this.next := succ;
    this.val := x;
  }
} 

datatype Edge = Edge(x: Node, y: Node)

function{:axiom} edges(g: set<Node>): set<Edge>
  reads g
  ensures forall x:Node, y:Node {:trigger Edge(x,y)} ::
    x in g && x.next == y <==> Edge(x,y) in edges(g) 

但是，我从 Dafny(使用该工具的在线版本)收到以下错误消息:

Dafny 2.3.0.10506
stdin.dfy(26,10): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'x'
stdin.dfy(26,10): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'y'
2 resolution/type errors detected in stdin.dfy

似乎 {:axiom} 注释在此上下文中没有任何作用。删除它会导致相同的错误消息。

Answer 1

我不知道您一般问题的答案，但我相信您可以通过以下方式获取具体示例的后置条件:

function{:axiom} edges(g: set<Node>): set<Edge>
  reads g
  ensures edges(g) == set x : Node | x in g :: Edge(x, x.next)

您也可以只将该后置条件写为函数定义:

function{:axiom} edges(g: set<Node>): set<Edge>
reads g
{
  set x : Node | x in g :: Edge(x, x.next)
}

为了完整性，这里是完整的例子:

class Node {
  var next: Node
  var val: int
  constructor (succ: Node, x: int) 
  {
    this.next := succ;
    this.val := x;
  }
} 

datatype Edge = Edge(x: Node, y: Node)

function{:axiom} edges(g: set<Node>): set<Edge>
  reads g
  ensures edges(g) == set x : Node | x in g :: Edge(x, x.next)

function{:axiom} edges2(g: set<Node>): set<Edge>
reads g
{
  set x : Node | x in g :: Edge(x, x.next)
}