diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-08-18 14:30:44 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-08-18 14:30:44 -0700 |
| commit | 6f30ae8c13da5f4111b8b923057075852cac78ed (patch) | |
| tree | 3372fdbb722625c5c1a1ce5fe104b99ada5b48d4 /Test/dafny0/Array.dfy | |
| parent | 996afd28c3c65c8cbd0442cd179e31adfdd12562 (diff) | |
Dafny: fixed bug in looking at the arguments of the :induction attribute
Diffstat (limited to 'Test/dafny0/Array.dfy')
| -rw-r--r-- | Test/dafny0/Array.dfy | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index f667e699..6699e648 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -144,3 +144,41 @@ class ArrayTests { b[7] := 13; // good
}
}
+
+// -------------------- induction attribute --------------------------------
+
+ghost method Fill_I(s: seq<int>)
+ requires forall i :: 1 <= i < |s| ==> s[i-1] <= s[i];
+ ensures forall i,j {:induction i} :: 0 <= i < j < |s| ==> s[i] <= s[j];
+{ // error: cannot prove postcondition
+}
+
+ghost method Fill_J(s: seq<int>)
+ requires forall i :: 1 <= i < |s| ==> s[i-1] <= s[i];
+ ensures forall i,j {:induction j} :: 0 <= i < j < |s| ==> s[i] <= s[j];
+{
+}
+
+ghost method Fill_All(s: seq<int>)
+ requires forall i :: 1 <= i < |s| ==> s[i-1] <= s[i];
+ ensures forall i,j {:induction i,j} :: 0 <= i < j < |s| ==> s[i] <= s[j];
+{
+}
+
+ghost method Fill_True(s: seq<int>)
+ requires forall i :: 1 <= i < |s| ==> s[i-1] <= s[i];
+ ensures forall i,j {:induction} :: 0 <= i < j < |s| ==> s[i] <= s[j];
+{
+}
+
+ghost method Fill_False(s: seq<int>)
+ requires forall i :: 1 <= i < |s| ==> s[i-1] <= s[i];
+ ensures forall i,j {:induction false} :: 0 <= i < j < |s| ==> s[i] <= s[j];
+{ // error: cannot prove postcondition
+}
+
+ghost method Fill_None(s: seq<int>)
+ requires forall i :: 1 <= i < |s| ==> s[i-1] <= s[i];
+ ensures forall i,j :: 0 <= i < j < |s| ==> s[i] <= s[j];
+{ // error: cannot prove postcondition
+}
|