diff options
| author |  Rustan Leino <unknown> | 2014-06-24 10:44:38 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-06-24 10:44:38 -0700 |
| commit | 19895aaed833d16bad36a07e9459abc882ccd6b6 (patch) | |
| tree | b5941c67f39f3fdf93f2f894ef1eaa353884a617 /Test/dafny0/Inverses.dfy | |
| parent | 92991242c8ea361b8da5a83bd19462b216387618 (diff) | |
Invert LHS sub-expressions in forall assignment statements, which gives the opportunity to designate a good trigger.
Diffstat (limited to 'Test/dafny0/Inverses.dfy')
| -rw-r--r-- | Test/dafny0/Inverses.dfy | 112 |
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
+ }
+}
|