如何编写关于读取堆的函数的 Dafny 公理？答案

【问题标题】：How can I write a Dafny axiom about a function that reads the heap?如何编写关于读取堆的函数的 Dafny 公理？
【发布时间】：2020-02-02 16:30:36
【问题描述】：

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

例如，我尝试编写一个名为 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} 注解在这种情况下没有任何作用。删除它将导致相同的错误消息。

【问题讨论】：

{:axiom} 注释只是告诉编译器你故意省略了函数体。验证者对无主体声明感到满意，但编译器会抱怨它们，除非它们被标记为 {:extern} 和 {:axiom}。

标签： dafny

【解决方案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)
}

【讨论】：