summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Compiler.cs4
-rw-r--r--Source/Dafny/Dafny.atg10
-rw-r--r--Source/Dafny/DafnyAst.cs47
-rw-r--r--Source/Dafny/Parser.cs53
-rw-r--r--Source/Dafny/Printer.cs10
-rw-r--r--Source/Dafny/Resolver.cs14
-rw-r--r--Source/Dafny/Translator.cs64
-rw-r--r--Test/dafny0/Answer11
-rw-r--r--Test/dafny0/PredExpr.dfy43
-rw-r--r--Test/dafny0/runtest.bat2
10 files changed, 241 insertions, 17 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 61b0398f..de863e39 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1767,6 +1767,10 @@ namespace Microsoft.Dafny {
wr.Write("return Dafny.Set<{0}>.FromCollection(_coll); ", typeName);
wr.Write("})()");
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ TrExpr(e.Body);
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
wr.Write("(");
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index fa857aad..8a9108f0 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1205,13 +1205,19 @@ EndlessExpression<out Expression e>
Expression e0, e1;
e = dummyExpr;
.)
- ( "if" (. x = t; .)
+ ( "if" (. x = t; .)
Expression<out e>
"then" Expression<out e0>
- "else" Expression<out e1> (. e = new ITEExpr(x, e, e0, e1); .)
+ "else" Expression<out e1> (. e = new ITEExpr(x, e, e0, e1); .)
| MatchExpression<out e>
| QuantifierGuts<out e>
| ComprehensionExpr<out e>
+ | "assert" (. x = t; .)
+ Expression<out e0> ";"
+ Expression<out e1> (. e = new AssertExpr(x, e0, e1); .)
+ | "assume" (. x = t; .)
+ Expression<out e0> ";"
+ Expression<out e1> (. e = new AssumeExpr(x, e0, e1); .)
)
.
MatchExpression<out Expression/*!*/ e>
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index bf8eb6b0..04b6b00e 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2721,7 +2721,52 @@ namespace Microsoft.Dafny {
}
}
- public class ITEExpr : Expression {
+ public abstract class PredicateExpr : Expression
+ {
+ public readonly Expression Guard;
+ public readonly Expression Body;
+ public PredicateExpr(IToken tok, Expression guard, Expression body)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(guard != null);
+ Contract.Requires(body != null);
+ Guard = guard;
+ Body = body;
+ }
+ public abstract string Kind { get; }
+
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return Guard;
+ yield return Body;
+ }
+ }
+ }
+
+ public class AssertExpr : PredicateExpr
+ {
+ public AssertExpr(IToken tok, Expression guard, Expression body)
+ : base(tok, guard, body) {
+ Contract.Requires(tok != null);
+ Contract.Requires(guard != null);
+ Contract.Requires(body != null);
+ }
+ public override string Kind { get { return "assert"; } }
+ }
+
+ public class AssumeExpr : PredicateExpr
+ {
+ public AssumeExpr(IToken tok, Expression guard, Expression body)
+ : base(tok, guard, body) {
+ Contract.Requires(tok != null);
+ Contract.Requires(guard != null);
+ Contract.Requires(body != null);
+ }
+ public override string Kind { get { return "assume"; } }
+ }
+
+ public class ITEExpr : Expression
+ {
public readonly Expression Test;
public readonly Expression Thn;
public readonly Expression Els;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 2fc50c37..0dc30e8a 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1789,7 +1789,7 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 38: case 55: case 61: case 98: case 99: case 100: case 101: {
+ case 38: case 55: case 61: case 62: case 63: case 98: case 99: case 100: case 101: {
EndlessExpression(out e);
break;
}
@@ -1846,7 +1846,8 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression e0, e1;
e = dummyExpr;
- if (la.kind == 55) {
+ switch (la.kind) {
+ case 55: {
Get();
x = t;
Expression(out e);
@@ -1855,13 +1856,40 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(56);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
- } else if (la.kind == 61) {
+ break;
+ }
+ case 61: {
MatchExpression(out e);
- } else if (StartOf(15)) {
+ break;
+ }
+ case 98: case 99: case 100: case 101: {
QuantifierGuts(out e);
- } else if (la.kind == 38) {
+ break;
+ }
+ case 38: {
ComprehensionExpr(out e);
- } else SynErr(133);
+ break;
+ }
+ case 62: {
+ Get();
+ x = t;
+ Expression(out e0);
+ Expect(17);
+ Expression(out e1);
+ e = new AssertExpr(x, e0, e1);
+ break;
+ }
+ case 63: {
+ Get();
+ x = t;
+ Expression(out e0);
+ Expect(17);
+ Expression(out e1);
+ e = new AssumeExpr(x, e0, e1);
+ break;
+ }
+ default: SynErr(133); break;
+ }
}
void DottedIdentifiersAndFunction(out Expression e) {
@@ -2014,7 +2042,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression(out e);
e = new MultiSetFormingExpr(x, e);
Expect(34);
- } else if (StartOf(16)) {
+ } else if (StartOf(15)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
} else SynErr(138);
}
@@ -2233,7 +2261,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(22);
Expect(1);
aName = t.val;
- if (StartOf(17)) {
+ if (StartOf(16)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 19) {
@@ -2263,18 +2291,17 @@ List<Expression/*!*/>/*!*/ decreases) {
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},
{x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, T,T,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,x,x, T,T,T,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x},
- {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
+ {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
};
} // end Parser
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 7f7ba963..10099bf4 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1054,6 +1054,16 @@ namespace Microsoft.Dafny {
} else if (expr is WildcardExpr) {
wr.Write("*");
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ bool parensNeeded = !isRightmost;
+ if (parensNeeded) { wr.Write("("); }
+ wr.Write("{0} ", e.Kind);
+ PrintExpression(e.Guard);
+ wr.Write("; ");
+ PrintExpression(e.Body);
+ if (parensNeeded) { wr.Write(")"); }
+
} else if (expr is ITEExpr) {
ITEExpr ite = (ITEExpr)expr;
bool parensNeeded = !isRightmost;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 2d3ddcca..c7fb8481 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2823,6 +2823,17 @@ namespace Microsoft.Dafny {
} else if (expr is WildcardExpr) {
expr.Type = new SetType(new ObjectType());
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ ResolveExpression(e.Guard, twoState);
+ Contract.Assert(e.Guard.Type != null); // follows from postcondition of ResolveExpression
+ ResolveExpression(e.Body, twoState);
+ Contract.Assert(e.Body.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Guard.Type, Type.Bool)) {
+ Error(expr, "guard condition in {0} expression must be a boolean (instead got {1})", e.Kind, e.Guard.Type);
+ }
+ expr.Type = e.Body.Type;
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
ResolveExpression(e.Test, twoState);
@@ -3932,6 +3943,9 @@ namespace Microsoft.Dafny {
return (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));
} else if (expr is WildcardExpr) {
return false;
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ return UsesSpecFeatures(e.Body);
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
return UsesSpecFeatures(e.Test) || UsesSpecFeatures(e.Thn) || UsesSpecFeatures(e.Els);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e455561a..37f80bf1 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1789,6 +1789,16 @@ namespace Microsoft.Dafny {
total = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, total));
}
return total;
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ Bpl.Expr gTotal = IsTotal(e.Guard, etran);
+ Bpl.Expr g = etran.TrExpr(e.Guard);
+ Bpl.Expr bTotal = IsTotal(e.Body, etran);
+ if (e is AssertExpr) {
+ return BplAnd(gTotal, BplAnd(g, bTotal));
+ } else {
+ return BplAnd(gTotal, Bpl.Expr.Imp(g, bTotal));
+ }
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
Bpl.Expr total = IsTotal(e.Test, etran);
@@ -1925,6 +1935,16 @@ namespace Microsoft.Dafny {
total = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, total));
}
return total;
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ Bpl.Expr gCanCall = CanCallAssumption(e.Guard, etran);
+ Bpl.Expr g = etran.TrExpr(e.Guard);
+ Bpl.Expr bCanCall = CanCallAssumption(e.Body, etran);
+ if (e is AssertExpr) {
+ return BplAnd(gCanCall, BplAnd(g, bCanCall));
+ } else {
+ return BplAnd(gCanCall, Bpl.Expr.Imp(g, bCanCall));
+ }
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
Bpl.Expr total = CanCallAssumption(e.Test, etran);
@@ -2316,6 +2336,27 @@ namespace Microsoft.Dafny {
builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(range), b.Collect(expr.tok), null, null));
}
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ CheckWellformed(e.Guard, options, locals, builder, etran);
+ if (e is AssertExpr) {
+ bool splitHappened;
+ var ss = TrSplitExpr(e.Guard, etran, out splitHappened);
+ if (!splitHappened) {
+ builder.Add(Assert(e.Guard.tok, etran.TrExpr(e.Guard), "condition in assert expression might not hold"));
+ } else {
+ foreach (var split in ss) {
+ if (!split.IsFree) {
+ builder.Add(AssertNS(split.E.tok, split.E, "condition in assert expression might not hold"));
+ }
+ }
+ builder.Add(new Bpl.AssumeCmd(e.tok, etran.TrExpr(e.Guard)));
+ }
+ } else {
+ builder.Add(new Bpl.AssumeCmd(e.tok, etran.TrExpr(e.Guard)));
+ }
+ CheckWellformed(e.Body, options, locals, builder, etran);
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
CheckWellformed(e.Test, options, locals, builder, etran);
@@ -5547,6 +5588,10 @@ namespace Microsoft.Dafny {
return new Bpl.LambdaExpr(expr.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, exst);
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ return TrExpr(e.Body);
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
Bpl.Expr g = TrExpr(e.Test);
@@ -6349,6 +6394,10 @@ namespace Microsoft.Dafny {
var e = (ConcreteSyntaxExpression)expr;
return TrSplitExpr(e.ResolvedExpression, splits, position, expandFunctions, etran);
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ return TrSplitExpr(e.Body, splits, position, expandFunctions, etran);
+
} else if (expr is UnaryExpr) {
var e = (UnaryExpr)expr;
if (e.Op == UnaryExpr.Opcode.Not) {
@@ -6819,6 +6868,11 @@ namespace Microsoft.Dafny {
}
return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) ||
VarOccursInArgumentToRecursiveFunction(e.E1, n, q);
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ // ignore the guard
+ return VarOccursInArgumentToRecursiveFunction(e.Body, n);
+
} else if (expr is ITEExpr) {
var e = (ITEExpr)expr;
return VarOccursInArgumentToRecursiveFunction(e.Test, n, subExprIsProminent) || // test is not "prominent"
@@ -7044,6 +7098,16 @@ namespace Microsoft.Dafny {
Contract.Assume(false); // unexpected ComprehensionExpr
}
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ Expression g = Substitute(e.Guard, receiverReplacement, substMap);
+ Expression b = Substitute(e.Body, receiverReplacement, substMap);
+ if (expr is AssertExpr) {
+ newExpr = new AssertExpr(e.tok, g, b);
+ } else {
+ newExpr = new AssumeExpr(e.tok, g, b);
+ }
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
Expression test = Substitute(e.Test, receiverReplacement, substMap);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index bae3aa50..bcdb7126 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1311,3 +1311,14 @@ CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost
-------------------- MultiSets.dfy --------------------
Dafny program verifier finished with 22 verified, 0 errors
+
+-------------------- PredExpr.dfy --------------------
+PredExpr.dfy(23,15): Error: value assigned to a nat must be non-negative
+Execution trace:
+ (0,0): anon6_Else
+ (0,0): anon7_Else
+PredExpr.dfy(36,17): Error: condition in assert expression might not hold
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 7 verified, 2 errors
diff --git a/Test/dafny0/PredExpr.dfy b/Test/dafny0/PredExpr.dfy
new file mode 100644
index 00000000..3499a01c
--- /dev/null
+++ b/Test/dafny0/PredExpr.dfy
@@ -0,0 +1,43 @@
+function Subonacci(n: nat): nat
+{
+ if 2 <= n then
+ // proving that this case is a nat requires more information,
+ // which is here supplied by an assume expression
+ assume Subonacci(n-2) <= Subonacci(n-1);
+ Subonacci(n-1) - Subonacci(n-2)
+ else
+ n
+}
+
+function F(n: int): nat
+{
+ Subonacci(assume 0 <= n; n) -
+ Subonacci(n)
+}
+
+function G(n: int, b: bool): nat
+{
+ if b then
+ Subonacci(assume 0 <= n; n)
+ else
+ Subonacci(n) // error: n may not be a nat
+}
+
+ghost method M(m: nat, n: int)
+{
+ var k := F(m);
+ assert k == 0;
+ k := F(n);
+ assert k == 0; // this is still known
+}
+
+method M0(j: int) returns (n: nat)
+{
+ n := assert 0 <= j; j; // error: j may be negative
+}
+
+method M1(j: int) returns (n: nat)
+{
+ n := (assume 0 <= j; j) + (assert 0 <= j; j);
+ assert n == 2*j;
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index c30ec3a5..32a60340 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -20,7 +20,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
Refinement.dfy RefinementErrors.dfy LoopModifies.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
- CallStmtTests.dfy MultiSets.dfy) do (
+ CallStmtTests.dfy MultiSets.dfy PredExpr.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 12:26:44 +0000