diff options
| author |  rustanleino <unknown> | 2010-06-05 02:00:33 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-05 02:00:33 +0000 |
| commit | 22e67dc18705c19b617678358c8e859349938ac3 (patch) | |
| tree | 7ee7efbcb76f209c97420dbd78b049d26c2e389c /Test/vacid0 | |
| parent | 93ac0e1e3eb6e18895087d2420b98bd8ba06443b (diff) | |
Dafny:
* Fixed bug in translation of well-formedness conditions
* Added Test/dafny0/Celebrity.dfy
* Added a harness to Test/vacid0/Composite.dfy
Diffstat (limited to 'Test/vacid0')
| -rw-r--r-- | Test/vacid0/Answer | 2 | ||||
| -rw-r--r-- | Test/vacid0/Composite.dfy | 17 |
2 files changed, 18 insertions, 1 deletions
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;
+}
+
|