diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/test20/TypeDecls1.bpl | |
Initial set of files.
Diffstat (limited to 'Test/test20/TypeDecls1.bpl')
| -rw-r--r-- | Test/test20/TypeDecls1.bpl | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/Test/test20/TypeDecls1.bpl b/Test/test20/TypeDecls1.bpl new file mode 100644 index 00000000..02c5536a --- /dev/null +++ b/Test/test20/TypeDecls1.bpl @@ -0,0 +1,23 @@ +
+// set of maps from anything to a specific type a
+const mapSet : <a>[<b>[b]a]bool;
+
+const emptySet : <a>[a]bool;
+
+axiom mapSet[5]; // type error
+
+axiom mapSet[emptySet] == true;
+
+axiom mapSet[emptySet := false] != mapSet;
+
+axiom mapSet[emptySet := 5] == mapSet; // type error
+
+axiom emptySet[13 := true][13] == true;
+
+axiom (forall f : <c>[c]int, x : ref :: mapSet[f] ==> f[x] >= 0);
+
+axiom (forall f : <c>[c]c :: mapSet[f]); // type error
+
+axiom mapSet[mapSet] == true; // type error
+
+type ref;
|