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 | bff446fb46898a2ef6222e957baef8ea5f788513 (patch) | |
| tree | 86d7ea7281d3d6baf3c37dd346f621dbd391202d /Test/dafny1/Induction.dfy | |
| parent | 6e93acd001f5d23c08b02c162dc2111e531f3d5d (diff) | |
Dafny: fixed bug in induction over integers
Dafny: added pow2 example
Diffstat (limited to 'Test/dafny1/Induction.dfy')
| -rw-r--r-- | Test/dafny1/Induction.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
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])
}
}
|