diff options
author | 2011-05-16 13:45:15 -0700 | |
---|---|---|
committer | 2011-05-16 13:45:15 -0700 | |
commit | fe6be535d3d792ef47d0aee23d04fa971d490654 (patch) | |
tree | 4be29111eafa70e223503626c71a21baa13e927b | |
parent | ddebd84b961b6ac942e4e97380ac1ff874e97386 (diff) | |
parent | f448d52dce21c0ed55369af51522d130cb1737b8 (diff) |
Merge
-rw-r--r-- | Source/Dafny/Compiler.cs | 2 | ||||
-rw-r--r-- | Source/Dafny/Dafny.atg | 8 | ||||
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 73 | ||||
-rw-r--r-- | Source/Dafny/Parser.cs | 9 | ||||
-rw-r--r-- | Source/Dafny/Printer.cs | 9 | ||||
-rw-r--r-- | Source/Dafny/Resolver.cs | 19 | ||||
-rw-r--r-- | Source/Dafny/Translator.cs | 33 | ||||
-rw-r--r-- | Test/dafny0/Answer | 31 | ||||
-rw-r--r-- | Test/dafny0/NonGhostQuantifiers.dfy | 17 | ||||
-rw-r--r-- | Test/dafny0/SmallTests.dfy | 36 | ||||
-rw-r--r-- | Test/dafny1/Answer | 2 | ||||
-rw-r--r-- | Test/dafny1/TerminationDemos.dfy | 22 |
12 files changed, 208 insertions, 53 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 9495d64e..4d352f65 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1335,7 +1335,7 @@ namespace Microsoft.Dafny { wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");
wr.Write("@{0} => ", bv.Name);
}
- TrExpr(e.Body);
+ TrExpr(e.LogicalBody());
for (int i = 0; i < n; i++) {
wr.Write(")");
}
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 39c4c29d..0ce1835f 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1361,6 +1361,7 @@ QuantifierGuts<out Expression/*!*/ q> List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
Attributes attrs = null;
Triggers trigs = null;
+ Expression range = null;
Expression/*!*/ body;
.)
( Forall (. x = t; univ = true; .)
@@ -1372,12 +1373,15 @@ QuantifierGuts<out Expression/*!*/ q> IdentTypeOptional<out bv> (. bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); .)
}
{ AttributeOrTrigger<ref attrs, ref trigs> }
+ [ "|"
+ Expression<out range>
+ ]
QSep
Expression<out body>
(. if (univ) {
- q = new ForallExpr(x, bvars, body, trigs, attrs);
+ q = new ForallExpr(x, bvars, range, body, trigs, attrs);
} else {
- q = new ExistsExpr(x, bvars, body, trigs, attrs);
+ q = new ExistsExpr(x, bvars, range, body, trigs, attrs);
}
parseVarScope.PopMarker();
.)
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index f76f24de..ad7f5fb6 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2300,17 +2300,23 @@ namespace Microsoft.Dafny { }
}
- public abstract class QuantifierExpr : Expression {
+ /// <summary>
+ /// A ComprehensionExpr has the form:
+ /// BINDER x Attributes | Range(x) :: Term(x)
+ /// where "Attributes" is optional, and "| Range(x)" is optional and defaults to "true".
+ /// Currently, BINDER is one of the logical quantifiers "exists" or "forall".
+ /// </summary>
+ public abstract class ComprehensionExpr : Expression {
public readonly List<BoundVar/*!*/>/*!*/ BoundVars;
- public readonly Expression/*!*/ Body;
+ public readonly Expression Range;
+ public readonly Expression/*!*/ Term;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(BoundVars != null);
- Contract.Invariant(Body != null);
+ Contract.Invariant(Term != null);
}
- public readonly Triggers Trigs;
public readonly Attributes Attributes;
public abstract class BoundedPool { }
@@ -2338,23 +2344,40 @@ namespace Microsoft.Dafny { }
public List<BoundedPool> Bounds; // initialized and filled in by resolver
- // invariant bounds == null || bounds.Count == BoundVars.Count;
+ // invariant Bounds == null || Bounds.Count == BoundVars.Count;
- public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ body, Triggers trigs, Attributes attrs)
+ public ComprehensionExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression/*!*/ term, Attributes attrs)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(bvars));
- Contract.Requires(body != null);
+ Contract.Requires(term != null);
this.BoundVars = bvars;
- this.Body = body;
- this.Trigs = trigs;
+ this.Range = range;
+ this.Term = term;
this.Attributes = attrs;
}
public override IEnumerable<Expression> SubExpressions {
- get { yield return Body; }
+ get {
+ if (Range != null) { yield return Range; }
+ yield return Term;
+ }
+ }
+ }
+
+ public abstract class QuantifierExpr : ComprehensionExpr {
+ public readonly Triggers Trigs;
+
+ public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression/*!*/ term, Triggers trigs, Attributes attrs)
+ : base(tok, bvars, range, term, attrs) {
+ Contract.Requires(tok != null);
+ Contract.Requires(cce.NonNullElements(bvars));
+ Contract.Requires(term != null);
+
+ this.Trigs = trigs;
}
+ public abstract Expression/*!*/ LogicalBody();
}
public class Triggers {
@@ -2373,20 +2396,38 @@ namespace Microsoft.Dafny { }
public class ForallExpr : QuantifierExpr {
- public ForallExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression body, Triggers trig, Attributes attrs)
- : base(tok, bvars, body, trig, attrs) {
+ public ForallExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression term, Triggers trig, Attributes attrs)
+ : base(tok, bvars, range, term, trig, attrs) {
Contract.Requires(cce.NonNullElements(bvars));
Contract.Requires(tok != null);
- Contract.Requires(body != null);
+ Contract.Requires(term != null);
+ }
+ public override Expression/*!*/ LogicalBody() {
+ if (Range == null) {
+ return Term;
+ }
+ var body = new BinaryExpr(Term.tok, BinaryExpr.Opcode.Imp, Range, Term);
+ body.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;
+ body.Type = Term.Type;
+ return body;
}
}
public class ExistsExpr : QuantifierExpr {
- public ExistsExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression body, Triggers trig, Attributes attrs)
- : base(tok, bvars, body, trig, attrs) {
+ public ExistsExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression term, Triggers trig, Attributes attrs)
+ : base(tok, bvars, range, term, trig, attrs) {
Contract.Requires(cce.NonNullElements(bvars));
Contract.Requires(tok != null);
- Contract.Requires(body != null);
+ Contract.Requires(term != null);
+ }
+ public override Expression/*!*/ LogicalBody() {
+ if (Range == null) {
+ return Term;
+ }
+ var body = new BinaryExpr(Term.tok, BinaryExpr.Opcode.And, Range, Term);
+ body.ResolvedOp = BinaryExpr.ResolvedOpcode.And;
+ body.Type = Term.Type;
+ return body;
}
}
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 70259973..983996d1 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1920,6 +1920,7 @@ List<Expression/*!*/>/*!*/ decreases) { List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
Attributes attrs = null;
Triggers trigs = null;
+ Expression range = null;
Expression/*!*/ body;
if (la.kind == 101 || la.kind == 102) {
@@ -1940,12 +1941,16 @@ List<Expression/*!*/>/*!*/ decreases) { while (la.kind == 7) {
AttributeOrTrigger(ref attrs, ref trigs);
}
+ if (la.kind == 17) {
+ Get();
+ Expression(out range);
+ }
QSep();
Expression(out body);
if (univ) {
- q = new ForallExpr(x, bvars, body, trigs, attrs);
+ q = new ForallExpr(x, bvars, range, body, trigs, attrs);
} else {
- q = new ExistsExpr(x, bvars, body, trigs, attrs);
+ q = new ExistsExpr(x, bvars, range, body, trigs, attrs);
}
parseVarScope.PopMarker();
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 003a977c..6dcf0020 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -931,14 +931,19 @@ namespace Microsoft.Dafny { wr.Write(" ");
PrintAttributes(e.Attributes);
PrintTriggers(e.Trigs);
+ if (e.Range != null) {
+ wr.Write("| ");
+ PrintExpression(e.Range);
+ wr.Write(" ");
+ }
wr.Write(":: ");
if (0 <= indent) {
int ind = indent + IndentAmount;
wr.WriteLine();
Indent(ind);
- PrintExpression(e.Body, ind);
+ PrintExpression(e.Term, ind);
} else {
- PrintExpression(e.Body);
+ PrintExpression(e.Term);
}
if (parensNeeded) { wr.Write(")"); }
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 6c2f6c38..c7deb42f 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2227,10 +2227,17 @@ namespace Microsoft.Dafny { }
ResolveType(v.tok, v.Type);
}
- ResolveExpression(e.Body, twoState, specContext);
- Contract.Assert(e.Body.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.Body.Type, Type.Bool)) {
- Error(expr, "body of quantifier must be of type bool (instead got {0})", e.Body.Type);
+ if (e.Range != null) {
+ ResolveExpression(e.Range, twoState, specContext);
+ Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Range.Type, Type.Bool)) {
+ Error(expr, "range of quantifier must be of type bool (instead got {0})", e.Range.Type);
+ }
+ }
+ ResolveExpression(e.Term, twoState, specContext);
+ Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Term.Type, Type.Bool)) {
+ Error(expr, "body of quantifier must be of type bool (instead got {0})", e.Term.Type);
}
// Since the body is more likely to infer the types of the bound variables, resolve it
// first (above) and only then resolve the attributes and triggers (below).
@@ -2391,7 +2398,7 @@ namespace Microsoft.Dafny { // Go through the conjuncts of the range expression look for bounds.
Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;
Expression upperBound = null;
- foreach (var conjunct in NormalizedConjuncts(e.Body, e is ExistsExpr)) {
+ foreach (var conjunct in NormalizedConjuncts(e.LogicalBody(), e is ExistsExpr)) {
var c = conjunct as BinaryExpr;
if (c == null) {
goto CHECK_NEXT_CONJUNCT;
@@ -2715,7 +2722,7 @@ namespace Microsoft.Dafny { } else if (expr is QuantifierExpr) {
var e = (QuantifierExpr)expr;
- var s = FreeVariables(e.Body);
+ var s = FreeVariables(e.LogicalBody());
foreach (var bv in e.BoundVars) {
s.Remove(bv);
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 557fcaf0..253a1f9b 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1511,7 +1511,7 @@ namespace Microsoft.Dafny { return z == null ? r : BplAnd(r, z);
} else if (expr is QuantifierExpr) {
QuantifierExpr e = (QuantifierExpr)expr;
- Bpl.Expr total = IsTotal(e.Body, etran);
+ Bpl.Expr total = IsTotal(e.LogicalBody(), etran);
if (total != Bpl.Expr.True) {
Bpl.VariableSeq bvars = new Bpl.VariableSeq();
Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);
@@ -1638,7 +1638,7 @@ namespace Microsoft.Dafny { return BplAnd(t0, t1);
} else if (expr is QuantifierExpr) {
QuantifierExpr e = (QuantifierExpr)expr;
- Bpl.Expr total = CanCallAssumption(e.Body, etran);
+ Bpl.Expr total = CanCallAssumption(e.LogicalBody(), etran);
if (total != Bpl.Expr.True) {
Bpl.VariableSeq bvars = new Bpl.VariableSeq();
Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);
@@ -1986,7 +1986,7 @@ namespace Microsoft.Dafny { builder.Add(new Bpl.AssumeCmd(bv.tok, wh));
}
}
- Expression body = Substitute(e.Body, null, substMap);
+ Expression body = Substitute(e.LogicalBody(), null, substMap);
CheckWellformed(body, options, locals, builder, etran);
} else if (expr is ITEExpr) {
@@ -4415,13 +4415,17 @@ namespace Microsoft.Dafny { }
tr = new Bpl.Trigger(expr.tok, true, tt, tr);
}
- Bpl.Expr body = TrExpr(e.Body);
+ var antecedent = typeAntecedent;
+ if (e.Range != null) {
+ antecedent = Bpl.Expr.And(antecedent, TrExpr(e.Range));
+ }
+ Bpl.Expr body = TrExpr(e.Term);
if (e is ForallExpr) {
- return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.Imp(typeAntecedent, body));
+ return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.Imp(antecedent, body));
} else {
Contract.Assert(e is ExistsExpr);
- return new Bpl.ExistsExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.And(typeAntecedent, body));
+ return new Bpl.ExistsExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.And(antecedent, body));
}
} else if (expr is ITEExpr) {
@@ -5220,7 +5224,7 @@ namespace Microsoft.Dafny { substMap.Add(n, ieK);
}
- Expression bodyK = Substitute(e.Body, null, substMap);
+ Expression bodyK = Substitute(e.LogicalBody(), null, substMap);
Bpl.Expr less = DecreasesCheck(toks, types, kk, nn, etran, null, null, false, true);
@@ -5252,7 +5256,7 @@ namespace Microsoft.Dafny { typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);
foreach (var kase in caseProduct) {
var ante = BplAnd(BplAnd(typeAntecedent, ih), kase);
- var bdy = etran.LayerOffset(1).TrExpr(e.Body);
+ var bdy = etran.LayerOffset(1).TrExpr(e.LogicalBody());
Bpl.Expr q = new Bpl.ForallExpr(kase.tok, bvars, Bpl.Expr.Imp(ante, bdy));
splits.Add(new SplitExprInfo(false, q));
}
@@ -5344,7 +5348,7 @@ namespace Microsoft.Dafny { // consider automatically applying induction
var inductionVariables = new List<BoundVar>();
foreach (var n in e.BoundVars) {
- if (VarOccursInArgumentToRecursiveFunction(e.Body, n, null)) {
+ if (VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {
if (CommandLineOptions.Clo.Trace) {
Console.Write("Applying automatic induction on variable '{0}' of: ", n.Name);
new Printer(Console.Out).PrintExpression(e);
@@ -5447,7 +5451,7 @@ namespace Microsoft.Dafny { VarOccursInArgumentToRecursiveFunction(e.E1, n, p);
} else if (expr is QuantifierExpr) {
var e = (QuantifierExpr)expr;
- return VarOccursInArgumentToRecursiveFunction(e.Body, n, null);
+ return VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null);
} else if (expr is ITEExpr) {
var e = (ITEExpr)expr;
return VarOccursInArgumentToRecursiveFunction(e.Test, n, null) || // test is not "elevated"
@@ -5617,14 +5621,15 @@ namespace Microsoft.Dafny { } else if (expr is QuantifierExpr) {
QuantifierExpr e = (QuantifierExpr)expr;
- Expression newBody = Substitute(e.Body, receiverReplacement, substMap);
+ Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);
+ Expression newTerm = Substitute(e.Term, receiverReplacement, substMap);
Triggers newTrigs = SubstTriggers(e.Trigs, receiverReplacement, substMap);
Attributes newAttrs = SubstAttributes(e.Attributes, receiverReplacement, substMap);
- if (newBody != e.Body || newTrigs != e.Trigs || newAttrs != e.Attributes) {
+ if (newRange != e.Range || newTerm != e.Term || newTrigs != e.Trigs || newAttrs != e.Attributes) {
if (expr is ForallExpr) {
- newExpr = new ForallExpr(expr.tok, e.BoundVars, newBody, newTrigs, newAttrs);
+ newExpr = new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);
} else {
- newExpr = new ExistsExpr(expr.tok, e.BoundVars, newBody, newTrigs, newAttrs);
+ newExpr = new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);
}
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 4bdea760..070aa6be 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -198,8 +198,18 @@ Execution trace: (0,0): anon0
SmallTests.dfy(267,19): anon3_Else
(0,0): anon2
+SmallTests.dfy(307,3): Error BP5003: A postcondition might not hold on this return path.
+SmallTests.dfy(301,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+ (0,0): anon18_Else
+ (0,0): anon11
+ (0,0): anon23_Then
+ (0,0): anon24_Then
+ (0,0): anon15
+ (0,0): anon25_Else
-Dafny program verifier finished with 34 verified, 13 errors
+Dafny program verifier finished with 39 verified, 14 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
@@ -464,14 +474,17 @@ Dafny program verifier finished with 8 verified, 2 errors -------------------- NonGhostQuantifiers.dfy --------------------
NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(57,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
-NonGhostQuantifiers.dfy(61,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(71,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(86,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(94,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
-NonGhostQuantifiers.dfy(103,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
-NonGhostQuantifiers.dfy(120,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-8 resolution/type errors detected in NonGhostQuantifiers.dfy
+NonGhostQuantifiers.dfy(42,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(46,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'
+NonGhostQuantifiers.dfy(50,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(74,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
+NonGhostQuantifiers.dfy(78,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(88,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(103,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(111,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
+NonGhostQuantifiers.dfy(120,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+11 resolution/type errors detected in NonGhostQuantifiers.dfy
-------------------- AdvancedLHS.dfy --------------------
AdvancedLHS.dfy(32,23): Error: target object may be null
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy index ea256a58..58e64827 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy +++ b/Test/dafny0/NonGhostQuantifiers.dfy @@ -33,6 +33,23 @@ class MyClass<T> { (forall n :: 2 <= n ==> 1000 <= n || (exists d :: n < d && d < 2*n))
}
+ function method GoodRange(): bool
+ {
+ (forall n | 2 <= n :: 1000 <= n || (exists d | n < d :: d < 2*n)) && (exists K: nat | K < 100 :: true)
+ }
+ function method BadRangeForall(): bool
+ {
+ forall n | n <= 2 :: 1000 <= n || n % 2 == 0 // error: cannot bound range for n
+ }
+ function method BadRangeExists(): bool
+ {
+ exists d | d < 1000 :: d < 2000 // error: cannot bound range for d
+ }
+ function method WhatAboutThis(): bool
+ {
+ forall n :: 2 <= n && (forall M | M == 1000 :: n < M) ==> n % 2 == 0 // error: heuristics don't get this one for n
+ }
+
// Here are more tests
function method F(a: array<T>): bool
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index a839d5a9..ef2049a3 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -272,3 +272,39 @@ class InitCalls { r := new InitCalls.InitFromReference(r); // error, since r.z is unknown
}
}
+
+// --------------- some tests with quantifiers and ranges ----------------------
+
+method QuantifierRange0<T>(a: seq<T>, x: T, y: T, N: int)
+ requires 0 <= N && N <= |a|;
+ requires forall k | 0 <= k && k < N :: a[k] != x;
+ requires exists k | 0 <= k && k < N :: a[k] == y;
+ ensures forall k :: 0 <= k && k < N ==> a[k] != x; // same as the precondition, but using ==> instead of |
+ ensures exists k :: 0 <= k && k < N && a[k] == y; // same as the precondition, but using && instead of |
+{
+ assert x != y;
+}
+
+method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int)
+ requires 0 <= N && N <= |a|;
+ requires forall k :: 0 <= k && k < N ==> a[k] != x;
+ requires exists k :: 0 <= k && k < N && a[k] == y;
+ ensures forall k | 0 <= k && k < N :: a[k] != x; // same as the precondition, but using | instead of ==>
+ ensures exists k | 0 <= k && k < N :: a[k] == y; // same as the precondition, but using | instead of &&
+{
+ assert x != y;
+}
+
+method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)
+ requires 0 <= N && N <= |a|;
+ requires exists k | 0 <= k && k < N :: a[k] == y;
+ ensures forall k | 0 <= k && k < N :: a[k] == y; // error
+{
+ assert N != 0;
+ if (N == 1) {
+ assert forall k | a[if 0 <= k && k < N then k else 0] != y :: k < 0 || N <= k; // in this case, the precondition holds trivially
+ }
+ if (forall k | 0 <= k && k < N :: a[k] == x) {
+ assert x == y;
+ }
+}
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index d0eba7cb..0111f9af 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -65,7 +65,7 @@ Dafny program verifier finished with 4 verified, 0 errors -------------------- TerminationDemos.dfy --------------------
-Dafny program verifier finished with 11 verified, 0 errors
+Dafny program verifier finished with 14 verified, 0 errors
-------------------- Substitution.dfy --------------------
diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy index 01a7c7bd..49f5a075 100644 --- a/Test/dafny1/TerminationDemos.dfy +++ b/Test/dafny1/TerminationDemos.dfy @@ -42,6 +42,28 @@ class Ackermann { else
G(m - 1, G(m, n - 1))
}
+
+ function H(m: nat, n: nat): nat
+ {
+ if m == 0 then
+ n + 1
+ else if n == 0 then
+ H(m - 1, 1)
+ else
+ H(m - 1, H(m, n - 1))
+ }
+
+ method ComputeAck(m: nat, n: nat) returns (r: nat)
+ {
+ if (m == 0) {
+ r := n + 1;
+ } else if (n == 0) {
+ call r := ComputeAck(m - 1, 1);
+ } else {
+ call s := ComputeAck(m, n - 1);
+ call r := ComputeAck(m - 1, s);
+ }
+ }
}
// -----------------------------------
|