summaryrefslogtreecommitdiff
path: root/Test/test2/UpdateExpr.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test2/UpdateExpr.bpl')
-rw-r--r--Test/test2/UpdateExpr.bpl81
1 files changed, 81 insertions, 0 deletions
diff --git a/Test/test2/UpdateExpr.bpl b/Test/test2/UpdateExpr.bpl
new file mode 100644
index 00000000..8f950073
--- /dev/null
+++ b/Test/test2/UpdateExpr.bpl
@@ -0,0 +1,81 @@
+
+const a: [int]bool;
+
+// element 5 of a stores the value true
+axiom a == a[5 := true];
+
+procedure P()
+{
+ assert a[5];
+}
+
+procedure Q()
+{
+ assert a[4]; // error
+}
+
+procedure R()
+{
+ assert !a[5]; // error
+}
+
+procedure S(y: int, t: bool)
+ requires y <= 5;
+{
+ if (a[y := t][5] == false) {
+ assert y == 5;
+ }
+}
+
+procedure T0(aa: [int,ref]bool)
+{
+ assert aa[5,null := true] != aa[2,null := false]; // error
+}
+
+procedure T1(aa: [int,ref]bool)
+ requires aa[5,null] && !aa[2,null];
+{
+ assert aa[5,null := true] == aa[2,null := false]; // error, because we have no extensionality
+}
+
+procedure T2(aa: [int,ref]bool)
+ requires aa[5,null] && !aa[2,null];
+{
+ assert (forall x: int, y: ref :: aa[5,null := true][x,y] == aa[2,null := false][x,y]);
+}
+
+procedure U0(a: [int]int)
+{
+ var b: [int]int;
+
+ b := a[5 := 12];
+ assert a == b; // error
+}
+
+procedure U1() returns (a: [int]int)
+{
+ var b: [int]int;
+
+ b := a[5 := 12];
+ a[5] := 12;
+ assert a == b;
+}
+
+type Field a;
+const unique IntField: Field int;
+const unique RefField: Field ref;
+const unique SomeField: Field int;
+
+procedure FieldProc(H: <a>[ref,Field a]a, this: ref)
+{
+ var i: int, r: ref, y: any;
+ var K: <a>[ref,Field a]a;
+
+ K := H[this, IntField := 5][this, RefField := null][this, SomeField := 100][this, IntField := 7];
+ assert K[this, IntField] == 7;
+ assert K[this, RefField] == null;
+ assert K[this, SomeField] == 100;
+}
+
+type ref, any;
+const null : ref;