diff options
| author |  Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 13:51:58 -0700 |
|---|---|---|
| committer | Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 13:51:58 -0700 |
| commit | 2e43fe69d087fb75213f67f735a3e85e0278a29f (patch) | |
| tree | 95ebb6bd41c03ca000074838e6a5b262084233ca /Test/dafny1/BDD.dfy | |
| parent | 7f62d2d4c83a89479adae5d758ddf466e441953c (diff) | |
Dafny: Added maps to regression tests.
Diffstat (limited to 'Test/dafny1/BDD.dfy')
| -rw-r--r-- | Test/dafny1/BDD.dfy | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/Test/dafny1/BDD.dfy b/Test/dafny1/BDD.dfy new file mode 100644 index 00000000..3b6e478c --- /dev/null +++ b/Test/dafny1/BDD.dfy @@ -0,0 +1,60 @@ +
+
+module SimpleBDD
+{
+ class BDDNode
+ {
+ static predicate bitfunc(f: map<seq<bool>, bool>, n: nat)
+ {
+ forall i:seq<bool> :: i in f <==> |i| == n
+ }
+ ghost var Contents: map<seq<bool>, bool>;
+ ghost var Repr: set<object>;
+ ghost var n: nat;
+ var f: BDDNode, t: BDDNode;
+ var b: bool;
+ predicate valid()
+ reads this, Repr;
+ {
+ bitfunc(Contents,n) &&
+ (0 == n ==> (b <==> Contents[[]])) &&
+ (0 < n ==> this in Repr && f != null && t != null && t in Repr && f in Repr && t.Repr <= Repr && f.Repr <= Repr && this !in f.Repr && this !in t.Repr && t.valid() && f.valid() &&
+ t.n == f.n == n-1 &&
+ (forall s | s in t.Contents :: Contents[[true] + s] <==> t.Contents[s]) &&
+ (forall s | s in f.Contents :: Contents[[false] + s] <==> f.Contents[s]))
+ }
+ }
+ class BDD
+ {
+ var root: BDDNode;
+ predicate valid()
+ reads this, Repr;
+ {
+ root != null && root in Repr && root.Repr <= Repr && root.valid() &&
+ n == root.n && Contents == root.Contents
+ }
+
+ ghost var Contents: map<seq<bool>, bool>;
+ var n: nat;
+ ghost var Repr: set<object>;
+
+ method Eval(s: seq<bool>) returns(b: bool)
+ requires valid() && |s| == n;
+ ensures b == Contents[s];
+ {
+ var node: BDDNode := root;
+ var i := n;
+ assert s[n-i..] == s;
+ while(i > 0)
+ invariant node != null && node.valid();
+ invariant 0 <= i == node.n <= n;
+ invariant Contents[s] == node.Contents[s[n-i..]];
+ {
+ assert s[n-i..] == [s[n-i]] + s[n-i+1..];
+ node := if s[n-i] then node.t else node.f;
+ i := i - 1;
+ }
+ b := node.b;
+ }
+ }
+}
\ No newline at end of file |