Dafny:

* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks

5 files changed, 409 insertions, 0 deletions

diff --git a/Test/vacid0/Answer b/Test/vacid0/Answer
new file mode 100644
index 00000000..6f270f92
--- /dev/null
+++ b/Test/vacid0/Answer
@@ -0,0 +1,12 @@
+

+-------------------- LazyInitArray.dfy --------------------

+

+Dafny program verifier finished with 7 verified, 0 errors

+

+-------------------- SparseArray.dfy --------------------

+

+Dafny program verifier finished with 9 verified, 0 errors

+

+-------------------- Composite.dfy --------------------

+

+Dafny program verifier finished with 14 verified, 0 errors

diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy
new file mode 100644
index 00000000..28074c7b
--- /dev/null
+++ b/Test/vacid0/Composite.dfy
@@ -0,0 +1,160 @@
+class Composite {

+  var left: Composite;

+  var right: Composite;

+  var parent: Composite;

+  var val: int;

+  var sum: int;

+

+  function Valid(S: set<Composite>): bool

+    reads this, parent, left, right;

+  {

+    this in S &&

+    (parent != null ==> parent in S && (parent.left == this || parent.right == this)) &&

+    (left != null ==> left in S && left.parent == this && left != right) &&

+    (right != null ==> right in S && right.parent == this && left != right) &&

+    sum == val + (if left == null then 0 else left.sum) + (if right == null then 0 else right.sum)

+  }

+

+  function Acyclic(S: set<Composite>): bool

+    reads S;

+  {

+    this in S &&

+    (parent != null ==> parent.Acyclic(S - {this}))

+  }

+

+  method Init(x: int)

+    modifies this;

+    ensures Valid({this}) && Acyclic({this}) && val == x && parent == null;

+  {

+    parent := null;

+    left := null;

+    right := null;

+    val := x;

+    sum := val;

+  }

+

+  method Update(x: int, ghost S: set<Composite>)

+    requires this in S && Acyclic(S);

+    requires (forall c :: c in S ==> c != null && c.Valid(S));

+    modifies S;

+    ensures (forall c :: c in S ==> c.Valid(S));

+    ensures (forall c :: c in S ==> c.left == old(c.left) && c.right == old(c.right) && c.parent == old(c.parent));

+    ensures (forall c :: c in S && c != this ==> c.val == old(c.val));

+    ensures val == x;

+  {

+    var delta := x - val;

+    val := x;

+    call Adjust(delta, S, S);

+  }

+

+  method Add(ghost S: set<Composite>, child: Composite, ghost U: set<Composite>)

+    requires this in S && Acyclic(S);

+    requires (forall c :: c in S ==> c != null && c.Valid(S));

+    requires child != null && child in U;

+    requires (forall c :: c in U ==> c != null && c.Valid(U));

+    requires S !! U;

+    requires left == null || right == null;

+    requires child.parent == null;

+    // modifies only one of this.left and this.right, and child.parent, and various sum fields:

+    modifies S, child;

+    ensures child.left == old(child.left) && child.right == old(child.right) && child.val == old(child.val);

+    ensures (forall c :: c in S && c != this ==> c.left == old(c.left) && c.right == old(c.right));

+    ensures old(left) != null ==> left == old(left);

+    ensures old(right) != null ==> right == old(right);

+    ensures (forall c :: c in S ==> c.parent == old(c.parent) && c.val == old(c.val));

+    // sets child.parent to this:

+    ensures child.parent == this;

+    // leaves everything in S+U valid:

+    ensures (forall c :: c in S+U ==> c.Valid(S+U));

+  {

+    if (left == null) {

+      left := child;

+    } else {

+      right := child;

+    }

+    child.parent := this;

+    call Adjust(child.sum, S, S+U);

+  }

+

+  method Dislodge(ghost S: set<Composite>)

+    requires this in S && Acyclic(S);

+    requires (forall c :: c in S ==> c != null && c.Valid(S));

+    modifies S;

+    ensures (forall c :: c in S ==> c.Valid(S));

+    ensures (forall c :: c in S ==> c.val == old(c.val));

+    ensures (forall c :: c in S && c != this ==> c.parent == old(c.parent));

+    ensures (forall c :: c in S ==> c.left == old(c.left) || (old(c.left) == this && c.left == null));

+    ensures (forall c :: c in S ==> c.right == old(c.right) || (old(c.right) == this && c.right == null));

+    ensures Acyclic({this});

+  {

+    var p := parent;

+    parent := null;

+    if (p != null) {

+      assert (p.left == this) != (p.right == this);

+      if (p.left == this) {

+        p.left := null;

+      } else {

+        p.right := null;

+      }

+      var delta := -sum;

+      call p.Adjust(delta, S - {this}, S);

+    }

+  }

+

+  /*private*/ method Adjust(delta: int, ghost U: set<Composite>, ghost S: set<Composite>)

+    requires U <= S && Acyclic(U);

+    // everything else is valid:

+    requires (forall c :: c in S && c != this ==> c != null && c.Valid(S));

+    // this is almost valid:

+    requires parent != null ==> parent in S && (parent.left == this || parent.right == this);

+    requires left != null ==> left in S && left.parent == this && left != right;

+    requires right != null ==> right in S && right.parent == this && left != right;

+    // ... except that sum needs to be adjusted by delta:

+    requires sum + delta == val + (if left == null then 0 else left.sum) + (if right == null then 0 else right.sum);

+    // modifies sum fields in U:

+    modifies U`sum;

+    // everything is valid, including this:

+    ensures (forall c :: c in S ==> c.Valid(S));

+  {

+    var p := this;

+    ghost var T := U;

+    while (p != null)

+      invariant T <= U;

+      invariant p == null || p.Acyclic(T);

+      invariant (forall c :: c in S && c != p ==> c.Valid(S));

+      invariant p != null ==> p.sum + delta == p.val + (if p.left == null then 0 else p.left.sum) + (if p.right == null then 0 else p.right.sum);

+      invariant (forall c :: c in S ==> c.left == old(c.left) && c.right == old(c.right) && c.parent == old(c.parent) && c.val == old(c.val));

+      decreases T;

+    {

+      p.sum := p.sum + delta;

+      T := T - {p};

+      p := p.parent;

+    }

+  }

+}

+

+method Main()

+{

+  var c0 := new Composite;

+  call c0.Init(57);

+

+  var c1 := new Composite;

+  call c1.Init(12);

+  call c0.Add({c0}, c1, {c1});

+

+  var c2 := new Composite;

+  call c2.Init(48);

+

+  var c3 := new Composite;

+  call c3.Init(48);

+  call c2.Add({c2}, c3, {c3});

+  call c0.Add({c0,c1}, c2, {c2,c3});

+

+  ghost var S := {c0, c1, c2, c3};

+  call c1.Update(100, S);

+  call c2.Update(102, S);

+

+  call c2.Dislodge(S);

+  call c2.Update(496, S);

+  call c0.Update(0, S);

+}

diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy
new file mode 100644
index 00000000..6ae00e24
--- /dev/null
+++ b/Test/vacid0/LazyInitArray.dfy
@@ -0,0 +1,105 @@
+class LazyInitArray<T> {

+  ghost var Contents: seq<T>;

+  var Zero: T;

+  /*private*/ var a: array<T>;

+  /*private*/ var b: array<int>;

+  /*private*/ var c: array<int>;

+  /*private*/ var n: int;

+  /*private*/ ghost var d: seq<int>;

+  /*private*/ ghost var e: seq<int>;

+  function Valid(): bool

+    reads this, a, b, c;

+  {

+    a != null && b != null && c != null &&

+    |a| == |Contents| + 1 &&  // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'

+    |b| == |Contents| &&

+    |c| == |Contents| &&

+    b != c &&

+    0 <= n && n <= |c| &&

+    (forall i :: 0 <= i && i < |Contents| ==>

+       Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&

+    (forall i :: 0 <= i && i < |Contents| ==>

+              ((exists j :: 0 <= j && j < n && c[j] == i)

+               <==>

+               0 <= b[i] && b[i] < n && c[b[i]] == i)) &&

+    // The idea behind d and e is the following:

+    //  *  d is a permutation of the first |Contents| natural numbers

+    //  *  e describes which permutation d is

+    //  *  c[..n] == d[..n]

+    |d| == |Contents| &&

+    |e| == |Contents| &&

+    (forall i :: 0 <= i && i < n ==> c[i] == d[i]) &&

+    (forall i :: 0 <= i && i < |d| ==> 0 <= d[i] && d[i] < |d|) &&

+    (forall i :: 0 <= i && i < |e| ==> 0 <= e[i] && e[i] < |e|) &&

+    (forall i :: 0 <= i && i < |e| ==> d[e[i]] == i)

+  }

+

+  method Init(N: int, zero: T)

+    requires 0 <= N;

+    modifies this, a, b, c;

+    ensures Valid();

+    ensures |Contents| == N && Zero == zero;

+    ensures (forall x :: x in Contents ==> x == zero);

+  {

+    var aa := new T[N+1];  a := aa;

+    var ii := new int[N];  b := ii;

+    ii := new int[N];      c := ii;

+    n := 0;

+

+    // initialize ghost variable Contents to a sequence of length N containing only zero's,

+    // and ghost variables d and e to be the identity sequences of length N

+    ghost var s := [];

+    ghost var id := [];

+    ghost var k := 0;

+    while (k < N)

+      invariant k <= N;

+      invariant |s| == k && (forall i :: 0 <= i && i < |s| ==> s[i] == zero);

+      invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);

+    {

+      s := s + [zero];

+      id := id + [k];

+      k := k + 1;

+    }

+

+    d := id;

+    e := id;

+    Zero := zero;

+    Contents := s;

+  }

+

+  method Get(i: int) returns (x: T)

+    requires Valid();

+    requires 0 <= i && i < |Contents|;

+    ensures x == Contents[i];

+  {

+    if (0 <= b[i] && b[i] < n && c[b[i]] == i) {

+      x := a[i];

+    } else {

+      x := Zero;

+    }

+  }

+

+  method Set(i: int, x: T)

+    requires Valid();

+    requires 0 <= i && i < |Contents|;

+    modifies this, a, b, c;

+    ensures Valid();

+    ensures |Contents| == |old(Contents)| && Contents == Contents[i := x];

+    ensures Zero == old(Zero);

+  {

+    if (0 <= b[i] && b[i] < n && c[b[i]] == i) {

+    } else {

+      assert n <= e[i];

+      b[i] := n;

+      c[n] := i;

+      ghost var t := d[n];

+      ghost var k := e[i];

+      d := d[n := i][k := t];

+      e := e[i := n][t := k];

+      n := n + 1;

+    }

+

+    a[i] := x;

+    Contents := Contents[i := x];

+  }

+}

diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy
new file mode 100644
index 00000000..da1f63bb
--- /dev/null
+++ b/Test/vacid0/SparseArray.dfy
@@ -0,0 +1,120 @@
+class SparseArray<T> {

+  ghost var Contents: seq<T>;

+  var zero: T;

+  /*private*/ var a: seq<T>;  // should really be an array

+  /*private*/ var b: seq<int>;  // should really be an array

+  /*private*/ var c: seq<int>;  // should really be an array

+  /*private*/ var n: int;

+  /*private*/ ghost var d: seq<int>;  // would be better as an array

+  /*private*/ ghost var e: seq<int>;  // would be better as an array

+  function Valid(): bool

+    reads this;

+  {

+    |a| == |Contents| &&

+    |b| == |Contents| &&

+    |c| == |Contents| &&

+    0 <= n && n <= |c| &&

+    (forall i :: 0 <= i && i < |Contents| ==>

+       Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else zero)) &&

+    (forall i :: 0 <= i && i < |Contents| ==>

+              (i in c[..n] <==> 0 <= b[i] && b[i] < n && c[b[i]] == i)) &&

+    // The idea behind d and e is the following:

+    //  *  d is a permutation of the first |Contents| natural numbers

+    //  *  e describes which permutation d is

+    //  *  c[..n] == d[..n]

+    |d| == |Contents| &&

+    |e| == |Contents| &&

+    (forall i :: 0 <= i && i < n ==> c[i] == d[i]) &&

+    (forall i :: 0 <= i && i < |d| ==> 0 <= d[i] && d[i] < |d|) &&

+    (forall i :: 0 <= i && i < |e| ==> 0 <= e[i] && e[i] < |e|) &&

+    (forall i :: 0 <= i && i < |e| ==> d[e[i]] == i)

+  }

+

+  method Init(N: int, zero: T)

+    requires 0 <= N;

+    modifies this;

+    ensures Valid();

+    ensures |Contents| == N && this.zero == zero;

+    ensures (forall x :: x in Contents ==> x == zero);

+  {

+    var aa;

+    var ii;

+    call aa := AllocateArray(N);  this.a := aa;

+    call ii := AllocateArray(N);  this.b := ii;

+    call ii := AllocateArray(N);  this.c := ii;

+    this.n := 0;

+

+    // initialize ghost variable Contents to a sequence of length N containing only zero's,

+    // and ghost variables d and e to be the identity sequences of length N

+    ghost var s := [];

+    ghost var id := [];

+    ghost var k := 0;

+    while (k < N)

+      invariant k <= N;

+      invariant |s| == k;

+      // TODO: why doesn't this work instead of the next line?  invariant (forall x :: x in s ==> x == zero);

+      invariant (forall i :: 0 <= i && i < |s| ==> s[i] == zero);

+      invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);

+      decreases N - k;

+    {

+      s := s + [zero];

+      id := id + [k];

+      k := k + 1;

+    }

+

+    this.zero := zero;

+    this.Contents := s;

+    this.d := id;

+    this.e := id;

+  }

+  method Get(i: int) returns (x: T)

+    requires Valid();

+    requires 0 <= i && i < |Contents|;

+    ensures x == Contents[i];

+  {

+    if (0 <= b[i] && b[i] < n && c[b[i]] == i) {

+      x := a[i];

+    } else {

+      x := zero;

+    }

+  }

+  method Set(i: int, x: T)

+    requires Valid();

+    requires 0 <= i && i < |Contents|;

+    modifies this;

+    ensures Valid();

+    ensures |Contents| == |old(Contents)| && Contents == Contents[i := x];

+    ensures zero == old(zero);

+  {

+    if (0 <= b[i] && b[i] < n && c[b[i]] == i) {

+    } else {

+      assert n <= e[i];

+      b := b[i := n];

+      c := c[n := i];

+      ghost var t := d[n];

+      ghost var k := e[i];

+      d := d[n := i][k := t];

+      e := e[i := n][t := k];

+      n := n + 1;

+    }

+    a := a[i := x];

+    Contents := Contents[i := x];

+  }

+

+  /* The following method is here only to simulate support of arrays in Dafny */

+  /*private*/ static method AllocateArray<G>(n: int) returns (arr: seq<G>)

+    requires 0 <= n;

+    ensures |arr| == n;

+  {

+    arr := [];

+    var i := 0;

+    while (i < n)

+      invariant i <= n && |arr| == i;

+      decreases n - i;

+    {

+      var g: G;

+      arr := arr + [g];

+      i := i + 1;

+    }

+  }

+}

diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat
new file mode 100644
index 00000000..d6af7b71
--- /dev/null
+++ b/Test/vacid0/runtest.bat
@@ -0,0 +1,12 @@
+@echo off

+setlocal

+

+set BOOGIEDIR=..\..\Binaries

+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

+set BPLEXE=%BOOGIEDIR%\Boogie.exe

+

+for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (

+  echo.

+  echo -------------------- %%f --------------------

+  %DAFNY_EXE% /compile:0 %* %%f

+)