1 files changed, 112 insertions, 0 deletions
diff --git a/Test/dafny0/Inverses.dfy b/Test/dafny0/Inverses.dfy
new file mode 100644
index 00000000..7995255a
--- /dev/null
+++ b/Test/dafny0/Inverses.dfy
@@ -0,0 +1,112 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This identity function is used to so that if the occurrence of i below
+// that is enclosed by Id gets chosen by the SMT solver as a trigger, then
+// Id will be part of that trigger.  This means that the quantifier will
+// not match, and thus the 'forall' statement will be useless and the method
+// will not verify.  If, however, the inverting functionality in Dafny
+// works properly, then the 'i' in the right-hand side of the forall assignments
+// below will not be chosen in any trigger, and then the methods should
+// verify.
+function method Id(x: int): int { x }
+
+method Copy<T>(a: array<T>) returns (r: array<T>)
+  requires a != null;
+  ensures fresh(r) && r.Length == a.Length && forall k :: 0 <= k < a.Length ==> r[k] == a[k];
+{
+  r := new T[a.Length];
+  forall i | 0 <= i < a.Length {
+    r[i] := a[Id(i)];
+  }
+}
+
+method ShiftLeftA<T>(a: array<T>, n: nat) returns (r: array<T>)
+  requires a != null && n <= a.Length;
+  ensures fresh(r) && r.Length == a.Length - n && forall k :: n <= k < a.Length ==> r[k - n] == a[k];
+{
+  r := new T[a.Length - n];
+  forall i | 0 <= i < a.Length - n {
+    r[i] := a[i + n];
+  }
+}
+
+method ShiftLeftB<T>(a: array<T>, n: nat) returns (r: array<T>)
+  requires a != null && n <= a.Length;
+  ensures fresh(r) && r.Length == a.Length - n && forall k :: 0 <= k < a.Length - n ==> r[k] == a[k + n];
+{
+  r := new T[a.Length - n];
+  forall i | n <= i < a.Length {
+    r[i - n] := a[Id(i)];
+  }
+}
+
+method ShiftLeftC<T>(a: array<T>, n: nat) returns (r: array<T>)
+  requires a != null && n <= a.Length;
+  ensures fresh(r) && r.Length == a.Length - n && forall k :: 0 <= k < a.Length - n ==> r[k] == a[k + n];
+{
+  r := new T[a.Length - n];
+  forall i | n <= i < a.Length {
+    r[i + 15 - n - 15] := a[Id(i)];
+  }
+}
+
+method Insert<T>(a: array<T>, p: nat, n: nat) returns (r: array<T>)
+  requires a != null && p <= a.Length;
+  ensures fresh(r) && r.Length == a.Length + n;
+  ensures forall k :: 0 <= k < p ==> r[k] == a[k];
+  ensures forall k :: p <= k < a.Length ==> r[k + n] == a[k];
+{
+  r := new T[a.Length + n];
+  forall i | 0 <= i < a.Length {
+    r[if i < p then i else i + n] := a[Id(i)];
+  }
+}
+
+method RotateA<T>(a: array<T>) returns (r: array<T>)
+  requires a != null;
+  ensures fresh(r) && r.Length == a.Length;
+  ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];
+{
+  r := new T[a.Length];
+  forall i | 0 <= i < a.Length {
+    r[(i + 1) % a.Length] := a[Id(i)];  // error: Dafny does not find an inverse for this one,
+                                        // which causes Z3 to pick Id(i) as the trigger, which
+                                        // causes the verification to fail.
+  }
+}
+
+method RotateB<T>(a: array<T>) returns (r: array<T>)
+  requires a != null;
+  ensures fresh(r) && r.Length == a.Length;
+  ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];
+{
+  r := new T[a.Length];
+  forall i | 0 <= i < a.Length {
+    r[if i + 1 == a.Length then 0 else i + 1] := a[Id(i)];  // error: Dafny does not find an inverse
+                                                            // for this one, so (like in RotateA),
+                                                            // the verification fails.
+  }
+}
+
+method RotateC<T>(a: array<T>) returns (r: array<T>)
+  requires a != null;
+  ensures fresh(r) && r.Length == a.Length;
+  ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];
+{
+  r := new T[a.Length];
+  forall i | 0 <= i < a.Length {
+    r[if i == a.Length - 1 then 0 else i + 1] := a[Id(i)];  // yes, Dafny can invert this one
+  }
+}
+
+method RotateD<T>(a: array<T>) returns (r: array<T>)
+  requires a != null;
+  ensures fresh(r) && r.Length == a.Length;
+  ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];
+{
+  r := new T[a.Length];
+  forall i | 0 <= i < a.Length {
+    r[if a.Length - 1 == i then 0 else i + 1] := a[Id(i)];  // yes, Dafny can invert this one
+  }
+}