diff options
| author |  leino <unknown> | 2014-10-31 22:41:44 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-31 22:41:44 -0700 |
| commit | daba15309feaed1ea06b6b2d9e3205c933010098 (patch) | |
| tree | 45425e60e422cc7e6c13c94ac1c95f4fd3504406 /Test/dafny0/SeqFromArray.dfy | |
| parent | 9f41b35b514eba87a037cbada83f0c294eafb936 (diff) | |
Improved power of axioms Seq#FromArray
Diffstat (limited to 'Test/dafny0/SeqFromArray.dfy')
| -rw-r--r-- | Test/dafny0/SeqFromArray.dfy | 90 |
1 files changed, 90 insertions, 0 deletions
diff --git a/Test/dafny0/SeqFromArray.dfy b/Test/dafny0/SeqFromArray.dfy new file mode 100644 index 00000000..d4c98424 --- /dev/null +++ b/Test/dafny0/SeqFromArray.dfy @@ -0,0 +1,90 @@ +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() { }
+
+method H(a: array<int>, c: array<int>, n: nat, j: nat)
+ requires a != null && c != null
+ requires j < n == a.Length == c.Length
+{
+ var A := a[..];
+ var C := c[..];
+
+ if {
+ case A[j] == C[j] =>
+ assert a[j] == c[j];
+ case forall i :: 0 <= i < n ==> A[i] == C[i] =>
+ assert a[j] == c[j];
+ case forall i :: 0 <= i < n ==> A[i] == C[i] =>
+ assert forall i :: 0 <= i < n ==> a[i] == c[i];
+ case A == C =>
+ assert forall i :: 0 <= i < n ==> A[i] == C[i];
+ case A == C =>
+ assert forall i :: 0 <= i < n ==> a[i] == c[i];
+ case true =>
+ }
+}
+
+method K(a: array<int>, c: array<int>, n: nat)
+ requires a != null && c != null
+ requires n <= a.Length && n <= c.Length
+{
+ var A := a[..n];
+ var C := c[..n];
+ if {
+ case A == C =>
+ assert forall i :: 0 <= i < n ==> A[i] == C[i];
+ case A == C =>
+ assert forall i :: 0 <= i < n ==> a[i] == c[i];
+ case true =>
+ }
+}
+
+method L(a: array<int>, c: array<int>, n: nat)
+ requires a != null && c != null
+ requires n <= a.Length == c.Length
+{
+ var A := a[n..];
+ var C := c[n..];
+ var h := a.Length - n;
+ if {
+ case A == C =>
+ assert forall i :: 0 <= i < h ==> A[i] == C[i];
+ case A == C =>
+ assert forall i :: 0 <= i < h ==> a[n+i] == c[n+i];
+ case true =>
+ }
+}
+
+method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat)
+ requires a != null && c != null
+ requires k + m <= a.Length;
+ requires l + n <= c.Length
+{
+ if {
+ case true =>
+ var A := a[k..k+m];
+ var C := c[l..l+n];
+ if A == C {
+ if * {
+ assert m == n;
+ } else if * {
+ assert forall i :: 0 <= i < n ==> A[i] == C[i];
+ } else if * {
+ assert forall i :: k <= i < k+n ==> A[i-k] == C[i-k];
+ } else if * {
+ assert forall i :: 0 <= i < n ==> A[i] == a[k+i];
+ } else if * {
+ assert forall i :: 0 <= i < n ==> C[i] == c[l+i];
+ } else if * {
+ assert forall i :: 0 <= i < n ==> a[k+i] == c[l+i];
+ }
+ }
+ case l+k+m <= c.Length && forall i :: k <= i < k+m ==> a[i] == c[l+i] =>
+ assert a[k..k+m] == c[l+k..l+k+m];
+ case l+m <= c.Length && forall i :: 0 <= i < m ==> a[i] == c[l+i] =>
+ assert a[..m] == c[l..l+m];
+ case l+a.Length <= c.Length && forall i :: k <= i < a.Length ==> a[i] == c[l+i] =>
+ assert a[k..] == c[l+k..l+a.Length];
+ }
+}
|