Is there a data type in Dafny like List<T> in java?

userE38m1 0
Viewed 18

Is there a built-in data type in Dafny like List in Java (or any type for dynamic list)? I've looked for it in Dafny Reference Manual, but nothing found. It seems that a self-defined class must be defined for it. If it is the fact, then how can the performance be assured for the generated java program and how can the gernerality of Dafny as a programming language be assured? Not criticism, just curious.

dafny
1 Answers

Dafny's first collection is undoubtedly seq, which is an immutable list.

function sum(s: seq<int>): int {
  if |s| == 0 then 0 else s[0] + sum(s[1..])
}

For anything else, the Dafny team is working on a standard library, but you might be interestest by the first example given in the Dafny documentation that also explain why lists are non trivial objects to verify:

https://dafny.org/dafny/DafnyRef/DafnyRef#sec-example

In short, to define a list, you want to write a class and store a ghost model of all the elements to ensure there is no cycle, and possibly write this node into another data structure. But the proofs are not obvious. Here is what I got so far.

class ListNode<T> {
  var head: T
  var tail: ListNode?<T>
  ghost var Repr: seq<ListNode<T>>
  constructor(h: T, t: ListNode?<T>) requires t != null ==> t.Valid() ensures Valid()
  {
    head:= h;
    tail := t;
    Repr := [this] + (if t == null then [] else t.Repr);
  }

  predicate Valid() reads this, Repr decreases |Repr|
  {
    && |Repr| > 0
    && Repr[0] == this
    && (if tail == null then |Repr| == 1 else
        && |Repr| > 1
        && tail == Repr[1]
        && tail.Repr == Repr[1..]
        && tail.Valid())
  }

  lemma ReprAreDecreasing(i: int)
    requires Valid()
    requires 0 <= i < |Repr|
    ensures Repr[i].Repr == Repr[i..]
    ensures Repr[i].Valid()
  {
    if i == 0 {
    } else {
      tail.ReprAreDecreasing(i-1);
    }
  }
}

class List<T> {
  var head: ListNode?<T>
  var last: ListNode?<T>
  ghost var Repr: seq<ListNode<T>>

  constructor() ensures Valid() {
    head := null;
    last := null;
    Repr := [];
  }

  lemma ValidImpliesAllNodesValid(n: ListNode<T>)
    requires Valid()
    requires n in Repr
    ensures n.Valid() {
    if n == head {
      assert n.Valid();
    } else {
      var i :| 0 <= i < |Repr| && Repr[i] == n;
      head.ReprAreDecreasing(i);
    }
  }

  method Append(node: ListNode<T>)
  {
...
  }

  predicate Valid() reads this, Repr
  {
    (if head != null then
      && last != null
      && head in Repr
      && head.Repr == Repr
      && head.Valid()
      && last == head.Repr[|head.Repr|-1]
      && assert last.Repr == head.Repr[|head.Repr|-1..] by {
        head.ReprAreDecreasing(|head.Repr|-1);
      } last.Valid()
    else
      && last == null
      && |Repr| == 0)
  }
}

References: https://dafny.org/dafny/DafnyRef/DafnyRef#sec-seq-comprehension

Mikaël Mayer0
Related