diff options
| author |  chrishaw <unknown> | 2015-02-26 23:11:11 -0800 |
|---|---|---|
| committer | chrishaw <unknown> | 2015-02-26 23:11:11 -0800 |
| commit | bcb9f9e189461258d9b50aee0565afe3b8c59e5c (patch) | |
| tree | 85914af749444540ef9c6d4b9421c244c3a38116 /Test/dafny0/IMaps.dfy | |
| parent | f9d6586f72af31d7654bf4590f47ac1292348941 (diff) | |
Add imap type, which is like map but may have have infinite size
Diffstat (limited to 'Test/dafny0/IMaps.dfy')
| -rw-r--r-- | Test/dafny0/IMaps.dfy | 136 |
1 files changed, 136 insertions, 0 deletions
diff --git a/Test/dafny0/IMaps.dfy b/Test/dafny0/IMaps.dfy new file mode 100644 index 00000000..19edd4fb --- /dev/null +++ b/Test/dafny0/IMaps.dfy @@ -0,0 +1,136 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This method can be used to test compilation.
+ghost method M()
+{
+ var m := map[2:=3];
+ ghost var im := imap i | i in m :: m[i];
+ // test "in"
+ if(2 in im)
+ {
+ }
+ else
+ { assert false; }
+ // test "!in"
+ if(3 !in im)
+ {
+ }
+ else
+ { assert false; }
+ // dereference
+ if(im[2] == 3)
+ {
+ }
+ else
+ { assert false; }
+ // test applicative nature of Map<U, V> in C#
+ if(im == (imap i | i == 2 :: 3))
+ {
+ }
+ else
+ { assert false; }
+}
+
+lemma m()
+{
+ ghost var a := imap i | i == 2 :: 3; var b := imap i | i == 3 :: 2;
+ assert a[b[3]] == 3;
+}
+lemma m2(a: imap<int, bool>, b: imap<int, bool>)
+ requires forall i | 0 <= i < 100 :: i in a && i in b && a[i] != b[i];
+{
+ assert forall i | 0 <= i < 100 :: a[i] || b[i];
+}
+lemma m3(a: imap<int, int>)
+ requires forall i | 0 <= i < 100 :: i in a && a[i] == i*i;
+{
+ assert a[20] == 400;
+}
+lemma m4()
+{
+ ghost var a := imap i | i == 3 :: 9;
+ if(a[4] == 4) // UNSAFE, 4 not in the domain
+ {
+ m();
+ }
+}
+
+lemma m5(a: imap<int, int>)
+ requires 20 in a;
+{
+ assert a[20] <= 0 || 0 < a[20];
+}
+lemma m7()
+{
+ var m := map[1:=1, 2:=4, 3:=9];
+ var a := imap i | i in m :: m[i];
+ assert forall i | i in a :: a[i] == i * i;
+ assert 0 !in a;
+ assert 1 in a;
+ assert 2 in a;
+ assert 3 in a;
+ assert forall i | i < 1 || i > 3 :: i !in a;
+}
+function Update<K, V>(a:imap<K, V>, k:K, v:V):imap<K, V>
+{
+ imap j | (j == k || j in a) :: (if j == k then v else a[j])
+}
+method m8()
+{
+ ghost var a: imap<int,int> := imap i | false :: 0;
+ assert forall i :: i !in a; // check emptiness
+ var i,n := 0, 100;
+ while(i < n)
+ invariant 0 <= i <= n;
+ invariant forall i | i in a :: a[i] == i * i;
+ invariant forall k :: 0 <= k < i <==> k in a;
+ {
+ a := Update(a, i, i * i);
+ i := i + 1;
+ }
+ m3(a);
+}
+lemma m12()
+{
+ ghost var x := imap i | 0 <= i < 10 :: i * 2;
+ assert 0 in x;
+ assert 1 in x;
+ assert 10 !in x;
+ assert x[0] == 0 && x[2] == 4;
+}
+
+/*
+function domain<U, V>(m: imap<U,V>): set<U>
+ ensures forall i :: i in domain(m) <==> i in m;
+{
+ set s | s in m // UNSAFE, m may have infinite domain
+}
+*/
+
+method m13()
+{
+ var s := {0, 1, 3, 4};
+ ghost var x := imap i | i in s :: i;
+ assert forall i | i in x :: x[i] == i;
+// assert domain(x) == s;
+}
+
+class A { var x: int; }
+
+method m15(b: set<A>)
+ requires forall a | a in b :: a != null;
+{
+ ghost var m := imap a | a in b :: a.x;
+ var aa := new A;
+ assert aa !in m;
+}
+
+method minf()
+{
+ ghost var m := imap i | i > 100 :: 2 * i;
+ assert 101 in m;
+ assert 99 !in m;
+ assert m[101] == 202;
+ assert forall i :: i > 200 ==> m[i] == 2 * i;
+}
|