From 24ceefe6fac22e6361b1dc73b4bc878b1ba9aad5 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Tue, 8 Jun 2010 18:05:23 +0000 Subject: Boogie: * Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it). * Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it). Dafny: * Split off some tests from Test/dafny0 into Test/dafny1. * Added Test/dafny1/UltraFilter.dfy. --- Test/dafny0/Answer | 52 ----- Test/dafny0/BQueue.bpl | 430 --------------------------------------- Test/dafny0/BinaryTree.dfy | 244 ---------------------- Test/dafny0/Celebrity.dfy | 95 --------- Test/dafny0/ListContents.dfy | 93 --------- Test/dafny0/ListCopy.dfy | 55 ----- Test/dafny0/ListReverse.dfy | 27 --- Test/dafny0/Queue.dfy | 202 ------------------ Test/dafny0/SchorrWaite.dfy | 272 ------------------------- Test/dafny0/Substitution.dfy | 120 ----------- Test/dafny0/SumOfCubes.dfy | 106 ---------- Test/dafny0/TerminationDemos.dfy | 80 -------- Test/dafny0/Tree.dfy | 72 ------- Test/dafny0/UnboundedStack.dfy | 98 --------- Test/dafny0/runtest.bat | 15 +- 15 files changed, 3 insertions(+), 1958 deletions(-) delete mode 100644 Test/dafny0/BQueue.bpl delete mode 100644 Test/dafny0/BinaryTree.dfy delete mode 100644 Test/dafny0/Celebrity.dfy delete mode 100644 Test/dafny0/ListContents.dfy delete mode 100644 Test/dafny0/ListCopy.dfy delete mode 100644 Test/dafny0/ListReverse.dfy delete mode 100644 Test/dafny0/Queue.dfy delete mode 100644 Test/dafny0/SchorrWaite.dfy delete mode 100644 Test/dafny0/Substitution.dfy delete mode 100644 Test/dafny0/SumOfCubes.dfy delete mode 100644 Test/dafny0/TerminationDemos.dfy delete mode 100644 Test/dafny0/Tree.dfy delete mode 100644 Test/dafny0/UnboundedStack.dfy (limited to 'Test/dafny0') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index e1b83c87..0c152d6e 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -64,10 +64,6 @@ class C { Dafny program verifier finished with 0 verified, 0 errors --------------------- BQueue.bpl -------------------- - -Boogie program verifier finished with 8 verified, 0 errors - -------------------- TypeTests.dfy -------------------- TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D) TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C) @@ -338,30 +334,6 @@ Execution trace: Dafny program verifier finished with 2 verified, 1 error --------------------- Queue.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors - --------------------- ListCopy.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- BinaryTree.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- ListReverse.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- ListContents.dfy -------------------- - -Dafny program verifier finished with 9 verified, 0 errors - --------------------- SchorrWaite.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - -------------------- Termination.dfy -------------------- Dafny program verifier finished with 13 verified, 0 errors @@ -423,27 +395,3 @@ Dafny program verifier finished with 24 verified, 2 errors -------------------- Datatypes.dfy -------------------- Dafny program verifier finished with 10 verified, 0 errors - --------------------- UnboundedStack.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- SumOfCubes.dfy -------------------- - -Dafny program verifier finished with 17 verified, 0 errors - --------------------- TerminationDemos.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- Substitution.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- Tree.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- Celebrity.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors diff --git a/Test/dafny0/BQueue.bpl b/Test/dafny0/BQueue.bpl deleted file mode 100644 index 77f1efb3..00000000 --- a/Test/dafny0/BQueue.bpl +++ /dev/null @@ -1,430 +0,0 @@ -// BQueue.bpl -// A queue program specified in the style of dynamic frames. -// Rustan Leino, Michal Moskal, and Wolfram Schulte, 2007. - -// --------------------------------------------------------------- - -type ref; -const null: ref; - -type Field x; - -// this variable represents the heap; read its type as \forall \alpha. ref * Field \alpha --> \alpha -type HeapType = [ref, Field x]x; -var H: HeapType; - -// every object has an 'alloc' field, which says whether or not the object has been allocated -const unique alloc: Field bool; - -// for simplicity, we say that every object has one field representing its abstract value and one -// field representing its footprint (aka frame aka data group). - -const unique abstractValue: Field Seq; -const unique footprint: Field [ref]bool; - -// --------------------------------------------------------------- - -type T; // the type of the elements of the queue -const NullT: T; // some value of type T - -// --------------------------------------------------------------- - -// Queue: -const unique head: Field ref; -const unique tail: Field ref; -const unique mynodes: Field [ref]bool; -// Node: -const unique data: Field T; -const unique next: Field ref; - -function ValidQueue(HeapType, ref) returns (bool); -axiom (forall h: HeapType, q: ref :: - { ValidQueue(h, q) } - q != null && h[q,alloc] ==> - (ValidQueue(h, q) <==> - h[q,head] != null && h[h[q,head],alloc] && - h[q,tail] != null && h[h[q,tail],alloc] && - h[h[q,tail], next] == null && - // The following line can be suppressed now that we have a ValidFootprint invariant - (forall o: ref :: { h[q,footprint][o] } o != null && h[q,footprint][o] ==> h[o,alloc]) && - h[q,footprint][q] && - h[q,mynodes][h[q,head]] && h[q,mynodes][h[q,tail]] && - (forall n: ref :: { h[q,mynodes][n] } - h[q,mynodes][n] ==> - n != null && h[n,alloc] && ValidNode(h, n) && - SubSet(h[n,footprint], h[q,footprint]) && - !h[n,footprint][q] && - (h[n,next] == null ==> n == h[q,tail]) - ) && - (forall n: ref :: { h[n,next] } - h[q,mynodes][n] ==> - (h[n,next] != null ==> h[q,mynodes][h[n,next]]) - ) && - h[q,abstractValue] == h[h[q,head],abstractValue] - )); - -// frame axiom for ValidQueue -axiom (forall h0: HeapType, h1: HeapType, n: ref :: - { ValidQueue(h0,n), ValidQueue(h1,n) } - (forall o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o] - ==> h0[o,f] == h1[o,f]) - && - (forall o: ref, f: Field alpha :: o != null && h1[o,alloc] && h1[n,footprint][o] - ==> h0[o,f] == h1[o,f]) - ==> - ValidQueue(h0,n) == ValidQueue(h1,n)); - -function ValidNode(HeapType, ref) returns (bool); -axiom (forall h: HeapType, n: ref :: - { ValidNode(h, n) } - n != null && h[n,alloc] ==> - (ValidNode(h, n) <==> - // The following line can be suppressed now that we have a ValidFootprint invariant - (forall o: ref :: { h[n,footprint][o] } o != null && h[n,footprint][o] ==> h[o,alloc]) && - h[n,footprint][n] && - (h[n,next] != null ==> - h[h[n,next],alloc] && - SubSet(h[h[n,next], footprint], h[n,footprint]) && - !h[h[n,next], footprint][n]) && - (h[n,next] == null ==> EqualSeq(h[n,abstractValue], EmptySeq)) && - (h[n,next] != null ==> EqualSeq(h[n,abstractValue], - Append(Singleton(h[h[n,next],data]), h[h[n,next],abstractValue]))) - )); - -// frame axiom for ValidNode -axiom (forall h0: HeapType, h1: HeapType, n: ref :: - { ValidNode(h0,n), ValidNode(h1,n) } - (forall o: ref, f: Field alpha :: o != null && h0[o,alloc] && h0[n,footprint][o] - ==> h0[o,f] == h1[o,f]) - && - (forall o: ref, f: Field alpha :: o != null && h1[o,alloc] && h1[n,footprint][o] - ==> h0[o,f] == h1[o,f]) - ==> - ValidNode(h0,n) == ValidNode(h1,n)); - -// --------------------------------------------------------------- - -procedure MakeQueue() returns (q: ref) - requires ValidFootprints(H); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySet(old(H), H, EmptySet); - ensures q != null && H[q,alloc]; - ensures AllNewSet(old(H), H[q,footprint]); - ensures ValidQueue(H, q); - ensures Length(H[q,abstractValue]) == 0; -{ - var n: ref; - - assume Fresh(H,q); - H[q,alloc] := true; - - call n := MakeNode(NullT); - H[q,head] := n; - H[q,tail] := n; - H[q,mynodes] := SingletonSet(n); - H[q,footprint] := UnionSet(SingletonSet(q), H[n,footprint]); - H[q,abstractValue] := H[n,abstractValue]; -} - -procedure IsEmpty(q: ref) returns (isEmpty: bool) - requires ValidFootprints(H); - requires q != null && H[q,alloc] && ValidQueue(H, q); - ensures isEmpty <==> Length(H[q,abstractValue]) == 0; -{ - isEmpty := H[q,head] == H[q,tail]; -} - -procedure Enqueue(q: ref, t: T) - requires ValidFootprints(H); - requires q != null && H[q,alloc] && ValidQueue(H, q); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySet(old(H), H, old(H)[q,footprint]); - ensures DifferenceIsNew(old(H), old(H)[q,footprint], H[q,footprint]); - ensures ValidQueue(H, q); - ensures EqualSeq(H[q,abstractValue], Append(old(H)[q,abstractValue], Singleton(t))); -{ - var n: ref; - - call n := MakeNode(t); - - // foreach m in q.mynodes { m.footprint := m.footprint U n.footprint } - call BulkUpdateFootprint(H[q,mynodes], H[n,footprint]); - H[q,footprint] := UnionSet(H[q,footprint], H[n,footprint]); - - // foreach m in q.mynodes { m.abstractValue := Append(m.abstractValue, Singleton(t)) } - call BulkUpdateAbstractValue(H[q,mynodes], t); - H[q,abstractValue] := H[H[q,head],abstractValue]; - - H[q,mynodes] := UnionSet(H[q,mynodes], SingletonSet(n)); - - H[H[q,tail], next] := n; - H[q,tail] := n; -} - -procedure BulkUpdateFootprint(targetSet: [ref]bool, delta: [ref]bool); - requires ValidFootprints(H); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySetField(old(H), H, targetSet, footprint); - ensures (forall o: ref :: - o != null && old(H)[o,alloc] && targetSet[o] - ==> H[o,footprint] == UnionSet(old(H)[o,footprint], delta)); - -procedure BulkUpdateAbstractValue(targetSet: [ref]bool, t: T); - requires ValidFootprints(H); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySetField(old(H), H, targetSet, abstractValue); - ensures (forall o: ref :: - o != null && old(H)[o,alloc] && targetSet[o] - ==> EqualSeq(H[o,abstractValue], Append(old(H)[o,abstractValue], Singleton(t)))); - -procedure Front(q: ref) returns (t: T) - requires ValidFootprints(H); - requires q != null && H[q,alloc] && ValidQueue(H, q); - requires 0 < Length(H[q,abstractValue]); - ensures t == Index(H[q,abstractValue], 0); -{ - t := H[H[H[q,head], next], data]; -} - -procedure Dequeue(q: ref) - requires ValidFootprints(H); - requires q != null && H[q,alloc] && ValidQueue(H, q); - requires 0 < Length(H[q,abstractValue]); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySet(old(H), H, old(H)[q,footprint]); - ensures DifferenceIsNew(old(H), old(H)[q,footprint], H[q,footprint]); - ensures ValidQueue(H, q); - ensures EqualSeq(H[q,abstractValue], Drop(old(H)[q,abstractValue], 1)); -{ - var n: ref; - - n := H[H[q,head], next]; - H[q,head] := n; - // we could also remove old(H)[q,head] from H[q,mynodes], and similar for the footprints - H[q,abstractValue] := H[n,abstractValue]; -} - -// -------------------------------------------------------------------------------- - -procedure MakeNode(t: T) returns (n: ref) - requires ValidFootprints(H); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySet(old(H), H, EmptySet); - ensures n != null && H[n,alloc]; - ensures AllNewSet(old(H), H[n,footprint]); - ensures ValidNode(H, n); - ensures H[n,data] == t && H[n,next] == null; -{ - assume Fresh(H,n); - H[n,alloc] := true; - - H[n,next] := null; - H[n,data] := t; - H[n,footprint] := SingletonSet(n); - H[n,abstractValue] := EmptySeq; -} - -// -------------------------------------------------------------------------------- - -procedure Main(t: T, u: T, v: T) - requires ValidFootprints(H); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySet(old(H), H, EmptySet); -{ - var q0, q1: ref; - var w: T; - - call q0 := MakeQueue(); - call q1 := MakeQueue(); - - call Enqueue(q0, t); - call Enqueue(q0, u); - - call Enqueue(q1, v); - - assert Length(H[q0,abstractValue]) == 2; - - call w := Front(q0); - assert w == t; - call Dequeue(q0); - - call w := Front(q0); - assert w == u; - - assert Length(H[q0,abstractValue]) == 1; - assert Length(H[q1,abstractValue]) == 1; -} - -// -------------------------------------------------------------------------------- - -procedure Main2(t: T, u: T, v: T, q0: ref, q1: ref) - requires q0 != null && H[q0,alloc] && ValidQueue(H, q0); - requires q1 != null && H[q1,alloc] && ValidQueue(H, q1); - requires DisjointSet(H[q0,footprint], H[q1,footprint]); - requires Length(H[q0,abstractValue]) == 0; - - requires ValidFootprints(H); - modifies H; - ensures ValidFootprints(H); - ensures ModifiesOnlySet(old(H), H, UnionSet(old(H)[q0,footprint], old(H)[q1,footprint])); -{ - var w: T; - - call Enqueue(q0, t); - call Enqueue(q0, u); - - call Enqueue(q1, v); - - assert Length(H[q0,abstractValue]) == 2; - - call w := Front(q0); - assert w == t; - call Dequeue(q0); - - call w := Front(q0); - assert w == u; - - assert Length(H[q0,abstractValue]) == 1; - assert Length(H[q1,abstractValue]) == old(Length(H[q1,abstractValue])) + 1; -} - -// --------------------------------------------------------------- - -// Helpful predicates used in specs - -function ModifiesOnlySet(oldHeap: HeapType, newHeap: HeapType, set: [ref]bool) returns (bool); -axiom (forall oldHeap: HeapType, newHeap: HeapType, set: [ref]bool :: - { ModifiesOnlySet(oldHeap, newHeap, set) } - ModifiesOnlySet(oldHeap, newHeap, set) <==> - NoDeallocs(oldHeap, newHeap) && - (forall o: ref, f: Field alpha :: { newHeap[o,f] } - o != null && oldHeap[o,alloc] ==> - oldHeap[o,f] == newHeap[o,f] || set[o])); - -function ModifiesOnlySetField(oldHeap: HeapType, newHeap: HeapType, - set: [ref]bool, field: Field alpha) returns (bool); -axiom (forall oldHeap: HeapType, newHeap: HeapType, set: [ref]bool, field: Field alpha :: - { ModifiesOnlySetField(oldHeap, newHeap, set, field) } - ModifiesOnlySetField(oldHeap, newHeap, set, field) <==> - NoDeallocs(oldHeap, newHeap) && - (forall o: ref, f: Field beta :: { newHeap[o,f] } - o != null && oldHeap[o,alloc] ==> - oldHeap[o,f] == newHeap[o,f] || (set[o] && f == field))); - -function NoDeallocs(oldHeap: HeapType, newHeap: HeapType) returns (bool); -axiom (forall oldHeap: HeapType, newHeap: HeapType :: - { NoDeallocs(oldHeap, newHeap) } - NoDeallocs(oldHeap, newHeap) <==> - (forall o: ref :: { newHeap[o,alloc] } - o != null && oldHeap[o,alloc] ==> newHeap[o,alloc])); - -function AllNewSet(oldHeap: HeapType, set: [ref]bool) returns (bool); -axiom (forall oldHeap: HeapType, set: [ref]bool :: - { AllNewSet(oldHeap, set) } - AllNewSet(oldHeap, set) <==> - (forall o: ref :: { oldHeap[o,alloc] } - o != null && set[o] ==> !oldHeap[o,alloc])); - -function DifferenceIsNew(oldHeap: HeapType, oldSet: [ref]bool, newSet: [ref]bool) returns (bool); -axiom (forall oldHeap: HeapType, oldSet: [ref]bool, newSet: [ref]bool :: - { DifferenceIsNew(oldHeap, oldSet, newSet) } - DifferenceIsNew(oldHeap, oldSet, newSet) <==> - (forall o: ref :: { oldHeap[o,alloc] } - o != null && !oldSet[o] && newSet[o] ==> !oldHeap[o,alloc])); - -function ValidFootprints(h: HeapType) returns (bool); -axiom (forall h: HeapType :: - { ValidFootprints(h) } - ValidFootprints(h) <==> - (forall o: ref, r: ref :: { h[o,footprint][r] } - o != null && h[o,alloc] && r != null && h[o,footprint][r] ==> h[r,alloc])); - -function Fresh(h: HeapType, o: ref) returns (bool); -axiom (forall h: HeapType, o: ref :: - { Fresh(h,o) } - Fresh(h,o) <==> - o != null && !h[o,alloc] && h[o,footprint] == SingletonSet(o)); - -// --------------------------------------------------------------- - -const EmptySet: [ref]bool; -axiom (forall o: ref :: { EmptySet[o] } !EmptySet[o]); - -function SingletonSet(ref) returns ([ref]bool); -axiom (forall r: ref :: { SingletonSet(r) } SingletonSet(r)[r]); -axiom (forall r: ref, o: ref :: { SingletonSet(r)[o] } SingletonSet(r)[o] <==> r == o); - -function UnionSet([ref]bool, [ref]bool) returns ([ref]bool); -axiom (forall a: [ref]bool, b: [ref]bool, o: ref :: { UnionSet(a,b)[o] } - UnionSet(a,b)[o] <==> a[o] || b[o]); - -function SubSet([ref]bool, [ref]bool) returns (bool); -axiom(forall a: [ref]bool, b: [ref]bool :: { SubSet(a,b) } - SubSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} a[o] ==> b[o])); - -function EqualSet([ref]bool, [ref]bool) returns (bool); -axiom(forall a: [ref]bool, b: [ref]bool :: { EqualSet(a,b) } - EqualSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} a[o] <==> b[o])); - -function DisjointSet([ref]bool, [ref]bool) returns (bool); -axiom (forall a: [ref]bool, b: [ref]bool :: { DisjointSet(a,b) } - DisjointSet(a,b) <==> (forall o: ref :: {a[o]} {b[o]} !a[o] || !b[o])); - -// --------------------------------------------------------------- - -// Sequence of T -type Seq; - -function Length(Seq) returns (int); -axiom (forall s: Seq :: { Length(s) } 0 <= Length(s)); - -const EmptySeq: Seq; -axiom Length(EmptySeq) == 0; -axiom (forall s: Seq :: { Length(s) } Length(s) == 0 ==> s == EmptySeq); - -function Singleton(T) returns (Seq); -axiom (forall t: T :: { Length(Singleton(t)) } Length(Singleton(t)) == 1); - -function Append(Seq, Seq) returns (Seq); -axiom (forall s0: Seq, s1: Seq :: { Length(Append(s0,s1)) } - Length(Append(s0,s1)) == Length(s0) + Length(s1)); - -function Index(Seq, int) returns (T); -axiom (forall t: T :: { Index(Singleton(t), 0) } Index(Singleton(t), 0) == t); -axiom (forall s0: Seq, s1: Seq, n: int :: { Index(Append(s0,s1), n) } - (n < Length(s0) ==> Index(Append(s0,s1), n) == Index(s0, n)) && - (Length(s0) <= n ==> Index(Append(s0,s1), n) == Index(s1, n - Length(s0)))); - -function EqualSeq(Seq, Seq) returns (bool); -axiom (forall s0: Seq, s1: Seq :: { EqualSeq(s0,s1) } - EqualSeq(s0,s1) <==> - Length(s0) == Length(s1) && - (forall j: int :: { Index(s0,j) } { Index(s1,j) } - 0 <= j && j < Length(s0) ==> Index(s0,j) == Index(s1,j))); - -function Take(s: Seq, howMany: int) returns (Seq); -axiom (forall s: Seq, n: int :: { Length(Take(s,n)) } - 0 <= n ==> - (n <= Length(s) ==> Length(Take(s,n)) == n) && - (Length(s) < n ==> Length(Take(s,n)) == Length(s))); -axiom (forall s: Seq, n: int, j: int :: { Index(Take(s,n), j) } - 0 <= j && j < n && j < Length(s) ==> - Index(Take(s,n), j) == Index(s, j)); - -function Drop(s: Seq, howMany: int) returns (Seq); -axiom (forall s: Seq, n: int :: { Length(Drop(s,n)) } - 0 <= n ==> - (n <= Length(s) ==> Length(Drop(s,n)) == Length(s) - n) && - (Length(s) < n ==> Length(Drop(s,n)) == 0)); -axiom (forall s: Seq, n: int, j: int :: { Index(Drop(s,n), j) } - 0 <= n && 0 <= j && j < Length(s)-n ==> - Index(Drop(s,n), j) == Index(s, j+n)); - -// --------------------------------------------------------------- diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy deleted file mode 100644 index 8b4892dd..00000000 --- a/Test/dafny0/BinaryTree.dfy +++ /dev/null @@ -1,244 +0,0 @@ -class IntSet { - ghost var contents: set; - ghost var footprint: set; - - var root: Node; - - function Valid(): bool - reads this, footprint; - { - this in footprint && - (root == null ==> contents == {}) && - (root != null ==> - root in footprint && root.footprint <= footprint && this !in root.footprint && - root.Valid() && - contents == root.contents) - } - - method Init() - modifies this; - ensures Valid() && fresh(footprint - {this}); - ensures contents == {}; - { - root := null; - footprint := {this}; - contents := {}; - } - - method Find(x: int) returns (present: bool) - requires Valid(); - ensures present <==> x in contents; - { - if (root == null) { - present := false; - } else { - call present := root.Find(x); - } - } - - method Insert(x: int) - requires Valid(); - modifies footprint; - ensures Valid() && fresh(footprint - old(footprint)); - ensures contents == old(contents) + {x}; - { - call t := InsertHelper(x, root); - root := t; - contents := root.contents; - footprint := root.footprint + {this}; - } - - static method InsertHelper(x: int, n: Node) returns (m: Node) - requires n == null || n.Valid(); - modifies n.footprint; - ensures m != null && m.Valid(); - ensures n == null ==> fresh(m.footprint) && m.contents == {x}; - ensures n != null ==> m == n && n.contents == old(n.contents) + {x}; - ensures n != null ==> fresh(n.footprint - old(n.footprint)); - decreases if n == null then {} else n.footprint; - { - if (n == null) { - m := new Node; - call m.Init(x); - } else if (x == n.data) { - m := n; - } else { - if (x < n.data) { - assert n.right == null || n.right.Valid(); - call t := InsertHelper(x, n.left); - n.left := t; - n.footprint := n.footprint + n.left.footprint; - } else { - assert n.left == null || n.left.Valid(); - call t := InsertHelper(x, n.right); - n.right := t; - n.footprint := n.footprint + n.right.footprint; - } - n.contents := n.contents + {x}; - m := n; - } - } - - method Remove(x: int) - requires Valid(); - modifies footprint; - ensures Valid() && fresh(footprint - old(footprint)); - ensures contents == old(contents) - {x}; - { - if (root != null) { - call newRoot := root.Remove(x); - root := newRoot; - if (root == null) { - contents := {}; - footprint := {this}; - } else { - contents := root.contents; - footprint := root.footprint + {this}; - } - } - } -} - -class Node { - ghost var contents: set; - ghost var footprint: set; - - var data: int; - var left: Node; - var right: Node; - - function Valid(): bool - reads this, footprint; - { - this in footprint && - null !in footprint && - (left != null ==> - left in footprint && - left.footprint <= footprint && this !in left.footprint && - left.Valid() && - (forall y :: y in left.contents ==> y < data)) && - (right != null ==> - right in footprint && - right.footprint <= footprint && this !in right.footprint && - right.Valid() && - (forall y :: y in right.contents ==> data < y)) && - (left == null && right == null ==> - contents == {data}) && - (left != null && right == null ==> - contents == left.contents + {data}) && - (left == null && right != null ==> - contents == {data} + right.contents) && - (left != null && right != null ==> - left.footprint !! right.footprint && - contents == left.contents + {data} + right.contents) - } - - method Init(x: int) - modifies this; - ensures Valid() && fresh(footprint - {this}); - ensures contents == {x}; - { - data := x; - left := null; - right := null; - contents := {x}; - footprint := {this}; - } - - method Find(x: int) returns (present: bool) - requires Valid(); - ensures present <==> x in contents; - decreases footprint; - { - if (x == data) { - present := true; - } else if (left != null && x < data) { - call present := left.Find(x); - } else if (right != null && data < x) { - call present := right.Find(x); - } else { - present := false; - } - } - - method Remove(x: int) returns (node: Node) - requires Valid(); - modifies footprint; - ensures fresh(footprint - old(footprint)); - ensures node != null ==> node.Valid(); - ensures node == null ==> old(contents) <= {x}; - ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {x}; - decreases footprint; - { - node := this; - if (left != null && x < data) { - call t := left.Remove(x); - left := t; - contents := contents - {x}; - if (left != null) { footprint := footprint + left.footprint; } - } else if (right != null && data < x) { - call t := right.Remove(x); - right := t; - contents := contents - {x}; - if (right != null) { footprint := footprint + right.footprint; } - } else if (x == data) { - if (left == null && right == null) { - node := null; - } else if (left == null) { - node := right; - } else if (right == null) { - node := left; - } else { - // rotate - call min, r := right.RemoveMin(); - data := min; right := r; - contents := contents - {x}; - if (right != null) { footprint := footprint + right.footprint; } - } - } - } - - method RemoveMin() returns (min: int, node: Node) - requires Valid(); - modifies footprint; - ensures fresh(footprint - old(footprint)); - ensures node != null ==> node.Valid(); - ensures node == null ==> old(contents) == {min}; - ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {min}; - ensures min in old(contents) && (forall x :: x in old(contents) ==> min <= x); - decreases footprint; - { - if (left == null) { - min := data; - node := right; - } else { - call min, t := left.RemoveMin(); - left := t; - node := this; - contents := contents - {min}; - if (left != null) { footprint := footprint + left.footprint; } - } - } -} - -class Main { - method Client0(x: int) - { - var s := new IntSet; - call s.Init(); - - call s.Insert(12); - call s.Insert(24); - call present := s.Find(x); - assert present <==> x == 12 || x == 24; - } - - method Client1(s: IntSet, x: int) - requires s != null && s.Valid(); - modifies s.footprint; - { - call s.Insert(x); - call s.Insert(24); - assert old(s.contents) - {x,24} == s.contents - {x,24}; - } -} diff --git a/Test/dafny0/Celebrity.dfy b/Test/dafny0/Celebrity.dfy deleted file mode 100644 index fd267c71..00000000 --- a/Test/dafny0/Celebrity.dfy +++ /dev/null @@ -1,95 +0,0 @@ -// Celebrity example, inspired by the Rodin tutorial - -method Pick(S: set) returns (t: T); - requires S != {}; - ensures t in S; - -static function Knows(a: Person, b: Person): bool; - requires a != b; // forbid asking about the reflexive case - -static function IsCelebrity(c: Person, people: set): bool -{ - c in people && - (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p)) -} - -method FindCelebrity0(people: set, ghost c: Person) returns (r: Person) - requires (exists c :: IsCelebrity(c, people)); - ensures r == c; -{ - var cc; assume cc == c; // this line essentially converts ghost c to non-ghost cc - r := cc; -} - -method FindCelebrity1(people: set, ghost c: Person) returns (r: Person) - requires IsCelebrity(c, people); - ensures r == c; -{ - var Q := people; - call x := Pick(Q); - while (Q != {x}) - //invariant Q <= people; // inv1 in Rodin's Celebrity_1, but it's not needed here - invariant IsCelebrity(c, Q); // inv2 - invariant x in Q; - decreases Q; - { - call y := Pick(Q - {x}); - if (Knows(x, y)) { - Q := Q - {x}; // remove_1 - } else { - Q := Q - {y}; assert x in Q; // remove_2 - } - call x := Pick(Q); - } - r := x; -} - -method FindCelebrity2(people: set, ghost c: Person) returns (r: Person) - requires IsCelebrity(c, people); - ensures r == c; -{ - call b := Pick(people); - var R := people - {b}; - while (R != {}) - invariant R <= people; // inv1 - invariant b in people; // inv2 - invariant b !in R; // inv3 - invariant IsCelebrity(c, R + {b}); // my non-refinement way of saying inv4 - - decreases R; - { - call x := Pick(R); - if (Knows(x, b)) { - R := R - {x}; - } else { - b := x; - R := R - {x}; - } - } - r := b; -} - -method FindCelebrity3(n: int, people: set, ghost c: int) returns (r: int) - requires 0 < n; - requires (forall p :: p in people <==> 0 <= p && p < n); - // requires IsCelebrity(c, people); // see next line: - requires c in people && (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p)); // hack to work around bug in Dafny-to-Boogie translator - ensures r == c; -{ - r := 0; - var a := 1; - var b := 0; - while (a < n) - invariant a <= n; - invariant b < a; // Celebrity_2/inv3 and Celebrity_3/inv2 - invariant c == b || (a <= c && c < n); - { - if (Knows(a, b)) { - a := a + 1; - } else { - b := a; - a := a + 1; - } - } - r := b; -} diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy deleted file mode 100644 index 62636ce5..00000000 --- a/Test/dafny0/ListContents.dfy +++ /dev/null @@ -1,93 +0,0 @@ -class Node { - var list: seq; - var footprint: set>; - - var data: T; - var next: Node; - - function Valid(): bool - reads this, footprint; - { - this in this.footprint && null !in this.footprint && - (next == null ==> list == [data]) && - (next != null ==> - next in footprint && next.footprint <= footprint && - this !in next.footprint && - list == [data] + next.list && - next.Valid()) - } - - method Init(d: T) - modifies this; - ensures Valid() && fresh(footprint - {this}); - ensures list == [d]; - { - data := d; - next := null; - list := [d]; - footprint := {this}; - } - - method SkipHead() returns (r: Node) - requires Valid(); - ensures r == null ==> |list| == 1; - ensures r != null ==> r.Valid() && r.footprint <= footprint; - ensures r != null ==> r.list == list[1..]; - { - r := next; - } - - method Prepend(d: T) returns (r: Node) - requires Valid(); - ensures r != null && r.Valid() && fresh(r.footprint - old(footprint)); - ensures r.list == [d] + list; - { - r := new Node; - r.data := d; - r.next := this; - r.footprint := {r} + this.footprint; - r.list := [r.data] + this.list; - } - - method ReverseInPlace() returns (reverse: Node) - requires Valid(); - modifies footprint; - ensures reverse != null && reverse.Valid(); - ensures fresh(reverse.footprint - old(footprint)); - ensures |reverse.list| == |old(list)|; - ensures (forall i :: 0 <= i && i < |old(list)| ==> old(list)[i] == reverse.list[|old(list)|-1-i]); - { - var current := next; - reverse := this; - reverse.next := null; - reverse.footprint := {reverse}; - reverse.list := [data]; - - while (current != null) - invariant reverse != null && reverse.Valid(); - invariant reverse.footprint <= old(footprint); - invariant current == null ==> |old(list)| == |reverse.list|; - invariant current != null ==> - current.Valid() && - current in old(footprint) && current.footprint <= old(footprint) && - current.footprint !! reverse.footprint && - |old(list)| == |reverse.list| + |current.list| && - (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]); - invariant - (forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]); - decreases if current != null then |current.list| else -1; - { - var nx := current.next; - assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma - - // ..., reverse, current, nx, ... - assert current.data == current.list[0]; // lemma - current.next := reverse; - current.footprint := {current} + reverse.footprint; - current.list := [current.data] + reverse.list; - - reverse := current; - current := nx; - } - } -} diff --git a/Test/dafny0/ListCopy.dfy b/Test/dafny0/ListCopy.dfy deleted file mode 100644 index 52f5cf76..00000000 --- a/Test/dafny0/ListCopy.dfy +++ /dev/null @@ -1,55 +0,0 @@ -class Node { - var nxt: Node; - - method Init() - modifies this; - ensures nxt == null; - { - nxt := null; - } - - method Copy(root: Node) returns (result: Node) - { - var existingRegion: set; - assume root == null || root in existingRegion; - assume (forall o: Node :: o != null && o in existingRegion && o.nxt != null ==> o.nxt in existingRegion); - - var newRoot := null; - var oldListPtr := root; - var newRegion: set := {}; - - if (oldListPtr != null) { - newRoot := new Node; - call newRoot.Init(); - newRegion := newRegion + {newRoot}; - var prev := newRoot; - - while (oldListPtr != null) - invariant newRoot in newRegion; - invariant (forall o: Node :: o in newRegion ==> o != null); - invariant (forall o: Node :: o in newRegion && o.nxt != null ==> o.nxt in newRegion); - invariant prev in newRegion; - invariant fresh(newRegion); - invariant newRegion !! existingRegion; - decreases *; // omit loop termination check - { - var tmp := new Node; - call tmp.Init(); - - newRegion := newRegion + {tmp}; - prev.nxt := tmp; - - prev := tmp; - oldListPtr := oldListPtr.nxt; - } - } - result := newRoot; - assert result == null || result in newRegion; - - // everything in newRegion is fresh - assert fresh(newRegion); - - // newRegion # exisitingRegion - assert newRegion !! existingRegion; - } -} diff --git a/Test/dafny0/ListReverse.dfy b/Test/dafny0/ListReverse.dfy deleted file mode 100644 index ef029b88..00000000 --- a/Test/dafny0/ListReverse.dfy +++ /dev/null @@ -1,27 +0,0 @@ - -class Node { - var nxt: Node; - - method ReverseInPlace(x: Node, r: set) returns (reverse: Node) - requires null !in r; - requires x == null || x in r; - requires (forall y :: y in r ==> y.nxt == null || y.nxt in r); // region closure - modifies r; - ensures reverse == null || reverse in r; - ensures (forall y :: y in r ==> y.nxt == null || y.nxt in r); // region closure - { - var current := x; - reverse := null; - while (current != null) - invariant current == null || current in r; - invariant reverse == null || reverse in r; - invariant (forall y :: y in r ==> y.nxt == null || y.nxt in r); // region closure - decreases *; // omit loop termination check - { - var tmp := current.nxt; - current.nxt := reverse; - reverse := current; - current := tmp; - } - } -} diff --git a/Test/dafny0/Queue.dfy b/Test/dafny0/Queue.dfy deleted file mode 100644 index 42b7dd64..00000000 --- a/Test/dafny0/Queue.dfy +++ /dev/null @@ -1,202 +0,0 @@ -// Queue.dfy -// Dafny version of Queue.bpl -// Rustan Leino, 2008 - -class Queue { - var head: Node; - var tail: Node; - - ghost var contents: seq; - ghost var footprint: set; - ghost var spine: set>; - - function Valid(): bool - reads this, footprint; - { - this in footprint && spine <= footprint && - head != null && head in spine && - tail != null && tail in spine && - tail.next == null && - (forall n :: - n in spine ==> - n != null && n.footprint <= footprint && this !in n.footprint && - n.Valid() && - (n.next == null ==> n == tail)) && - (forall n :: - n in spine ==> - n.next != null ==> n.next in spine) && - contents == head.tailContents - } - - method Init() - modifies this; - ensures Valid() && fresh(footprint - {this}); - ensures |contents| == 0; - { - var n := new Node; - call n.Init(); - head := n; - tail := n; - contents := n.tailContents; - footprint := {this} + n.footprint; - spine := {n}; - } - - method Rotate() - requires Valid(); - requires 0 < |contents|; - modifies footprint; - ensures Valid() && fresh(footprint - old(footprint)); - ensures contents == old(contents)[1..] + old(contents)[..1]; - { - call t := Front(); - call Dequeue(); - call Enqueue(t); - } - - method RotateAny() - requires Valid(); - requires 0 < |contents|; - modifies footprint; - ensures Valid() && fresh(footprint - old(footprint)); - ensures |contents| == |old(contents)|; - ensures (exists i :: 0 <= i && i <= |contents| && - contents == old(contents)[i..] + old(contents)[..i]); - { - call t := Front(); - call Dequeue(); - call Enqueue(t); - } - - method IsEmpty() returns (isEmpty: bool) - requires Valid(); - ensures isEmpty <==> |contents| == 0; - { - isEmpty := head == tail; - } - - method Enqueue(t: T) - requires Valid(); - modifies footprint; - ensures Valid() && fresh(footprint - old(footprint)); - ensures contents == old(contents) + [t]; - { - var n := new Node; - call n.Init(); n.data := t; - tail.next := n; - tail := n; - - foreach (m in spine) { - m.tailContents := m.tailContents + [t]; - } - contents := head.tailContents; - - foreach (m in spine) { - m.footprint := m.footprint + n.footprint; - } - footprint := footprint + n.footprint; - - spine := spine + {n}; - } - - method Front() returns (t: T) - requires Valid(); - requires 0 < |contents|; - ensures t == contents[0]; - { - t := head.next.data; - } - - method Dequeue() - requires Valid(); - requires 0 < |contents|; - modifies footprint; - ensures Valid() && fresh(footprint - old(footprint)); - ensures contents == old(contents)[1..]; - { - var n := head.next; - head := n; - contents := n.tailContents; - } -} - -class Node { - var data: T; - var next: Node; - - ghost var tailContents: seq; - ghost var footprint: set; - - function Valid(): bool - reads this, footprint; - { - this in footprint && - (next != null ==> next in footprint && next.footprint <= footprint) && - (next == null ==> tailContents == []) && - (next != null ==> tailContents == [next.data] + next.tailContents) - } - - method Init() - modifies this; - ensures Valid() && fresh(footprint - {this}); - ensures next == null; - { - next := null; - tailContents := []; - footprint := {this}; - } -} - -class Main { - method A(t: T, u: T, v: T) - { - var q0 := new Queue; - call q0.Init(); - var q1 := new Queue; - call q1.Init(); - - call q0.Enqueue(t); - call q0.Enqueue(u); - - call q1.Enqueue(v); - - assert |q0.contents| == 2; - - call w := q0.Front(); - assert w == t; - call q0.Dequeue(); - - call w := q0.Front(); - assert w == u; - - assert |q0.contents| == 1; - assert |q1.contents| == 1; - } - - method Main2(t: U, u: U, v: U, q0: Queue, q1: Queue) - requires q0 != null && q0.Valid(); - requires q1 != null && q1.Valid(); - requires q0.footprint !! q1.footprint; - requires |q0.contents| == 0; - modifies q0.footprint, q1.footprint; - ensures fresh(q0.footprint - old(q0.footprint)); - ensures fresh(q1.footprint - old(q1.footprint)); - { - call q0.Enqueue(t); - call q0.Enqueue(u); - - call q1.Enqueue(v); - - assert |q0.contents| == 2; - - call w := q0.Front(); - assert w == t; - call q0.Dequeue(); - - call w := q0.Front(); - assert w == u; - - assert |q0.contents| == 1; - assert |q1.contents| == old(|q1.contents|) + 1; - } -} diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy deleted file mode 100644 index a46e83a3..00000000 --- a/Test/dafny0/SchorrWaite.dfy +++ /dev/null @@ -1,272 +0,0 @@ -// Rustan Leino -// 7 November 2008 -// Schorr-Waite and other marking algorithms, written and verified in Dafny. -// Copyright (c) 2008, Microsoft. - -class Node { - var children: seq; - var marked: bool; - var childrenVisited: int; - ghost var pathFromRoot: Path; -} - -class Main { - method RecursiveMark(root: Node, ghost S: set) - requires root in S; - // S is closed under 'children': - requires (forall n :: n in S ==> n != null && - (forall ch :: ch in n.children ==> ch == null || ch in S)); - requires (forall n :: n in S ==> ! n.marked && n.childrenVisited == 0); - modifies S; - ensures root.marked; - // nodes reachable from 'root' are marked: - ensures (forall n :: n in S && n.marked ==> - (forall ch :: ch in n.children && ch != null ==> ch.marked)); - ensures (forall n :: n in S ==> - n.childrenVisited == old(n.childrenVisited) && - n.children == old(n.children)); - { - call RecursiveMarkWorker(root, S, {}); - } - - method RecursiveMarkWorker(root: Node, ghost S: set, ghost stackNodes: set) - requires root != null && root in S; - requires (forall n :: n in S ==> n != null && - (forall ch :: ch in n.children ==> ch == null || ch in S)); - requires (forall n :: n in S && n.marked ==> - n in stackNodes || - (forall ch :: ch in n.children && ch != null ==> ch.marked)); - requires (forall n :: n in stackNodes ==> n != null && n.marked); - modifies S; - ensures root.marked; - // nodes reachable from 'root' are marked: - ensures (forall n :: n in S && n.marked ==> - n in stackNodes || - (forall ch :: ch in n.children && ch != null ==> ch.marked)); - ensures (forall n: Node :: n in S && old(n.marked) ==> n.marked); - ensures (forall n :: n in S ==> - n.childrenVisited == old(n.childrenVisited) && - n.children == old(n.children)); - decreases S - stackNodes; - { - if (! root.marked) { - root.marked := true; - var i := 0; - while (i < |root.children|) - invariant root.marked && i <= |root.children|; - invariant (forall n :: n in S && n.marked ==> - n == root || - n in stackNodes || - (forall ch :: ch in n.children && ch != null ==> ch.marked)); - invariant (forall j :: 0 <= j && j < i ==> - root.children[j] == null || root.children[j].marked); - invariant (forall n: Node :: n in S && old(n.marked) ==> n.marked); - invariant (forall n :: n in S ==> - n.childrenVisited == old(n.childrenVisited) && - n.children == old(n.children)); - decreases |root.children| - i; - { - var c := root.children[i]; - if (c != null) { - ghost var D := S - stackNodes; assert root in D; - call RecursiveMarkWorker(c, S, stackNodes + {root}); - } - i := i + 1; - } - } - } - - // --------------------------------------------------------------------------------- - - method IterativeMark(root: Node, ghost S: set) - requires root in S; - // S is closed under 'children': - requires (forall n :: n in S ==> n != null && - (forall ch :: ch in n.children ==> ch == null || ch in S)); - requires (forall n :: n in S ==> ! n.marked && n.childrenVisited == 0); - modifies S; - ensures root.marked; - // nodes reachable from 'root' are marked: - ensures (forall n :: n in S && n.marked ==> - (forall ch :: ch in n.children && ch != null ==> ch.marked)); - ensures (forall n :: n in S ==> - n.childrenVisited == old(n.childrenVisited) && - n.children == old(n.children)); - { - var t := root; - t.marked := true; - var stackNodes := []; - ghost var unmarkedNodes := S - {t}; - while (true) - invariant root.marked && t in S && t !in stackNodes; - // stackNodes has no duplicates: - invariant (forall i, j :: 0 <= i && i < j && j < |stackNodes| ==> - stackNodes[i] != stackNodes[j]); - invariant (forall n :: n in stackNodes ==> n in S); - invariant (forall n :: n in stackNodes || n == t ==> - n.marked && - 0 <= n.childrenVisited && n.childrenVisited <= |n.children| && - (forall j :: 0 <= j && j < n.childrenVisited ==> - n.children[j] == null || n.children[j].marked)); - invariant (forall n :: n in stackNodes ==> n.childrenVisited < |n.children|); - // nodes on the stack are linked: - invariant (forall j :: 0 <= j && j+1 < |stackNodes| ==> - stackNodes[j].children[stackNodes[j].childrenVisited] == stackNodes[j+1]); - invariant 0 < |stackNodes| ==> - stackNodes[|stackNodes|-1].children[stackNodes[|stackNodes|-1].childrenVisited] == t; - invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==> - (forall ch :: ch in n.children && ch != null ==> ch.marked)); - invariant (forall n :: n in S && n !in stackNodes && n != t ==> - n.childrenVisited == old(n.childrenVisited)); - invariant (forall n: Node :: n in S ==> n.children == old(n.children)); - invariant (forall n :: n in S && !n.marked ==> n in unmarkedNodes); - decreases unmarkedNodes, stackNodes, |t.children| - t.childrenVisited; - { - if (t.childrenVisited == |t.children|) { - // pop - t.childrenVisited := 0; - if (|stackNodes| == 0) { - return; - } - t := stackNodes[|stackNodes| - 1]; - stackNodes := stackNodes[..|stackNodes| - 1]; - t.childrenVisited := t.childrenVisited + 1; - } else if (t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked) { - // just advance to next child - t.childrenVisited := t.childrenVisited + 1; - } else { - // push - stackNodes := stackNodes + [t]; - t := t.children[t.childrenVisited]; - t.marked := true; - unmarkedNodes := unmarkedNodes - {t}; - } - } - } - - // --------------------------------------------------------------------------------- - - function Reachable(from: Node, to: Node, S: set): bool - requires null !in S; - reads S; - { - (exists via: Path :: ReachableVia(from, via, to, S)) - } - - function ReachableVia(from: Node, via: Path, to: Node, S: set): bool - requires null !in S; - reads S; - decreases via; - { - match via - case Empty => from == to - case Extend(prefix, n) => n in S && to in n.children && ReachableVia(from, prefix, n, S) - } - - method SchorrWaite(root: Node, ghost S: set) - requires root in S; - // S is closed under 'children': - requires (forall n :: n in S ==> n != null && - (forall ch :: ch in n.children ==> ch == null || ch in S)); - // the graph starts off with nothing marked and nothing being indicated as currently being visited: - requires (forall n :: n in S ==> ! n.marked && n.childrenVisited == 0); - modifies S; - // nodes reachable from 'root' are marked: - ensures root.marked; - ensures (forall n :: n in S && n.marked ==> - (forall ch :: ch in n.children && ch != null ==> ch.marked)); - // every marked node was reachable from 'root' in the pre-state: - ensures (forall n :: n in S && n.marked ==> old(Reachable(root, n, S))); - // the structure of the graph has not changed: - ensures (forall n :: n in S ==> - n.childrenVisited == old(n.childrenVisited) && - n.children == old(n.children)); - { - var t := root; - var p: Node := null; // parent of t in original graph - ghost var path := #Path.Empty; - t.marked := true; - t.pathFromRoot := path; - ghost var stackNodes := []; - ghost var unmarkedNodes := S - {t}; - while (true) - invariant root.marked && t != null && t in S && t !in stackNodes; - invariant |stackNodes| == 0 <==> p == null; - invariant 0 < |stackNodes| ==> p == stackNodes[|stackNodes|-1]; - // stackNodes has no duplicates: - invariant (forall i, j :: 0 <= i && i < j && j < |stackNodes| ==> - stackNodes[i] != stackNodes[j]); - invariant (forall n :: n in stackNodes ==> n in S); - invariant (forall n :: n in stackNodes || n == t ==> - n.marked && - 0 <= n.childrenVisited && n.childrenVisited <= |n.children| && - (forall j :: 0 <= j && j < n.childrenVisited ==> - n.children[j] == null || n.children[j].marked)); - invariant (forall n :: n in stackNodes ==> n.childrenVisited < |n.children|); - invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==> - (forall ch :: ch in n.children && ch != null ==> ch.marked)); - invariant (forall n :: n in S && n !in stackNodes && n != t ==> - n.childrenVisited == old(n.childrenVisited)); - invariant (forall n :: n in S ==> n in stackNodes || n.children == old(n.children)); - invariant (forall n :: n in stackNodes ==> - |n.children| == old(|n.children|) && - (forall j :: 0 <= j && j < |n.children| ==> - j == n.childrenVisited || n.children[j] == old(n.children[j]))); - // every marked node is reachable: - invariant old(ReachableVia(root, path, t, S)); - invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==> - old(ReachableVia(root, pth, n, S))); - invariant (forall n :: n in S && n.marked ==> old(Reachable(root, n, S))); - // the current values of m.children[m.childrenVisited] for m's on the stack: - invariant 0 < |stackNodes| ==> stackNodes[0].children[stackNodes[0].childrenVisited] == null; - invariant (forall k :: 0 < k && k < |stackNodes| ==> - stackNodes[k].children[stackNodes[k].childrenVisited] == stackNodes[k-1]); - // the original values of m.children[m.childrenVisited] for m's on the stack: - invariant (forall k :: 0 <= k && k+1 < |stackNodes| ==> - old(stackNodes[k].children)[stackNodes[k].childrenVisited] == stackNodes[k+1]); - invariant 0 < |stackNodes| ==> - old(stackNodes[|stackNodes|-1].children)[stackNodes[|stackNodes|-1].childrenVisited] == t; - invariant (forall n :: n in S && !n.marked ==> n in unmarkedNodes); - decreases unmarkedNodes, stackNodes, |t.children| - t.childrenVisited; - { - if (t.childrenVisited == |t.children|) { - // pop - t.childrenVisited := 0; - if (p == null) { - return; - } - var oldP := p.children[p.childrenVisited]; - // p.children[p.childrenVisited] := t; - p.children := p.children[..p.childrenVisited] + [t] + p.children[p.childrenVisited + 1..]; - t := p; - p := oldP; - stackNodes := stackNodes[..|stackNodes| - 1]; - t.childrenVisited := t.childrenVisited + 1; - path := t.pathFromRoot; - - } else if (t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked) { - // just advance to next child - t.childrenVisited := t.childrenVisited + 1; - - } else { - // push - - var newT := t.children[t.childrenVisited]; - // t.children[t.childrenVisited] := p; - t.children := t.children[..t.childrenVisited] + [p] + t.children[t.childrenVisited + 1..]; - p := t; - stackNodes := stackNodes + [t]; - path := #Path.Extend(path, t); - t := newT; - t.marked := true; - t.pathFromRoot := path; - unmarkedNodes := unmarkedNodes - {t}; - } - } - } -} - -datatype Path { - Empty; - Extend(Path, Node); -} diff --git a/Test/dafny0/Substitution.dfy b/Test/dafny0/Substitution.dfy deleted file mode 100644 index 72415fea..00000000 --- a/Test/dafny0/Substitution.dfy +++ /dev/null @@ -1,120 +0,0 @@ -datatype List { - Nil; - Cons(Expr, List); -} - -datatype Expr { - Const(int); - Var(int); - Nary(int, List); -} - -static function Subst(e: Expr, v: int, val: int): Expr - decreases e; -{ - match e - case Const(c) => e - case Var(x) => if x == v then #Expr.Const(val) else e - case Nary(op, args) => #Expr.Nary(op, SubstList(args, v, val)) -} - -static function SubstList(l: List, v: int, val: int): List - decreases l; -{ - match l - case Nil => l - case Cons(e, tail) => #List.Cons(Subst(e, v, val), SubstList(tail, v, val)) -} - -static ghost method Theorem(e: Expr, v: int, val: int) - ensures Subst(Subst(e, v, val), v, val) == Subst(e, v, val); - decreases e; -{ - match e { - case Const(c) => - case Var(x) => - case Nary(op, args) => - call Lemma(args, v, val); - } -} - -static ghost method Lemma(l: List, v: int, val: int) - ensures SubstList(SubstList(l, v, val), v, val) == SubstList(l, v, val); - decreases l; -{ - match l { - case Nil => - case Cons(e, tail) => - call Theorem(e, v, val); - call Lemma(tail, v, val); - } -} - -// ------------------------------- - -datatype Expression { - Const(int); - Var(int); - Nary(int, seq); -} - -static function Substitute(e: Expression, v: int, val: int): Expression - decreases e, true; -{ - match e - case Const(c) => e - case Var(x) => if x == v then #Expression.Const(val) else e - case Nary(op, args) => #Expression.Nary(op, SubstSeq(e, args, v, val)) -} - -static function SubstSeq(/*ghost*/ parent: Expression, - q: seq, v: int, val: int): seq - requires (forall a :: a in q ==> a < parent); - decreases parent, false, q; -{ - if q == [] then [] else - SubstSeq(parent, q[..|q|-1], v, val) + [Substitute(q[|q|-1], v, val)] -} - -static ghost method TheoremSeq(e: Expression, v: int, val: int) - ensures Substitute(Substitute(e, v, val), v, val) == Substitute(e, v, val); - decreases e, true; -{ - match e { - case Const(c) => - case Var(x) => - case Nary(op, args) => - ghost var seArgs := SubstSeq(e, args, v, val); - call LemmaSeq(e, args, v, val); - - ghost var se := Substitute(e, v, val); - ghost var seArgs2 := SubstSeq(se, seArgs, v, val); - call LemmaSeq(se, seArgs, v, val); - - var N := |args|; - var j := 0; - while (j < N) - invariant j <= N; - invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]); - decreases N - j; - { - call TheoremSeq(args[j], v, val); - j := j + 1; - } - assert seArgs == seArgs2; - } -} - -static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq, - v: int, val: int) - requires (forall a :: a in q ==> a < parent); - ensures |SubstSeq(parent, q, v, val)| == |q|; - ensures (forall k :: 0 <= k && k < |q| ==> - SubstSeq(parent, q, v, val)[k] == Substitute(q[k], v, val)); - decreases q; -{ - if (q == []) { - } else { - call LemmaSeq(parent, q[..|q|-1], v, val); - } -} diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy deleted file mode 100644 index b4fab490..00000000 --- a/Test/dafny0/SumOfCubes.dfy +++ /dev/null @@ -1,106 +0,0 @@ -class SumOfCubes { - static function SumEmUp(n: int, m: int): int - requires 0 <= n && n <= m; - decreases m - n; - { - if m == n then 0 else n*n*n + SumEmUp(n+1, m) - } - - static method Socu(n: int, m: int) returns (r: int) - requires 0 <= n && n <= m; - ensures r == SumEmUp(n, m); - { - call a := SocuFromZero(m); - call b := SocuFromZero(n); - r := a - b; - call Lemma0(n, m); - } - - static method SocuFromZero(k: int) returns (r: int) - requires 0 <= k; - ensures r == SumEmUp(0, k); - { - call g := Gauss(k); - r := g * g; - call Lemma1(k); - } - - ghost static method Lemma0(n: int, m: int) - requires 0 <= n && n <= m; - ensures SumEmUp(n, m) == SumEmUp(0, m) - SumEmUp(0, n); - { - var k := n; - while (k < m) - invariant n <= k && k <= m; - invariant SumEmDown(0, n) + SumEmDown(n, k) == SumEmDown(0, k); - { - k := k + 1; - } - call Lemma3(0, n); - call Lemma3(n, k); - call Lemma3(0, k); - } - - static function GSum(k: int): int - requires 0 <= k; - decreases k; - { - if k == 0 then 0 else GSum(k-1) + k-1 - } - - static method Gauss(k: int) returns (r: int) - requires 0 <= k; - ensures r == GSum(k); - { - r := k * (k - 1) / 2; - call Lemma2(k); - } - - ghost static method Lemma1(k: int) - requires 0 <= k; - ensures SumEmUp(0, k) == GSum(k) * GSum(k); - { - var i := 0; - while (i < k) - invariant i <= k; - invariant SumEmDown(0, i) == GSum(i) * GSum(i); - { - call Lemma2(i); - i := i + 1; - } - call Lemma3(0, k); - } - - ghost static method Lemma2(k: int) - requires 0 <= k; - ensures 2 * GSum(k) == k * (k - 1); - { - var i := 0; - while (i < k) - invariant i <= k; - invariant 2 * GSum(i) == i * (i - 1); - { - i := i + 1; - } - } - - static function SumEmDown(n: int, m: int): int - requires 0 <= n && n <= m; - decreases m; - { - if m == n then 0 else SumEmDown(n, m-1) + (m-1)*(m-1)*(m-1) - } - - ghost static method Lemma3(n: int, m: int) - requires 0 <= n && n <= m; - ensures SumEmUp(n, m) == SumEmDown(n, m); - { - var k := n; - while (k < m) - invariant n <= k && k <= m; - invariant SumEmUp(n, m) == SumEmDown(n, k) + SumEmUp(k, m); - { - k := k + 1; - } - } -} diff --git a/Test/dafny0/TerminationDemos.dfy b/Test/dafny0/TerminationDemos.dfy deleted file mode 100644 index 6b63bfec..00000000 --- a/Test/dafny0/TerminationDemos.dfy +++ /dev/null @@ -1,80 +0,0 @@ -class Example { - method M(n: int) - { - var i := 0; - while (i < n) - decreases n - i; - { - i := i + 1; - } - } -} - -// ----------------------------------- - -class Fibonacci { - function Fib(n: int): int - decreases n; - { - if n < 2 then n else Fib(n-2) + Fib(n-1) - } -} - -// ----------------------------------- - -class Ackermann { - function F(m: int, n: int): int - decreases m, n; - { - if m <= 0 then - n + 1 - else if n <= 0 then - F(m - 1, 1) - else - F(m - 1, F(m, n - 1)) - } -} - -// ----------------------------------- - -class List { - var data: int; - var next: List; - ghost var ListNodes: set; - function IsAcyclic(): bool - reads *; - decreases ListNodes; - { - this in ListNodes && - (next != null ==> - next.ListNodes <= ListNodes && this !in next.ListNodes && - next.IsAcyclic()) - } - - method Singleton(x: int) returns (list: List) - ensures list != null && list.IsAcyclic(); - { - list := new List; - list.data := x; - list.next := null; - list.ListNodes := {list}; - } - - method Prepend(x: int, tail: List) returns (list: List) - requires tail == null || tail.IsAcyclic(); - ensures list != null && list.IsAcyclic(); - { - list := new List; - list.data := x; - list.next := tail; - list.ListNodes := if tail == null then {list} else {list} + tail.ListNodes; - } - - function Sum(): int - requires IsAcyclic(); - reads *; - decreases ListNodes; - { - if next == null then data else data + next.Sum() - } -} diff --git a/Test/dafny0/Tree.dfy b/Test/dafny0/Tree.dfy deleted file mode 100644 index 58124171..00000000 --- a/Test/dafny0/Tree.dfy +++ /dev/null @@ -1,72 +0,0 @@ -// ------------------ generic list, non-generic tree - -datatype List { - Nil; - Cons(T, List); -} - -datatype Tree { - Node(int, List); -} - -static function Inc(t: Tree): Tree - decreases t; -{ - match t - case Node(n, children) => #Tree.Node(n+1, ForestInc(children)) -} - -static function ForestInc(forest: List): List - decreases forest; -{ - match forest - case Nil => forest - case Cons(tree, tail) => #List.Cons(Inc(tree), ForestInc(tail)) -} - -// ------------------ generic list, generic tree (but GInc defined only for GTree - -datatype GTree { - Node(T, List>); -} - -static function GInc(t: GTree): GTree - decreases t; -{ - match t - case Node(n, children) => #GTree.Node(n+1, GForestInc(children)) -} - -static function GForestInc(forest: List>): List> - decreases forest; -{ - match forest - case Nil => forest - case Cons(tree, tail) => #List.Cons(GInc(tree), GForestInc(tail)) -} - -// ------------------ non-generic structures - -datatype TreeList { - Nil; - Cons(OneTree, TreeList); -} - -datatype OneTree { - Node(int, TreeList); -} - -static function XInc(t: OneTree): OneTree - decreases t; -{ - match t - case Node(n, children) => #OneTree.Node(n+1, XForestInc(children)) -} - -static function XForestInc(forest: TreeList): TreeList - decreases forest; -{ - match forest - case Nil => forest - case Cons(tree, tail) => #TreeList.Cons(XInc(tree), XForestInc(tail)) -} diff --git a/Test/dafny0/UnboundedStack.dfy b/Test/dafny0/UnboundedStack.dfy deleted file mode 100644 index 4c3b095a..00000000 --- a/Test/dafny0/UnboundedStack.dfy +++ /dev/null @@ -1,98 +0,0 @@ -class UnboundedStack { - ghost var representation: set; - ghost var content: seq; - var top: Node; - - function IsUnboundedStack(): bool - reads this, representation; - { - this in representation && - (top == null ==> - content == []) && - (top != null ==> - top in representation && this !in top.footprint && top.footprint <= representation && - content == top.content && - top.Valid()) - } - - method InitUnboundedStack() - modifies this; - ensures IsUnboundedStack(); - ensures content == []; - { - this.top := null; - this.content := []; - this.representation := {this}; - } - - method Push(val: T) - requires IsUnboundedStack(); - modifies this; - ensures IsUnboundedStack(); - ensures content == [val] + old(content); - { - var tmp := new Node; - call tmp.InitNode(val,top); - top := tmp; - representation := representation + top.footprint; - content := [val] + content; - } - - method Pop() returns (result: T) - requires IsUnboundedStack(); - requires content != []; - modifies this; - ensures IsUnboundedStack(); - ensures content == old(content)[1..]; - { - result := top.val; - top := top.next; - content := content[1..]; - } - - method isEmpty() returns (result: bool) - requires IsUnboundedStack(); - ensures result <==> content == []; - { - result := top == null; - } -} - -class Node { - ghost var footprint: set; - ghost var content: seq; - var val: T; - var next: Node; - - function Valid(): bool - reads this, footprint; - { - this in footprint && - (next == null ==> - content == [val]) && - (next != null ==> - next in footprint && next.footprint <= footprint && this !in next.footprint && - content == [val] + next.content && - next.Valid()) - } - - method InitNode(val: T, next: Node) - requires next != null ==> next.Valid() && !(this in next.footprint); - modifies this; - ensures Valid(); - ensures next != null ==> content == [val] + next.content && - footprint == {this} + next.footprint; - ensures next == null ==> content == [val] && - footprint == {this}; - { - this.val := val; - this.next := next; - if (next == null) { - this.footprint := {this}; - this.content := [val]; - } else { - this.footprint := {this} + next.footprint; - this.content := [val] + next.content; - } - } -} diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index eb7ea4f7..aa45ca05 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -11,19 +11,10 @@ for %%f in (Simple.dfy) do ( %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f ) -for %%f in (BQueue.bpl) do ( - echo. - echo -------------------- %%f -------------------- - %BPLEXE% %* %%f -) - for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy - Modules0.dfy Modules1.dfy BadFunction.dfy Queue.dfy ListCopy.dfy - BinaryTree.dfy ListReverse.dfy ListContents.dfy - SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy - TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy - SumOfCubes.dfy TerminationDemos.dfy Substitution.dfy - Tree.dfy Celebrity.dfy) do ( + Modules0.dfy Modules1.dfy BadFunction.dfy + Termination.dfy Use.dfy DTypes.dfy + TypeParameters.dfy Datatypes.dfy) do ( echo. echo -------------------- %%f -------------------- %DAFNY_EXE% /compile:0 %* %%f -- cgit v1.2.3