diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-02-29 21:36:03 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-02-29 21:36:03 -0800 |
| commit | 8bcdbb318c0c61b1148705accccb294906cdffb1 (patch) | |
| tree | 3753794e9788e5e9dfb1257d5751dc0b5fb7efa8 | |
| parent | ba75a2d0b67ce5c330abd1903a6942a9b385d361 (diff) | |
Dafny: fixed well-formedness checking of LET expressions to allow the RHS to be used
| -rw-r--r-- | Dafny/Translator.cs | 17 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/LetExpr.dfy | 40 |
3 files changed, 57 insertions, 6 deletions
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index c0a56d05..40d7c266 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -2406,10 +2406,21 @@ namespace Microsoft.Dafny { } else if (expr is LetExpr) {
var e = (LetExpr)expr;
- foreach (var rhs in e.RHSs) {
- CheckWellformed(rhs, options, locals, builder, etran);
+
+ var substMap = new Dictionary<IVariable, Expression>();
+ Contract.Assert(e.Vars.Count == e.RHSs.Count); // checked by resolution
+ for (int i = 0; i < e.Vars.Count; i++) {
+ var vr = e.Vars[i];
+ var tp = TrType(vr.Type);
+ var v = new Bpl.LocalVariable(vr.tok, new Bpl.TypedIdent(vr.tok, vr.UniqueName, tp));
+ locals.Add(v);
+ var lhs = new Bpl.IdentifierExpr(vr.tok, vr.UniqueName, tp);
+
+ CheckWellformedWithResult(e.RHSs[i], options, lhs, vr.Type, locals, builder, etran);
+ substMap.Add(vr, new BoogieWrapper(lhs, vr.Type));
}
- CheckWellformedWithResult(etran.GetSubstitutedBody(e), options, result, resultType, locals, builder, etran);
+ CheckWellformedWithResult(Substitute(e.Body, null, substMap), options, result, resultType, locals, builder, etran);
+ result = null;
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index d0dfc9be..bbf9769d 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1445,7 +1445,7 @@ Execution trace: (0,0): anon0
(0,0): anon11_Then
-Dafny program verifier finished with 13 verified, 2 errors
+Dafny program verifier finished with 19 verified, 2 errors
-------------------- Predicates.dfy --------------------
Predicates.dfy[B](18,5): Error BP5003: A postcondition might not hold on this return path.
@@ -1705,7 +1705,7 @@ Execution trace: (0,0): anon0
(0,0): anon11_Then
-Dafny program verifier finished with 13 verified, 2 errors
+Dafny program verifier finished with 19 verified, 2 errors
out.tmp.dfy(10,12): Error: assertion violation
Execution trace:
(0,0): anon0
@@ -1714,4 +1714,4 @@ Execution trace: (0,0): anon0
(0,0): anon11_Then
-Dafny program verifier finished with 13 verified, 2 errors
+Dafny program verifier finished with 19 verified, 2 errors
diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy index 48e4810b..11bf4fbe 100644 --- a/Test/dafny0/LetExpr.dfy +++ b/Test/dafny0/LetExpr.dfy @@ -107,3 +107,43 @@ method PMain(a: array<int>) assert index == old(index) ==> a[index] == 21 && old(a[index]) == 19;
}
}
+
+// ---------- lemmas ----------
+
+method Theorem0(n: int)
+ requires 1 <= n;
+ ensures 1 <= Fib(n);
+{
+ if (n < 3) {
+ } else {
+ Theorem0(n-2);
+ Theorem0(n-1);
+ }
+}
+
+ghost method Theorem1(n: int)
+ requires 1 <= n;
+ ensures 1 <= Fib(n);
+{
+ // in a ghost method, the induction tactic takes care of it
+}
+
+function Theorem2(n: int): int
+ requires 1 <= n;
+ ensures 1 <= Fib(n);
+{
+ if n < 3 then 5 else
+ var x := Theorem2(n-2);
+ var y := Theorem2(n-1);
+ x + y
+}
+
+function Theorem3(n: int): int
+ requires 1 <= n;
+ ensures 1 <= Fib(n);
+{
+ if n < 3 then 5 else
+ var x := Theorem3(n-2);
+ var y := Theorem3(n-1);
+ 5
+}
|