diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-13 14:47:55 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-13 14:47:55 -0700 |
| commit | daaaf8cfb87024a3c7b03bd83ea9e0dd4c619203 (patch) | |
| tree | 307338289f5a0ab92954e20168af5e6763cc7b90 /Test/dafny1 | |
| parent | bef81a88562baf473a01df2df52a08b506da1561 (diff) | |
| parent | 59351f9ee9e0eb809339065ce9cd61222b39dea8 (diff) | |
Merge
Diffstat (limited to 'Test/dafny1')
| -rw-r--r-- | Test/dafny1/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny1/FindZero.dfy | 30 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 2 |
3 files changed, 35 insertions, 1 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index d96e12a5..d0eba7cb 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -59,6 +59,10 @@ Dafny program verifier finished with 2 verified, 0 errors Dafny program verifier finished with 17 verified, 0 errors
+-------------------- FindZero.dfy --------------------
+
+Dafny program verifier finished with 4 verified, 0 errors
+
-------------------- TerminationDemos.dfy --------------------
Dafny program verifier finished with 11 verified, 0 errors
diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy new file mode 100644 index 00000000..cff8b934 --- /dev/null +++ b/Test/dafny1/FindZero.dfy @@ -0,0 +1,30 @@ +method FindZero(a: array<int>) returns (r: int)
+ requires a != null && forall i :: 0 <= i && i < a.Length ==> 0 <= a[i];
+ requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ ensures 0 <= r ==> r < a.Length && a[r] == 0;
+ ensures r < 0 ==> forall i :: 0 <= i && i < a.Length ==> a[i] != 0;
+{
+ var n := 0;
+ while (n < a.Length)
+ invariant forall i :: 0 <= i && i < n && i < a.Length ==> a[i] != 0;
+ {
+ if (a[n] == 0) { r := n; return; }
+ call Lemma(a, n, a[n]);
+ n := n + a[n];
+ }
+ r := -1;
+}
+
+ghost method Lemma(a: array<int>, k: int, m: int)
+ requires a != null && forall i :: 0 <= i && i < a.Length ==> 0 <= a[i];
+ requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ requires 0 <= k;
+ requires k < a.Length ==> m <= a[k];
+ ensures forall i :: k <= i && i < k+m && i < a.Length ==> a[i] != 0;
+ decreases m;
+{
+ if (0 < m && k < a.Length) {
+ assert a[k] != 0;
+ call Lemma(a, k+1, m-1);
+ }
+}
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index 36b93883..57ac97e3 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -19,7 +19,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy ListCopy.dfy ListReverse.dfy ListContents.dfy
MatrixFun.dfy pow2.dfy
SchorrWaite.dfy
- Cubes.dfy SumOfCubes.dfy
+ Cubes.dfy SumOfCubes.dfy FindZero.dfy
TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy
Induction.dfy Rippling.dfy
Celebrity.dfy
|