我如何编写有关读取堆的函数的Dafny公理?

问题描述 投票:2回答:1

是否可以对读取堆并返回与堆无关的快照的函数进行编码?这对于我想开发的实验编码将非常有用。

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

dafny
1个回答
0
投票

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

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)
}
© www.soinside.com 2019 - 2024. All rights reserved.