diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 29 | ||||
| -rw-r--r-- | Test/dafny0/SeqFromArray.dfy | 90 | ||||
| -rw-r--r-- | Test/dafny0/SeqFromArray.dfy.expect | 5 |
3 files changed, 119 insertions, 5 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 91d8a01a..eea23383 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -872,7 +872,10 @@ axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) } 0 <= n ==>
(n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&
(Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));
-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:weight 25}
+axiom (forall<T> s: Seq T, n: int, j: int ::
+ {:weight 25}
+ { Seq#Index(Seq#Take(s,n), j) }
+ { Seq#Index(s, j), Seq#Take(s,n) }
0 <= j && j < n && j < Seq#Length(s) ==>
Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));
@@ -881,9 +884,16 @@ axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) } 0 <= n ==>
(n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&
(Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));
-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } {:weight 25}
+axiom (forall<T> s: Seq T, n: int, j: int ::
+ {:weight 25}
+ { Seq#Index(Seq#Drop(s,n), j) }
0 <= n && 0 <= j && j < Seq#Length(s)-n ==>
Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));
+axiom (forall<T> s: Seq T, n: int, k: int ::
+ {:weight 25}
+ { Seq#Index(s, k), Seq#Drop(s,n) }
+ 0 <= n && n <= k && k < Seq#Length(s) ==>
+ Seq#Index(Seq#Drop(s,n), k-n) == Seq#Index(s, k));
axiom (forall<T> s, t: Seq T ::
{ Seq#Append(s, t) }
@@ -894,9 +904,18 @@ function Seq#FromArray(h: Heap, a: ref): Seq Box; axiom (forall h: Heap, a: ref ::
{ Seq#Length(Seq#FromArray(h,a)) }
Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));
-axiom (forall h: Heap, a: ref, i: int ::
- { Seq#Index(Seq#FromArray(h, a): Seq Box, i) }
- 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i)));
+axiom (forall h: Heap, a: ref ::
+ { Seq#FromArray(h, a) }
+ (forall i: int ::
+ // it's important to include both triggers, so that assertions about the
+ // the relation between the array and the sequence can be proved in either
+ // direction
+ { read(h, a, IndexField(i)) }
+ { Seq#Index(Seq#FromArray(h, a): Seq Box, i) }
+ 0 <= i &&
+ i < Seq#Length(Seq#FromArray(h, a)) // this will trigger the previous axiom to get a connection with _System.array.Length(a)
+ ==>
+ Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));
axiom (forall h0, h1: Heap, a: ref ::
{ Seq#FromArray(h1, a), $HeapSucc(h0, h1) }
$IsGoodHeap(h0) && $IsGoodHeap(h1) && $HeapSucc(h0, h1) &&
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];
+ }
+}
diff --git a/Test/dafny0/SeqFromArray.dfy.expect b/Test/dafny0/SeqFromArray.dfy.expect new file mode 100644 index 00000000..af845d3e --- /dev/null +++ b/Test/dafny0/SeqFromArray.dfy.expect @@ -0,0 +1,5 @@ +
+Dafny program verifier finished with 10 verified, 0 errors
+Program compiled successfully
+Running...
+
|