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 | |
| parent | 996afd28c3c65c8cbd0442cd179e31adfdd12562 (diff) | |
Dafny: fixed bug in looking at the arguments of the :induction attribute
| -rw-r--r-- | Dafny/Translator.cs | 2 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 14 | ||||
| -rw-r--r-- | Test/dafny0/Array.dfy | 38 |
3 files changed, 52 insertions, 2 deletions
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index cc97fb40..998eeb3a 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -6063,7 +6063,7 @@ namespace Microsoft.Dafny { if (a.Args.Count != 0) {
var L = new List<BoundVar>();
foreach (var arg in a.Args) {
- var id = arg.E as IdentifierExpr;
+ var id = arg.E.Resolved as IdentifierExpr;
var bv = id == null ? null : id.Var as BoundVar;
if (bv != null && e.BoundVars.Contains(bv)) {
// add to L, but don't add duplicates
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 9a8c7541..3a650ce2 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -520,8 +520,20 @@ Execution trace: Array.dfy(128,6): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
+Array.dfy(153,1): Error BP5003: A postcondition might not hold on this return path.
+Array.dfy(152,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+Array.dfy(177,1): Error BP5003: A postcondition might not hold on this return path.
+Array.dfy(176,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+Array.dfy(183,1): Error BP5003: A postcondition might not hold on this return path.
+Array.dfy(182,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 21 verified, 10 errors
+Dafny program verifier finished with 30 verified, 13 errors
-------------------- MultiDimArray.dfy --------------------
MultiDimArray.dfy(53,21): Error: assertion violation
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
+}
|