Как я могу написать аксиому Дафни о функции, которая читает кучу? - PullRequest
Новая
       13

Как я могу написать аксиому Дафни о функции, которая читает кучу?

3 голосов
/ 04 октября 2019

Есть ли способ кодировать функцию, которая читает кучу и возвращает независимый от кучи снимок? Это было бы очень полезно для экспериментальной кодировки, которую я хотел бы разработать.

Например, я попытался написать функцию Dafny с именем edges, которую планирую использовать только для спецификаций. Он должен принимать набор 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} не содержитэффект в этом контексте. Удаление приведет к тому же сообщению об ошибке.

1 Ответ

2 голосов
/ 04 октября 2019

Я не знаю ответа на ваш общий вопрос, но я полагаю, что вы можете зафиксировать постусловие для вашего конкретного примера с помощью: 

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)
}
...