summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Test/hofs/VectorUpdate.dfy60
-rw-r--r--Test/hofs/VectorUpdate.dfy.expect10
2 files changed, 70 insertions, 0 deletions
diff --git a/Test/hofs/VectorUpdate.dfy b/Test/hofs/VectorUpdate.dfy
new file mode 100644
index 00000000..96edbe77
--- /dev/null
+++ b/Test/hofs/VectorUpdate.dfy
@@ -0,0 +1,60 @@
+// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method VectorUpdate(N: int, a : array<A>, f : (int,A) -> A)
+ requires a != null;
+ requires N == a.Length;
+ requires forall j :: 0 <= j < N ==> f.requires(j,a[j]);
+ requires forall j :: 0 <= j < N ==> a !in f.reads(j,a[j]);
+ modifies a;
+ ensures forall j :: 0 <= j < N ==> a[j] == f(j,old(a[j]));
+{
+ var i := 0;
+ while (i < N)
+ invariant 0 <= i <= N;
+ invariant forall j :: i <= j < N ==> f.requires(j,a[j]);
+ invariant forall j :: 0 <= j < N ==> f.requires(j,old(a[j]));
+ invariant forall j :: i <= j < N ==> a !in f.reads(j,a[j]);
+ invariant forall j :: i <= j < N ==> a[j] == old(a[j]);
+ invariant forall j :: 0 <= j < i ==> a[j] == f(j,old(a[j]));
+ {
+ a[i] := f(i,a[i]);
+ i := i + 1;
+ }
+}
+
+method Main()
+{
+ var v := new int[10];
+ // Hey, works as an initialiser:
+ VectorUpdate(10, v, (i,_) => i);
+ PrintArray(v);
+ VectorUpdate(10, v, (_,x) => x + 1);
+ PrintArray(v);
+ // Phew, now they are all positive, so we can do:
+ VectorUpdate(10, v, (_,x) requires x != 0 => 100 / x);
+ PrintArray(v);
+ var u := new int[10];
+ // Hey, works as a copy as well!
+ VectorUpdate(10, u, (i,_) requires 0 <= i < 10 reads v => v[i]);
+ PrintArray(u);
+ // Having some fun with the index:
+ var z := new int[9];
+ VectorUpdate(9, z, (i,_) requires 0 <= i < 9 reads u => u[i] + u[i+1]);
+ PrintArray(z);
+ assert z[8] == 21; // voila, the prover also knows what's going on
+}
+
+method PrintArray(a : array<int>)
+ requires a != null;
+{
+ var i := 0;
+ while (i < a.Length) {
+ if (i != 0) {
+ print ", ";
+ }
+ print a[i];
+ i := i + 1;
+ }
+ print "\n";
+}
diff --git a/Test/hofs/VectorUpdate.dfy.expect b/Test/hofs/VectorUpdate.dfy.expect
new file mode 100644
index 00000000..b01ace00
--- /dev/null
+++ b/Test/hofs/VectorUpdate.dfy.expect
@@ -0,0 +1,10 @@
+
+Dafny program verifier finished with 6 verified, 0 errors
+Program compiled successfully
+Running...
+
+0, 1, 2, 3, 4, 5, 6, 7, 8, 9
+1, 2, 3, 4, 5, 6, 7, 8, 9, 10
+100, 50, 33, 25, 20, 16, 14, 12, 11, 10
+100, 50, 33, 25, 20, 16, 14, 12, 11, 10
+150, 83, 58, 45, 36, 30, 26, 23, 21