From 22e67dc18705c19b617678358c8e859349938ac3 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 5 Jun 2010 02:00:33 +0000
Subject: Dafny: * Fixed bug in translation of well-formedness conditions *
 Added Test/dafny0/Celebrity.dfy * Added a harness to
 Test/vacid0/Composite.dfy

---
 Test/vacid0/Answer        |  2 +-
 Test/vacid0/Composite.dfy | 17 +++++++++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)

(limited to 'Test/vacid0')

diff --git a/Test/vacid0/Answer b/Test/vacid0/Answer
index 6f270f92..90bbcc78 100644
--- a/Test/vacid0/Answer
+++ b/Test/vacid0/Answer
@@ -9,4 +9,4 @@ Dafny program verifier finished with 9 verified, 0 errors
 
 -------------------- Composite.dfy --------------------
 
-Dafny program verifier finished with 14 verified, 0 errors
+Dafny program verifier finished with 16 verified, 0 errors
diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy
index 28074c7b..ca5f206b 100644
--- a/Test/vacid0/Composite.dfy
+++ b/Test/vacid0/Composite.dfy
@@ -83,6 +83,7 @@ class Composite {
     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 parent == null;
     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});
@@ -158,3 +159,19 @@ method Main()
   call c2.Update(496, S);
   call c0.Update(0, S);
 }
+
+method Harness() {
+  var a := new Composite;  call a.Init(5);
+  var b := new Composite;  call b.Init(7);
+  call a.Add({a}, b, {b});
+  assert a.sum == 12;
+
+  call b.Update(17, {a,b});
+  assert a.sum == 22;
+
+  var c := new Composite;  call c.Init(10);
+  call b.Add({a,b}, c, {c});
+  call b.Dislodge({a,b,c});
+  assert b.sum == 27;
+}
+
-- 
cgit v1.2.3