diff options
| author |  Unknown <leino@leino5.redmond.corp.microsoft.com> | 2011-04-04 18:45:15 -0700 |
|---|---|---|
| committer | Unknown <leino@leino5.redmond.corp.microsoft.com> | 2011-04-04 18:45:15 -0700 |
| commit | fbb1ee30ae5b6e2335eb7af7ebb9a83b7c696289 (patch) | |
| tree | e9d6033afdd497dd5dda5c09d4119c87b4fa14ca /Test/dafny1 | |
| parent | 2b09756f836307f75a36c5a982784dc620fda657 (diff) | |
Dafny: fixed bug in induction over integers
Dafny: added pow2 example
Diffstat (limited to 'Test/dafny1')
| -rw-r--r-- | Test/dafny1/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny1/Induction.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny1/pow2.dfy | 54 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 2 |
4 files changed, 61 insertions, 3 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 2fd70cc2..0cd0c5b5 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -43,6 +43,10 @@ Dafny program verifier finished with 9 verified, 0 errors Dafny program verifier finished with 8 verified, 0 errors
+-------------------- pow2.dfy --------------------
+
+Dafny program verifier finished with 8 verified, 0 errors
+
-------------------- SchorrWaite.dfy --------------------
Dafny program verifier finished with 10 verified, 0 errors
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index f31d79f8..c3daad9e 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -119,12 +119,12 @@ class IntegerInduction { // possibility of applying induction. Instead, the "==>" and "<==" cases are given separately.
// Proving the "<==" case is simple; it's the "==>" case that requires induction.
// The example uses an attribute that requests induction on just "j". However, the proof also
- // goes through by applying induction just on "i" or applying induction on both bound variables.
+ // goes through by applying induction on both bound variables.
function method IsSorted(s: seq<int>): bool
ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]);
ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s);
{
- (forall i :: 0 <= i && i+1 < |s| ==> s[i] <= s[i+1])
+ (forall i :: 1 <= i && i < |s| ==> s[i-1] <= s[i])
}
}
diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy new file mode 100644 index 00000000..52cddaac --- /dev/null +++ b/Test/dafny1/pow2.dfy @@ -0,0 +1,54 @@ +// This is a Dafny adaptation of a Coq program by David Pichardie.
+
+function IsEven(n: int): bool
+ requires 0 <= n;
+ ensures IsEven(n) ==> n == (n/2)+(n/2);
+{
+ (n/2)*2 == n
+}
+
+function Square(n: int): int { n * n }
+
+function pow2(n: int): int
+ requires 0 <= n;
+ ensures 0 <= pow2(n);
+{
+ if n == 0 then
+ 1
+ else if IsEven(n) then
+ Square(pow2(n / 2))
+ else
+ 2*pow2(n-1)
+
+}
+
+function pow2_slow(n: int): int
+ requires 0 <= n;
+{
+ if n == 0 then
+ 1
+ else
+ 2*pow2_slow(n-1)
+}
+
+ghost method Lemma(n: int)
+ requires 0 <= n && IsEven(n);
+ ensures pow2_slow(n) == Square(pow2_slow(n/2));
+{
+ if (n != 0) {
+ call Lemma(n-2);
+ }
+}
+
+ghost method Theorem(n: int)
+ requires 0 <= n;
+ ensures pow2(n) == pow2_slow(n);
+{
+ if (n == 0) {
+ } else if (IsEven(n)) {
+ call Lemma(n);
+ call Theorem(n/2);
+ } else {
+ call Theorem(n-1);
+ }
+}
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index 8d34dfc0..b6fc7f62 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -16,7 +16,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy UnboundedStack.dfy
SeparationLogicList.dfy
ListCopy.dfy ListReverse.dfy ListContents.dfy
- MatrixFun.dfy
+ MatrixFun.dfy pow2.dfy
SchorrWaite.dfy
Cubes.dfy SumOfCubes.dfy
TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy
|