diff --git a/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs b/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs index db914c9c9f6..481f0032b95 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs @@ -1,6 +1,7 @@ using System.Collections.Generic; using System.Diagnostics; using System.Diagnostics.Contracts; +using JetBrains.Annotations; namespace Microsoft.Dafny; @@ -36,7 +37,7 @@ public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expr } /// - /// Map a list of quantified variables to an eqivalent list of bound variables plus a single range expression. + /// Map a list of quantified variables to an equivalent list of bound variables plus a single range expression. /// The transformation looks like this in general: /// /// x1 <- C1 | E1, ..., xN <- CN | EN @@ -48,7 +49,7 @@ public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expr /// Note the result will be null rather than "true" if there are no such domains or ranges. /// Some quantification contexts (such as comprehensions) will replace this with "true". /// - public static void ExtractSingleRange(List qvars, out List bvars, out Expression range) { + public static void ExtractSingleRange(List qvars, out List bvars, [CanBeNull] out Expression range) { bvars = new List(); range = null; diff --git a/Source/DafnyCore/AST/Grammar/ParseErrors.cs b/Source/DafnyCore/AST/Grammar/ParseErrors.cs index 8b59ebc15a9..ecebdd4dbc6 100644 --- a/Source/DafnyCore/AST/Grammar/ParseErrors.cs +++ b/Source/DafnyCore/AST/Grammar/ParseErrors.cs @@ -96,6 +96,7 @@ public enum ErrorId { p_no_decreases_expressions_with_star, p_assert_needs_by_or_semicolon, p_deprecated_forall_with_no_bound_variables, + p_deprecated_forall_statement_with_parentheses_around_bound_variables, p_forall_with_ensures_must_have_body, p_deprecated_modify_statement_with_block, p_calc_operator_must_be_transitive, diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 56eaf176803..24317b57a17 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -3093,36 +3093,45 @@ RevealStmt . /*------------------------------------------------------------------------*/ -ForallStmt +ForallStmt = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); - IToken/*!*/ x = Token.NoToken; List bvars = null; Attributes qattrs = null; Expression range = null; - var ens = new List(); IToken startToken = null; - BlockStmt block = null; - IToken bodyStart, bodyEnd; - IToken tok = Token.NoToken; .) - "forall" (. x = t; tok = x; startToken = t; .) + "forall" (. startToken = t; .) ( IF(la.kind == _openparen) /* disambiguation needed, because of the possibility of a body-less forall statement */ - "(" [ QuantifierDomain ] ")" - | [ IF(IsIdentifier(la.kind)) /* disambiguation needed, because of the possibility of a body-less forall statement */ - QuantifierDomain - ] + "(" (. errors.Deprecated(ErrorId.p_deprecated_forall_statement_with_parentheses_around_bound_variables, t, + "parentheses around the forall-statement bound variables are deprecated and not needed"); + .) + [ QuantifierDomain ] + ")" + | [ IF(IsIdentifier(la.kind)) /* disambiguation needed, because of the possibility of a body-less forall statement */ + QuantifierDomain + ] ) - (. if (bvars == null) errors.Deprecated(ErrorId.p_deprecated_forall_with_no_bound_variables, startToken, "a forall statement with no bound variables is deprecated; use an 'assert by' statement instead"); - if (bvars == null) { bvars = new List(); } - if (range == null) { range = new LiteralExpr(x, true); } + (. if (bvars == null) { + errors.Deprecated(ErrorId.p_deprecated_forall_with_no_bound_variables, startToken, + "a forall statement with no bound variables is deprecated; use an 'assert by' statement instead"); + } + bvars ??= new List(); .) + ForallStatementEnsuresAndBody + . + +ForallStatementEnsuresAndBody<.out Statement s, IToken startToken, List bvars, Attributes qattrs, Expression/*?*/ range.> += (. var ens = new List(); + BlockStmt block = null; + range ??= new LiteralExpr(startToken, true); + .) { EnsuresClause } [ IF(la.kind == _lbrace) /* if the input continues like a block statement, take it to be the body of the forall statement; a body-less forall statement must continue in some other way */ - BlockStmt + BlockStmt ] (. if (theOptions.DisallowSoundnessCheating && block == null && 0 < ens.Count) { SemErr(ErrorId.p_forall_with_ensures_must_have_body, t, "a forall statement with an ensures clause must have a body"); @@ -3996,7 +4005,7 @@ MapComprehensionExpr + QuantifierDomain QSep Expression [ IF(IsGets()) /* greedily parse ":=" */ (. bodyLeft = bodyRight; .) @@ -4021,7 +4030,8 @@ EndlessExpression /* types are such that we can allow bitwise operations in the quantifier body */ | SetComprehensionExpr | StmtInExpr - Expression (. e = new StmtExpr(s.Tok, s, e) { RangeToken = new RangeToken(s.StartToken, e.EndToken) }; .) + Expression + (. e = new StmtExpr(s.Tok, s, e) { RangeToken = new RangeToken(s.StartToken, e.EndToken) }; .) | LetExpression | MapComprehensionExpr ) @@ -4499,20 +4509,30 @@ QuantifierExpression List bvars; Attributes attrs; Expression range; - Expression/*!*/ body; + q = dummyExpr; .) ( Forall (. x = t; univ = true; .) | Exists (. x = t; .) ) - QuantifierDomain - QSep - Expression - (. if (univ) { - q = new ForallExpr(x, new RangeToken(x, t), bvars, range, body, attrs); - } else { - q = new ExistsExpr(x, new RangeToken(x, t), bvars, range, body, attrs); - } - .) + QuantifierDomain + ( IF(univ && (la.kind == _ensures || la.kind == _lbrace)) + // It's a forall statement. Parse it as part of a StmtExpr. + ForallStatementEnsuresAndBody + Expression + (. q = new StmtExpr(forallStatement.Tok, forallStatement, expr) { + RangeToken = new RangeToken(forallStatement.StartToken, forallStatement.EndToken) + }; + .) + + | QSep + Expression + (. if (univ) { + q = new ForallExpr(x, new RangeToken(x, t), bvars, range, body, attrs); + } else { + q = new ExistsExpr(x, new RangeToken(x, t), bvars, range, body, attrs); + } + .) + ) . /*------------------------------------------------------------------------*/ @@ -4586,9 +4606,7 @@ SetComprehensionExpr x / y >= x / z { - forall (x: int, y: int, z: int | 0 <= x && 1 <= y <= z) + forall x: int, y: int, z: int | 0 <= x && 1 <= y <= z ensures x / y >= x / z { LemmaDivIsOrderedByDenominator(x, y, z); @@ -174,7 +174,7 @@ module Std.Arithmetic.DivMod { lemma LemmaDivIsStrictlyOrderedByDenominatorAuto() ensures forall x: int, d: int {:trigger x / d} :: 0 < x && 1 < d ==> x / d < x { - forall (x: int, d: int | 0 < x && 1 < d ) + forall x: int, d: int | 0 < x && 1 < d ensures x / d < x { LemmaDivIsStrictlyOrderedByDenominator(x, d); @@ -205,7 +205,7 @@ module Std.Arithmetic.DivMod { :: 0 < d && R == a%d + b%d - (a+b)%d ==> d*((a+b)/d) - R == d*(a/d) + d*(b/d) { // https://github.com/dafny-lang/dafny/issues/4771 - forall (a: int, b: int, d: int, R: int {:trigger d * ((a + b) / d) - R, d*(a/d) + d*(b/d)} | 0< d && R == a%d + b%d - (a+b)%d) + forall a: int, b: int, d: int, R: int {:trigger d * ((a + b) / d) - R, d*(a/d) + d*(b/d)} | 0< d && R == a%d + b%d - (a+b)%d ensures d*((a+b)/d) - R == d*(a/d) + d*(b/d) { LemmaDividingSums(a, b, d, R); @@ -225,7 +225,7 @@ module Std.Arithmetic.DivMod { lemma LemmaDivPosIsPosAuto() ensures forall x: int, d: int {:trigger x / d} :: 0 <= x && 0 < d ==> 0 <= x / d { - forall (x: int, d: int | 0 <= x && 0 < d) + forall x: int, d: int | 0 <= x && 0 < d ensures 0 <= x / d { LemmaDivPosIsPos(x, d); @@ -244,7 +244,7 @@ module Std.Arithmetic.DivMod { lemma LemmaDivPlusOneAuto() ensures forall x: int, d: int {:trigger 1 + x / d, (d + x) / d} :: 0 < d ==> 1 + x / d == (d + x) / d { - forall (x: int, d: int | 0 < d) + forall x: int, d: int | 0 < d ensures 1 + x / d == (d + x) / d { LemmaDivPlusOne(x, d); @@ -263,7 +263,7 @@ module Std.Arithmetic.DivMod { lemma LemmaDivMinusOneAuto() ensures forall x: int, d: int {:trigger -1 + x / d, (-d + x) / d} :: 0 < d ==> -1 + x / d == (-d + x) / d { - forall (x: int, d: int | 0 < d) + forall x: int, d: int | 0 < d ensures -1 + x / d == (-d + x) / d { LemmaDivMinusOne(x, d); @@ -281,7 +281,7 @@ module Std.Arithmetic.DivMod { lemma LemmaBasicDivAuto() ensures forall x: int, d: int {:trigger x / d} :: 0 <= x < d ==> x / d == 0 { - forall (x: int, d: int | 0 <= x < d) + forall x: int, d: int | 0 <= x < d ensures x / d == 0 { LemmaBasicDiv(d); @@ -300,7 +300,7 @@ module Std.Arithmetic.DivMod { lemma LemmaDivIsOrderedAuto() ensures forall x: int, y: int, z: int {:trigger x / z, y / z} :: x <= y && 0 < z ==> x / z <= y / z { - forall (x: int, y: int, z: int | x <= y && 0 < z) + forall x: int, y: int, z: int | x <= y && 0 < z ensures x / z <= y / z { LemmaDivIsOrdered(x, y, z); @@ -320,7 +320,7 @@ module Std.Arithmetic.DivMod { lemma LemmaDivDecreasesAuto() ensures forall x: int, d: int {:trigger x / d} :: 0 < x && 1 < d ==> x / d < x { - forall (x: int, d: int | 0 < x && 1 < d) + forall x: int, d: int | 0 < x && 1 < d ensures x / d < x { LemmaDivDecreases(x, d); @@ -340,7 +340,7 @@ module Std.Arithmetic.DivMod { lemma LemmaDivNonincreasingAuto() ensures forall x: int, d: int {:trigger x / d } :: 0 <= x && 0 < d ==> x / d <= x { - forall (x: int, d: int | 0 <= x && 0 < d) + forall x: int, d: int | 0 <= x && 0 < d ensures x / d <= x { LemmaDivNonincreasing(x, d); @@ -410,7 +410,7 @@ module Std.Arithmetic.DivMod { ensures forall x: int, y: int, z: int {:trigger y * z, x % (y * z), y * ((x / y) % z) + x % y} :: 0 <= x && 0 < y && 0 < z ==> 0 < y * z && x % (y * z) == y * ((x / y) % z) + x % y { - forall (x: int, y: int, z: int | 0 <= x && 0 < y && 0 < z) + forall x: int, y: int, z: int | 0 <= x && 0 < y && 0 < z ensures 0 < y * z && x % (y * z) == y * ((x / y) % z) + x % y { LemmaBreakdown(x, y, z); @@ -429,7 +429,7 @@ module Std.Arithmetic.DivMod { lemma LemmaRemainderUpperAuto() ensures forall x: int, d: int {:trigger x - d, d * d} :: 0 <= x && 0 < d ==> x - d < x / d * d { - forall (x: int, d: int | 0 <= x && 0 < d) + forall x: int, d: int | 0 <= x && 0 < d ensures x - d < x / d * d { LemmaRemainderUpper(x, d); @@ -628,7 +628,7 @@ module Std.Arithmetic.DivMod { ensures forall x: int, y: int, z: int {:trigger x * (y / z), (x * y) / z} :: 0 <= x && 0 < z ==> x * (y / z) <= (x * y) / z { - forall (x: int, y: int, z: int | 0 <= x && 0 < z) + forall x: int, y: int, z: int | 0 <= x && 0 < z ensures x * (y / z) <= (x * y) / z { LemmaMulHoistInequality(x, y, z); diff --git a/Source/DafnyStandardLibraries/src/Std/Arithmetic/Mul.dfy b/Source/DafnyStandardLibraries/src/Std/Arithmetic/Mul.dfy index 7c599978641..a307f3055ea 100644 --- a/Source/DafnyStandardLibraries/src/Std/Arithmetic/Mul.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Arithmetic/Mul.dfy @@ -87,7 +87,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulNonzeroAuto() ensures forall x: int, y: int {:trigger x * y} :: x * y != 0 <==> x != 0 && y != 0 { - forall (x: int, y: int) + forall x: int, y: int ensures x * y != 0 <==> x != 0 && y != 0 { LemmaMulNonzero(x, y); @@ -117,7 +117,7 @@ module Std.Arithmetic.Mul { ensures forall x: int, y: int, z: int {:trigger x * (y * z)} {:trigger (x * y) * z} :: x * (y * z) == (x * y) * z { - forall (x: int, y: int, z: int) + forall x: int, y: int, z: int ensures x * (y * z) == (x * y) * z { LemmaMulIsAssociative(x, y, z); @@ -166,7 +166,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulEqualityAuto() ensures forall x: int, y: int, z: int {:trigger x * z, y * z } :: x == y ==> x * z == y * z { - forall (x: int, y: int, z: int | x == y) + forall x: int, y: int, z: int | x == y ensures x * z == y * z { LemmaMulEquality(x, y, z); @@ -186,7 +186,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulInequalityAuto() ensures forall x: int, y: int, z: int {:trigger x * z, y * z} :: x <= y && z >= 0 ==> x * z <= y * z { - forall (x: int, y: int, z: int | x <= y && z >= 0) + forall x: int, y: int, z: int | x <= y && z >= 0 ensures x * z <= y * z { LemmaMulInequality(x, y, z); @@ -206,7 +206,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulStrictInequalityAuto() ensures forall x: int, y: int, z: int {:trigger x * z, y * z} :: x < y && z > 0 ==> x * z < y * z { - forall (x: int, y: int, z: int | x < y && z > 0) + forall x: int, y: int, z: int | x < y && z > 0 ensures x * z < y * z { LemmaMulStrictInequality(x, y, z); @@ -229,7 +229,7 @@ module Std.Arithmetic.Mul { ensures forall x: int, XBound: int, y: int, YBound: int {:trigger x * y, XBound * YBound} :: x <= XBound && y <= YBound && 0 <= x && 0 <= y ==> x * y <= XBound * YBound { - forall (x: int, XBound: int, y: int, YBound: int | x <= XBound && y <= YBound && 0 <= x && 0 <= y) + forall x: int, XBound: int, y: int, YBound: int | x <= XBound && y <= YBound && 0 <= x && 0 <= y ensures x * y <= XBound * YBound { LemmaMulUpperBound(x, XBound, y, YBound); @@ -252,14 +252,14 @@ module Std.Arithmetic.Mul { ensures forall x: int, XBound: int, y: int, YBound: int {:trigger x * y, (XBound - 1) * (YBound - 1)} :: x < XBound && y < YBound && 0 < x && 0 < y ==> x * y <= (XBound - 1) * (YBound - 1) { - forall (x: int, XBound: int, y: int, YBound: int + forall x: int, XBound: int, y: int, YBound: int // https://github.com/dafny-lang/dafny/issues/4771 {:trigger (XBound - 1) * (YBound - 1), x * y} {:trigger YBound - 1, XBound - 1, 0 < y, 0 < x} {:trigger YBound - 1, 0 < y, x < XBound} {:trigger XBound - 1, 0 < x, y < YBound} {:trigger y < YBound, x < XBound} - | x < XBound && y < YBound && 0 < x && 0 < y) + | x < XBound && y < YBound && 0 < x && 0 < y ensures x * y <= (XBound - 1) * (YBound - 1) { LemmaMulStrictUpperBound(x, XBound, y, YBound); @@ -280,7 +280,7 @@ module Std.Arithmetic.Mul { ensures forall x: int, y: int, z: int {:trigger x * y, x * z} :: x > 0 ==> (y <= z ==> x * y <= x * z) && (y < z ==> x * y < x * z) { - forall (x: int, y: int, z: int | (y <= z || y < z) && 0 < x) + forall x: int, y: int, z: int | (y <= z || y < z) && 0 < x ensures (y <= z ==> x * y <= x * z) && (y < z ==> x * y < x * z) { LemmaMulLeftInequality(x, y, z); @@ -305,7 +305,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulEqualityConverseAuto() ensures forall m: int, x: int, y: int {:trigger m * x, m * y} :: (m != 0 && m * x == m * y) ==> x == y { - forall (m: int, x: int, y: int | m != 0 && m * x == m * y) + forall m: int, x: int, y: int | m != 0 && m * x == m * y ensures x == y { LemmaMulEqualityConverse(m, x, y); @@ -326,7 +326,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulInequalityConverseAuto() ensures forall x: int, y: int, z: int {:trigger x * z, y * z} :: x * z <= y * z && z > 0 ==> x <= y { - forall (x: int, y: int, z: int | x * z <= y * z && z > 0) + forall x: int, y: int, z: int | x * z <= y * z && z > 0 ensures x <= y { LemmaMulInequalityConverse(x, y, z); @@ -347,7 +347,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulStrictInequalityConverseAuto() ensures forall x: int, y: int, z: int {:trigger x * z, y * z} :: x * z < y * z && z >= 0 ==> x < y { - forall (x: int, y: int, z: int | x * z < y * z && z >= 0) + forall x: int, y: int, z: int | x * z < y * z && z >= 0 ensures x < y { LemmaMulStrictInequalityConverse(x, y, z); @@ -365,7 +365,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulIsDistributiveAddAuto() ensures forall x: int, y: int, z: int {:trigger x * (y + z)} :: x * (y + z) == x * y + x * z { - forall (x: int, y: int, z: int) + forall x: int, y: int, z: int ensures x * (y + z) == x * y + x * z { LemmaMulIsDistributiveAdd(x, y, z); @@ -382,7 +382,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulIsDistributiveAddOtherWayAuto() ensures forall x: int, y: int, z: int {:trigger (y + z) * x} :: (y + z) * x == y * x + z * x { - forall (x: int, y: int, z: int) + forall x: int, y: int, z: int ensures (y+z) * x == y * x + z * x { LemmaMulIsDistributiveAddOtherWay(x, y, z); @@ -400,7 +400,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulIsDistributiveSubAuto() ensures forall x: int, y: int, z: int {:trigger x * (y - z)} :: x * (y - z) == x * y - x * z { - forall (x: int, y: int, z: int) + forall x: int, y: int, z: int ensures x * (y - z) == x * y - x * z { LemmaMulIsDistributiveSub(x, y, z); @@ -444,7 +444,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulStrictlyPositiveAuto() ensures forall x: int, y: int {:trigger x * y} :: (0 < x && 0 < y) ==> (0 < x * y) { - forall (x: int, y: int | 0 < x && 0 < y) + forall x: int, y: int | 0 < x && 0 < y ensures 0 < x * y { LemmaMulStrictlyPositive(x,y); @@ -466,7 +466,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulStrictlyIncreasesAuto() ensures forall x: int, y: int {:trigger x * y} :: 1 < x && 0 < y ==> y < x * y { - forall (x: int, y: int | 1 < x && 0 < y) + forall x: int, y: int | 1 < x && 0 < y ensures y < x * y { LemmaMulStrictlyIncreases(x, y); @@ -488,7 +488,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulIncreasesAuto() ensures forall x: int, y: int {:trigger x * y} :: (0 < x && 0 < y) ==> (y <= x * y) { - forall (x: int, y: int | 0 < x && 0 < y) + forall x: int, y: int | 0 < x && 0 < y ensures y <= x * y { LemmaMulIncreases(x, y); @@ -508,7 +508,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulNonnegativeAuto() ensures forall x: int, y: int {:trigger x * y} :: 0 <= x && 0 <= y ==> 0 <= x * y { - forall (x: int, y: int | 0 <= x && 0 <= y) + forall x: int, y: int | 0 <= x && 0 <= y ensures 0 <= x * y { LemmaMulNonnegative(x, y); @@ -526,7 +526,7 @@ module Std.Arithmetic.Mul { lemma LemmaMulUnaryNegationAuto() ensures forall x: int, y: int {:trigger (-x) * y} {:trigger x * (-y)} :: (-x) * y == -(x * y) == x * (-y) { - forall (x: int, y: int) + forall x: int, y: int ensures (-x) * y == -(x * y) == x * (-y) { LemmaMulUnaryNegation(x, y); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ConsistentBuilds.legacy.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ConsistentBuilds.legacy.dfy index cbc42e19353..e94ea5f4e61 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ConsistentBuilds.legacy.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ConsistentBuilds.legacy.dfy @@ -82,7 +82,7 @@ lemma UpdateCLemma(cmd: Expression, deps: Expression, exts: Expression, stC: Sta var exts' := exprLiteral(litArrOfStrings(strs - {e})); // note: This assertion is necessary. assert stC' == UpdateC(cmd, deps, exts', S(stC.st, c')); - forall (cmd', deps', e' | Hash(Loc(cmd', deps', e')) == Hash(Loc(cmd, deps, e))) { + forall cmd', deps', e' | Hash(Loc(cmd', deps', e')) == Hash(Loc(cmd, deps, e)) { HashProperty(cmd', deps', e', cmd, deps, e); } } @@ -612,7 +612,7 @@ lemma {:induction expr} EvalCLemma(expr: Expression, stC: StateC, env: Env) var stExecC := resultExec.snd; // note: This assertion is necessary. assert DomSt(stC'.st) <= DomSt(stCombinedC.st); - forall (p | p in DomSt(stCombinedC.st) && p in DomSt(stExecC.st)) + forall p | p in DomSt(stCombinedC.st) && p in DomSt(stExecC.st) ensures GetSt(p, stCombinedC.st) == GetSt(p, stExecC.st) { assert DomSt(stCombinedC.st) <= DomSt(stExecC.st); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Deprecation.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Deprecation.dfy index b45668c76c6..9637ae77669 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Deprecation.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Deprecation.dfy @@ -31,3 +31,59 @@ inductive lemma InductiveLemma() // deprecation warning: "inductive lemma" has colemma CoLemma() // deprecation warning: "colemma" has been renamed to "greatest lemma" { } +// ------- empty forall statement and forall statement with parentheses ----------------------------------------- + +class EmptyForallStatement { + var data: int + + ghost predicate P(x: int) + + lemma EstablishP(x: int) + ensures P(x) + + method EmptyForall0() + modifies this + ensures data == 8 + { + forall () { // warning (x2): forall statement with no bound variables, and forall statement with parentheses + this.data := 8; + } + } + + method EmptyForall1() + ensures P(8) + { + forall { // warning: forall statement with no bound variables + EstablishP(8); + } + } + + method EmptyForall2(s: set) + ensures forall x :: x in s ==> P(x.data) + { + forall (x | x in s) { // warning: forall statement with parentheses + EstablishP(x.data); + } + } + + method EmptyForall3(s: set) + ensures forall x <- s :: P(x.data) + { + forall (x <- s) // warning: forall statement with parentheses + ensures P(x.data) + { + EstablishP(x.data); + } + } + + method EmptyForall4() + { + forall // warning: forall statement with no bound variables + ensures exists k :: P(k) + { + var y := 8; + assume P(y); + } + assert exists k :: P(k); // yes + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Deprecation.dfy.verifier.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Deprecation.dfy.verifier.expect index c0851e9888c..3216510dd40 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Deprecation.dfy.verifier.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Deprecation.dfy.verifier.expect @@ -3,3 +3,9 @@ Deprecation.dfy(22,0): Warning: the old keyword phrase 'inductive predicate' has Deprecation.dfy(25,0): Warning: the old keyword 'copredicate' has been renamed to the keyword phrase 'greatest predicate' Deprecation.dfy(28,0): Warning: the old keyword phrase 'inductive lemma' has been renamed to 'least lemma' Deprecation.dfy(31,0): Warning: the old keyword 'colemma' has been renamed to the keyword phrase 'greatest lemma' +Deprecation.dfy(48,11): Warning: parentheses around the forall-statement bound variables are deprecated and not needed +Deprecation.dfy(48,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead +Deprecation.dfy(56,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead +Deprecation.dfy(64,11): Warning: parentheses around the forall-statement bound variables are deprecated and not needed +Deprecation.dfy(72,11): Warning: parentheses around the forall-statement bound variables are deprecated and not needed +Deprecation.dfy(81,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy similarity index 90% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy index bb45f97a50e..4fdf67393f1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy @@ -255,45 +255,6 @@ method TwoState_Main3() assert false; // it is known that the forall's postcondition is contradictory, so this assert is fine } -// ------- empty forall statement ----------------------------------------- - -class EmptyForallStatement { - var emptyPar: int - - method Empty_Parallel0() - modifies this - ensures emptyPar == 8 - { - forall () { - this.emptyPar := 8; - } - } - - ghost function EmptyPar_P(x: int): bool - lemma EmptyPar_Lemma(x: int) - ensures EmptyPar_P(x) - - method Empty_Parallel1() - ensures EmptyPar_P(8) - { - forall { - EmptyPar_Lemma(8); - } - } - - method Empty_Parallel2() - { - forall - ensures exists k :: EmptyPar_P(k) - { - var y := 8; - assume EmptyPar_P(y); - } - assert exists k :: EmptyPar_P(k); // yes - assert EmptyPar_P(8); // error: the forall statement's ensures clause does not promise this - } -} - // --------------------------------------------------------------------- // The following is an example that once didn't verify (because the forall statement that // induction inserts had caused the $Heap to be advanced, despite the fact that Th is a diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy.expect new file mode 100644 index 00000000000..f31e392521b --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy.expect @@ -0,0 +1,13 @@ +ForallStmt.dfy(33,9): Error: a precondition for this call could not be proved +ForallStmt.dfy(59,13): Related location: this is the precondition that could not be proved +ForallStmt.dfy(37,4): Error: target object might be null +ForallStmt.dfy(41,17): Error: possible violation of postcondition of forall statement +ForallStmt.dfy(46,18): Error: assertion might not hold +ForallStmt.dfy(91,18): Error: assertion might not hold +ForallStmt.dfy(97,19): Error: possible violation of postcondition of forall statement +ForallStmt.dfy(119,11): Error: value does not satisfy the subset constraints of 'nat' +ForallStmt.dfy(182,11): Error: left-hand sides for different forall-statement bound variables might refer to the same location (and right-hand sides might not be equivalent) +ForallStmt.dfy(303,9): Error: assertion might not hold +ForallStmt.dfy(290,32): Related location: this proposition could not be proved + +Dafny program verifier finished with 17 verified, 9 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParallelResolveErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmtResolveErrors.dfy similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParallelResolveErrors.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmtResolveErrors.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmtResolveErrors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmtResolveErrors.dfy.expect new file mode 100644 index 00000000000..1362eed332a --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmtResolveErrors.dfy.expect @@ -0,0 +1,55 @@ +ForallStmtResolveErrors.dfy(210,15): Warning: the modify statement with a block statement is deprecated +ForallStmtResolveErrors.dfy(247,7): Warning: the ... refinement feature in statements is deprecated +ForallStmtResolveErrors.dfy(248,10): Warning: the ... refinement feature in statements is deprecated +ForallStmtResolveErrors.dfy(249,13): Warning: the ... refinement feature in statements is deprecated +ForallStmtResolveErrors.dfy(249,17): Warning: the modify statement with a block statement is deprecated +ForallStmtResolveErrors.dfy(256,9): Warning: the ... refinement feature in statements is deprecated +ForallStmtResolveErrors.dfy(263,7): Warning: the ... refinement feature in statements is deprecated +ForallStmtResolveErrors.dfy(264,10): Warning: the ... refinement feature in statements is deprecated +ForallStmtResolveErrors.dfy(265,15): Warning: the modify statement with a block statement is deprecated +ForallStmtResolveErrors.dfy(272,9): Warning: the ... refinement feature in statements is deprecated +ForallStmtResolveErrors.dfy(279,7): Warning: the ... refinement feature in statements is deprecated +ForallStmtResolveErrors.dfy(280,10): Warning: the ... refinement feature in statements is deprecated +ForallStmtResolveErrors.dfy(281,13): Warning: the ... refinement feature in statements is deprecated +ForallStmtResolveErrors.dfy(281,17): Warning: the modify statement with a block statement is deprecated +ForallStmtResolveErrors.dfy(288,9): Warning: the ... refinement feature in statements is deprecated +ForallStmtResolveErrors.dfy(26,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ForallStmtResolveErrors.dfy(8,6): Error: a forall statement is not allowed to update a variable it doesn't declare +ForallStmtResolveErrors.dfy(25,6): Error: a forall statement is not allowed to update a variable it doesn't declare +ForallStmtResolveErrors.dfy(26,6): Error: a forall statement is not allowed to update a variable it doesn't declare +ForallStmtResolveErrors.dfy(36,6): Error: LHS of assignment must denote a mutable variable +ForallStmtResolveErrors.dfy(48,15): Error: new allocation not supported in aggregate assignments +ForallStmtResolveErrors.dfy(55,19): Error: a non-labeled 'break' statement is allowed only in loops +ForallStmtResolveErrors.dfy(62,21): Error: a non-labeled 'break' statement is allowed only in loops +ForallStmtResolveErrors.dfy(63,20): Error: a 'break break' statement is allowed only in loops +ForallStmtResolveErrors.dfy(64,26): Error: break label is undefined or not in scope: OutsideLoop +ForallStmtResolveErrors.dfy(73,24): Error: a 'break break' statement is allowed only in contexts with 2 enclosing loops, but the current context only has 1 +ForallStmtResolveErrors.dfy(74,30): Error: break label is undefined or not in scope: OutsideLoop +ForallStmtResolveErrors.dfy(85,26): Error: a 'break break' statement is allowed only in contexts with 2 enclosing loops, but the current context only has 1 +ForallStmtResolveErrors.dfy(86,32): Error: break label is undefined or not in scope: WhileOutsideForall +ForallStmtResolveErrors.dfy(129,15): Error: a forall statement is not allowed to use 'new' +ForallStmtResolveErrors.dfy(130,15): Error: a forall statement is not allowed to use 'new' +ForallStmtResolveErrors.dfy(130,21): Error: in a forall statement, calls are allowed only to lemmas +ForallStmtResolveErrors.dfy(131,15): Error: a forall statement is not allowed to use 'new' +ForallStmtResolveErrors.dfy(131,21): Error: in a forall statement, calls are allowed only to lemmas +ForallStmtResolveErrors.dfy(132,15): Error: a forall statement is not allowed to use 'new' +ForallStmtResolveErrors.dfy(132,21): Error: in a forall statement, calls are allowed only to lemmas +ForallStmtResolveErrors.dfy(133,24): Error: in a forall statement, calls are allowed only to lemmas +ForallStmtResolveErrors.dfy(134,22): Error: in a forall statement, calls are allowed only to lemmas +ForallStmtResolveErrors.dfy(143,7): Error: cannot assign to array element in a ghost context +ForallStmtResolveErrors.dfy(149,31): Error: in a forall statement, calls are allowed only to lemmas +ForallStmtResolveErrors.dfy(154,31): Error: in a forall statement, calls are allowed only to lemmas +ForallStmtResolveErrors.dfy(162,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ForallStmtResolveErrors.dfy(105,11): Error: assignment to non-ghost field is not allowed in this context, because this is a ghost method +ForallStmtResolveErrors.dfy(178,12): Error: in a forall statement, calls are allowed only to lemmas +ForallStmtResolveErrors.dfy(174,6): Error: a forall statement is not allowed to update a variable it doesn't declare +ForallStmtResolveErrors.dfy(176,6): Error: a forall statement is not allowed to update a variable it doesn't declare +ForallStmtResolveErrors.dfy(178,6): Error: a forall statement is not allowed to update a variable it doesn't declare +ForallStmtResolveErrors.dfy(190,18): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) +ForallStmtResolveErrors.dfy(251,10): Error: break statement in skeleton is not allowed to break outside the skeleton fragment +ForallStmtResolveErrors.dfy(253,10): Error: break statement in skeleton is not allowed to break outside the skeleton fragment +ForallStmtResolveErrors.dfy(267,10): Error: break statement in skeleton is not allowed to break outside the skeleton fragment +ForallStmtResolveErrors.dfy(269,10): Error: break statement in skeleton is not allowed to break outside the skeleton fragment +ForallStmtResolveErrors.dfy(283,10): Error: continue statement in skeleton is not allowed to break outside the skeleton fragment +ForallStmtResolveErrors.dfy(285,10): Error: continue statement in skeleton is not allowed to break outside the skeleton fragment +39 resolution/type errors detected in ForallStmtResolveErrors.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect deleted file mode 100644 index 2025fe08040..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect +++ /dev/null @@ -1,17 +0,0 @@ -Parallel.dfy(267,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead -Parallel.dfy(279,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead -Parallel.dfy(286,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead -Parallel.dfy(33,9): Error: a precondition for this call could not be proved -Parallel.dfy(59,13): Related location: this is the precondition that could not be proved -Parallel.dfy(37,4): Error: target object might be null -Parallel.dfy(41,17): Error: possible violation of postcondition of forall statement -Parallel.dfy(46,18): Error: assertion might not hold -Parallel.dfy(91,18): Error: assertion might not hold -Parallel.dfy(97,19): Error: possible violation of postcondition of forall statement -Parallel.dfy(119,11): Error: value does not satisfy the subset constraints of 'nat' -Parallel.dfy(182,11): Error: left-hand sides for different forall-statement bound variables might refer to the same location (and right-hand sides might not be equivalent) -Parallel.dfy(293,21): Error: assertion might not hold -Parallel.dfy(342,9): Error: assertion might not hold -Parallel.dfy(329,32): Related location: this proposition could not be proved - -Dafny program verifier finished with 19 verified, 10 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParallelResolveErrors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParallelResolveErrors.dfy.expect deleted file mode 100644 index eee0d123d2c..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParallelResolveErrors.dfy.expect +++ /dev/null @@ -1,55 +0,0 @@ -ParallelResolveErrors.dfy(210,15): Warning: the modify statement with a block statement is deprecated -ParallelResolveErrors.dfy(247,7): Warning: the ... refinement feature in statements is deprecated -ParallelResolveErrors.dfy(248,10): Warning: the ... refinement feature in statements is deprecated -ParallelResolveErrors.dfy(249,13): Warning: the ... refinement feature in statements is deprecated -ParallelResolveErrors.dfy(249,17): Warning: the modify statement with a block statement is deprecated -ParallelResolveErrors.dfy(256,9): Warning: the ... refinement feature in statements is deprecated -ParallelResolveErrors.dfy(263,7): Warning: the ... refinement feature in statements is deprecated -ParallelResolveErrors.dfy(264,10): Warning: the ... refinement feature in statements is deprecated -ParallelResolveErrors.dfy(265,15): Warning: the modify statement with a block statement is deprecated -ParallelResolveErrors.dfy(272,9): Warning: the ... refinement feature in statements is deprecated -ParallelResolveErrors.dfy(279,7): Warning: the ... refinement feature in statements is deprecated -ParallelResolveErrors.dfy(280,10): Warning: the ... refinement feature in statements is deprecated -ParallelResolveErrors.dfy(281,13): Warning: the ... refinement feature in statements is deprecated -ParallelResolveErrors.dfy(281,17): Warning: the modify statement with a block statement is deprecated -ParallelResolveErrors.dfy(288,9): Warning: the ... refinement feature in statements is deprecated -ParallelResolveErrors.dfy(26,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression -ParallelResolveErrors.dfy(8,6): Error: a forall statement is not allowed to update a variable it doesn't declare -ParallelResolveErrors.dfy(25,6): Error: a forall statement is not allowed to update a variable it doesn't declare -ParallelResolveErrors.dfy(26,6): Error: a forall statement is not allowed to update a variable it doesn't declare -ParallelResolveErrors.dfy(36,6): Error: LHS of assignment must denote a mutable variable -ParallelResolveErrors.dfy(48,15): Error: new allocation not supported in aggregate assignments -ParallelResolveErrors.dfy(55,19): Error: a non-labeled 'break' statement is allowed only in loops -ParallelResolveErrors.dfy(62,21): Error: a non-labeled 'break' statement is allowed only in loops -ParallelResolveErrors.dfy(63,20): Error: a 'break break' statement is allowed only in loops -ParallelResolveErrors.dfy(64,26): Error: break label is undefined or not in scope: OutsideLoop -ParallelResolveErrors.dfy(73,24): Error: a 'break break' statement is allowed only in contexts with 2 enclosing loops, but the current context only has 1 -ParallelResolveErrors.dfy(74,30): Error: break label is undefined or not in scope: OutsideLoop -ParallelResolveErrors.dfy(85,26): Error: a 'break break' statement is allowed only in contexts with 2 enclosing loops, but the current context only has 1 -ParallelResolveErrors.dfy(86,32): Error: break label is undefined or not in scope: WhileOutsideForall -ParallelResolveErrors.dfy(129,15): Error: a forall statement is not allowed to use 'new' -ParallelResolveErrors.dfy(130,15): Error: a forall statement is not allowed to use 'new' -ParallelResolveErrors.dfy(130,21): Error: in a forall statement, calls are allowed only to lemmas -ParallelResolveErrors.dfy(131,15): Error: a forall statement is not allowed to use 'new' -ParallelResolveErrors.dfy(131,21): Error: in a forall statement, calls are allowed only to lemmas -ParallelResolveErrors.dfy(132,15): Error: a forall statement is not allowed to use 'new' -ParallelResolveErrors.dfy(132,21): Error: in a forall statement, calls are allowed only to lemmas -ParallelResolveErrors.dfy(133,24): Error: in a forall statement, calls are allowed only to lemmas -ParallelResolveErrors.dfy(134,22): Error: in a forall statement, calls are allowed only to lemmas -ParallelResolveErrors.dfy(143,7): Error: cannot assign to array element in a ghost context -ParallelResolveErrors.dfy(149,31): Error: in a forall statement, calls are allowed only to lemmas -ParallelResolveErrors.dfy(154,31): Error: in a forall statement, calls are allowed only to lemmas -ParallelResolveErrors.dfy(162,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ParallelResolveErrors.dfy(105,11): Error: assignment to non-ghost field is not allowed in this context, because this is a ghost method -ParallelResolveErrors.dfy(178,12): Error: in a forall statement, calls are allowed only to lemmas -ParallelResolveErrors.dfy(174,6): Error: a forall statement is not allowed to update a variable it doesn't declare -ParallelResolveErrors.dfy(176,6): Error: a forall statement is not allowed to update a variable it doesn't declare -ParallelResolveErrors.dfy(178,6): Error: a forall statement is not allowed to update a variable it doesn't declare -ParallelResolveErrors.dfy(190,18): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) -ParallelResolveErrors.dfy(251,10): Error: break statement in skeleton is not allowed to break outside the skeleton fragment -ParallelResolveErrors.dfy(253,10): Error: break statement in skeleton is not allowed to break outside the skeleton fragment -ParallelResolveErrors.dfy(267,10): Error: break statement in skeleton is not allowed to break outside the skeleton fragment -ParallelResolveErrors.dfy(269,10): Error: break statement in skeleton is not allowed to break outside the skeleton fragment -ParallelResolveErrors.dfy(283,10): Error: continue statement in skeleton is not allowed to break outside the skeleton fragment -ParallelResolveErrors.dfy(285,10): Error: continue statement in skeleton is not allowed to break outside the skeleton fragment -39 resolution/type errors detected in ParallelResolveErrors.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/StatementExpressions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/StatementExpressions.dfy index f7e3bd77e69..ef02e5c9a54 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/StatementExpressions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/StatementExpressions.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 4 %verify --relax-definite-assignment "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %testDafnyForEachResolver --expect-exit-code 4 "%s" + lemma M(n: nat) //returns (y: nat) { @@ -20,7 +20,7 @@ lemma MM(n: nat) returns (y: nat) { if n != 0 { y := FF(n-1); - } + } else { y := *; } } ghost function FF(n: nat): nat decreases n, 1 @@ -92,9 +92,9 @@ ghost function F_PreconditionViolation(n: int): int // --------------------- These had had parsing problems in the past lemma MyLemma(x: int) { - var d: Dtz; + var d: Dtz := *; if 0 < x { - var y: int; + var y: int := *; match MyLemma(y); d { // error: cannot prove termination case Cons0(_) => case Cons1(_) => @@ -159,3 +159,96 @@ ghost function Parsing_Regression_test2(): int 17 ) ) ) ) ) ) ) } + +function PartialToTheDiagonal(x: int, y: int): int + requires x == y +{ + 5 +} + +opaque function GimmieSeven(i: int): int { 7 } +lemma AboutGimmieSeven(i: int) + ensures GimmieSeven(i) == 7 +{ + reveal GimmieSeven(); +} + +function TestForallStatement0(a: int, b: int): int +{ + PartialToTheDiagonal(GimmieSeven(a), GimmieSeven(b)) // error: precondition violation +} + +function TestForallStatement1(a: int, b: int): int +{ + reveal GimmieSeven(); + PartialToTheDiagonal(GimmieSeven(a), GimmieSeven(b)) +} + +function TestForallStatement2(a: int, b: int): int +{ + AboutGimmieSeven(a); + AboutGimmieSeven(b); + PartialToTheDiagonal(GimmieSeven(a), GimmieSeven(b)) +} + +function TestForallStatement3(a: int, b: int): int +{ + assert GimmieSeven(a) == GimmieSeven(b) by { + forall i + ensures GimmieSeven(i) == 7 + { + AboutGimmieSeven(i); + } + } + PartialToTheDiagonal(GimmieSeven(a), GimmieSeven(b)) +} + +function TestForallStatement4(a: int, b: int): int +{ + assert forall i :: GimmieSeven(i) == 7 by { + forall i + ensures GimmieSeven(i) == 7 + { + AboutGimmieSeven(i); + } + } + PartialToTheDiagonal(GimmieSeven(a), GimmieSeven(b)) +} + +function TestForallStatement5(a: int, b: int): int +{ + forall i + ensures GimmieSeven(i) == 7 + { + AboutGimmieSeven(i); + } + PartialToTheDiagonal(GimmieSeven(a), GimmieSeven(b)) +} + +function TestForallStatement6(a: int, b: int): int +{ + forall i { + AboutGimmieSeven(i); + } + PartialToTheDiagonal(GimmieSeven(a), GimmieSeven(b)) +} + +function TestForallStatement7(a: int, b: int): int + requires 0 <= a && 0 <= b +{ + forall i | 0 <= i + ensures GimmieSeven(i) == 7 + { + AboutGimmieSeven(i); + } + PartialToTheDiagonal(GimmieSeven(a), GimmieSeven(b)) +} + +function TestForallStatement8(a: int, b: int): int + requires 0 <= a && 0 <= b +{ + forall i | 0 <= i { + AboutGimmieSeven(i); + } + PartialToTheDiagonal(GimmieSeven(a), GimmieSeven(b)) +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/StatementExpressions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/StatementExpressions.dfy.expect index 20f1e76303c..86fcea13980 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/StatementExpressions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/StatementExpressions.dfy.expect @@ -3,5 +3,7 @@ StatementExpressions.dfy(59,13): Error: assertion might not hold StatementExpressions.dfy(77,5): Error: possible division by zero StatementExpressions.dfy(88,4): Error: value does not satisfy the subset constraints of 'nat' StatementExpressions.dfy(98,17): Error: cannot prove termination; try supplying a decreases clause +StatementExpressions.dfy(178,2): Error: function precondition could not be proved +StatementExpressions.dfy(164,13): Related location: this proposition could not be proved -Dafny program verifier finished with 11 verified, 5 errors +Dafny program verifier finished with 20 verified, 6 errors diff --git a/docs/DafnyRef/GrammarDetails.md b/docs/DafnyRef/GrammarDetails.md index af6ed32b078..ce00966a00f 100644 --- a/docs/DafnyRef/GrammarDetails.md +++ b/docs/DafnyRef/GrammarDetails.md @@ -1631,7 +1631,7 @@ MapComprehensionExpr(allowLemma, allowLambda) = ````grammar StmtInExpr = ( AssertStmt | AssumeStmt | ExpectStmt - | RevealStmt | CalcStmt + | RevealStmt | CalcStmt | ForallStmt ) ```` diff --git a/docs/dev/news/5894.feat b/docs/dev/news/5894.feat new file mode 100644 index 00000000000..9fe2145a7d4 --- /dev/null +++ b/docs/dev/news/5894.feat @@ -0,0 +1 @@ +Allow forall statements in statement expressions