2 files changed, 20 insertions, 1 deletions

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 4bf200cd..d9b32305 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -73,7 +73,7 @@ Dafny program verifier finished with 6 verified, 0 errors
 

 -------------------- Induction.dfy --------------------

 

-Dafny program verifier finished with 22 verified, 0 errors

+Dafny program verifier finished with 23 verified, 0 errors

 

 -------------------- Rippling.dfy --------------------

 

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 4bd1f35b..f31d79f8 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -107,6 +107,25 @@ class IntegerInduction {
       call Theorem4();

     }

   }

+

+  // The body of this function method gives a single quantifier, which leads to an efficient

+  // way to check sortedness at run time.  However, an alternative, and ostensibly more general,

+  // way to express sortedness is given in the function's postcondition.  The alternative

+  // formulation may be easier to understand for a human and may also be more readily applicable

+  // for the program verifier.  Dafny will show that postcondition holds, which ensures the

+  // equivalence of the two formulations.

+  // The proof of the postcondition requires induction.  It would have been nicer to state it

+  // as one formula of the form "IsSorted(s) <==> ...", but then Dafny would never consider the

+  // 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.

+  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])

+  }

 }

 

 datatype Tree<T> {