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/Prog0.bpl | |
Initial set of files.
Diffstat (limited to 'Test/test20/Prog0.bpl')
| -rw-r--r-- | Test/test20/Prog0.bpl | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/Test/test20/Prog0.bpl b/Test/test20/Prog0.bpl new file mode 100644 index 00000000..ea71b8a8 --- /dev/null +++ b/Test/test20/Prog0.bpl @@ -0,0 +1,35 @@ +// Let's test some Boogie 2 features ...
+type real;
+type elements;
+
+type Field a;
+var heap : <a> [ref, Field a] a;
+
+const emptyset : <a> [a] bool;
+
+function union(<a> [a] bool, <a> [a] bool) returns (<a> [a] bool);
+
+axiom (forall x : <a> [a] bool, y : <a> [a] bool,
+ z : int ::
+ { union(x, y)[z] }
+ union(x, y)[z] == (x[z] || y[z]));
+
+var tau : <a> [ref] int; // error: type variable has to occur in arguments
+
+axiom (forall x : int :: !emptyset[x]);
+
+// the more general version of the axiom that also uses type quantifiers
+
+axiom (forall<alpha>
+ x : <a> [a] bool, y : <a> [a] bool,
+ z : alpha ::
+ { union(x, y)[z] }
+ union(x, y)[z] == (x[z] || y[z]));
+
+axiom (forall<beta, alpha, beta> a:alpha, b:beta :: // error: variable bound twice
+ a == b ==> (exists c:alpha :: c == b));
+
+axiom (forall<beta> a:alpha, b:beta :: // error: alpha is not declared
+ a == b ==> (exists c:alpha :: c == b));
+
+type ref;
|