From 31f21367f901b990a9d4940ec81fc6ec3c38e492 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 3 Nov 2024 16:51:16 -0800 Subject: [PATCH 01/11] Improve code and comments --- Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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; From 414c4c1c85fd0f9ab3139067a44041f094310779 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 3 Nov 2024 16:51:37 -0800 Subject: [PATCH 02/11] Make test run with both resolvers --- .../LitTests/LitTest/dafny0/StatementExpressions.dfy | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/StatementExpressions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/StatementExpressions.dfy index f7e3bd77e69..8b2bf852c9e 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(_) => From 6f97e14be0008771f79b2233c52b4449c42d7785 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 3 Nov 2024 17:13:05 -0800 Subject: [PATCH 03/11] Allow forall statements in statement expressions --- Source/DafnyCore/AST/Grammar/ParseErrors.cs | 1 + Source/DafnyCore/Dafny.atg | 76 +++++++++------ .../LitTest/dafny0/StatementExpressions.dfy | 93 +++++++++++++++++++ .../dafny0/StatementExpressions.dfy.expect | 4 +- 4 files changed, 143 insertions(+), 31 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/ParseErrors.cs b/Source/DafnyCore/AST/Grammar/ParseErrors.cs index 898e1161766..2ae6be27380 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 c8b2ba37b60..3b7c96f587e 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -3091,36 +3091,43 @@ 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 - ] + "(" + [ 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"); @@ -3978,7 +3985,7 @@ MapComprehensionExpr + QuantifierDomain QSep Expression [ IF(IsGets()) /* greedily parse ":=" */ (. bodyLeft = bodyRight; .) @@ -4003,7 +4010,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 ) @@ -4481,20 +4489,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); + } + .) + ) . /*------------------------------------------------------------------------*/ @@ -4568,9 +4586,7 @@ SetComprehensionExpr Date: Sun, 3 Nov 2024 17:13:29 -0800 Subject: [PATCH 04/11] Deprecate forall statements with parenthesized bound variables --- Source/DafnyCore/Dafny.atg | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 3b7c96f587e..13a78795685 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -3101,7 +3101,9 @@ ForallStmt "forall" (. startToken = t; .) ( IF(la.kind == _openparen) /* disambiguation needed, because of the possibility of a body-less forall statement */ - "(" + "(" (. errors.Deprecated(ErrorId.p_deprecated_forall_statement_with_parentheses_around_bound_variables, t, + "a forall statement with no bound variables is deprecated; use an 'assert by' statement instead"); + .) [ QuantifierDomain ] ")" | [ IF(IsIdentifier(la.kind)) /* disambiguation needed, because of the possibility of a body-less forall statement */ From 2921cd4e68fa8ea1215d722e188213018d6e38f2 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 3 Nov 2024 17:25:17 -0800 Subject: [PATCH 05/11] Update documentation --- docs/DafnyRef/GrammarDetails.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 ) ```` From fd7ea466e55019a25e5bba1b13b79924e275970b Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 3 Nov 2024 17:32:11 -0800 Subject: [PATCH 06/11] Add release notes --- docs/dev/news/5894.feat | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/5894.feat 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 From ace95abd472816f864082669c72babe8428ee21c Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 3 Nov 2024 18:12:31 -0800 Subject: [PATCH 07/11] Fix deprecated parentheses in standard library --- Source/DafnyCore/Dafny.atg | 2 +- .../src/Std/Arithmetic/DivMod.dfy | 26 ++++++------ .../src/Std/Arithmetic/Mul.dfy | 40 +++++++++---------- 3 files changed, 34 insertions(+), 34 deletions(-) diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 13a78795685..db6a1c2425e 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -3102,7 +3102,7 @@ ForallStmt ( IF(la.kind == _openparen) /* disambiguation needed, because of the possibility of a body-less forall statement */ "(" (. errors.Deprecated(ErrorId.p_deprecated_forall_statement_with_parentheses_around_bound_variables, t, - "a forall statement with no bound variables is deprecated; use an 'assert by' statement instead"); + "parentheses around the forall-statement bound variables are deprecated and not needed"); .) [ QuantifierDomain ] ")" diff --git a/Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy b/Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy index c99998a53e7..d6340101b0f 100644 --- a/Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy @@ -152,7 +152,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod { lemma LemmaDivIsOrderedByDenominatorAuto() ensures forall x: int, y: int, z: int {:trigger x / y, x / z} :: 0 <= x && 1 <= y <= z ==> 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); @@ -173,7 +173,7 @@ module {:disableNonlinearArithmetic} 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); @@ -204,7 +204,7 @@ module {:disableNonlinearArithmetic} 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); @@ -224,7 +224,7 @@ module {:disableNonlinearArithmetic} 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); @@ -243,7 +243,7 @@ module {:disableNonlinearArithmetic} 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); @@ -262,7 +262,7 @@ module {:disableNonlinearArithmetic} 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); @@ -280,7 +280,7 @@ module {:disableNonlinearArithmetic} 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); @@ -299,7 +299,7 @@ module {:disableNonlinearArithmetic} 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); @@ -319,7 +319,7 @@ module {:disableNonlinearArithmetic} 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); @@ -339,7 +339,7 @@ module {:disableNonlinearArithmetic} 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); @@ -409,7 +409,7 @@ module {:disableNonlinearArithmetic} 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); @@ -428,7 +428,7 @@ module {:disableNonlinearArithmetic} 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); @@ -627,7 +627,7 @@ module {:disableNonlinearArithmetic} 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 8731e740e23..d460aa8739d 100644 --- a/Source/DafnyStandardLibraries/src/Std/Arithmetic/Mul.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Arithmetic/Mul.dfy @@ -73,7 +73,7 @@ module {:disableNonlinearArithmetic} 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); @@ -103,7 +103,7 @@ module {:disableNonlinearArithmetic} 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); @@ -152,7 +152,7 @@ module {:disableNonlinearArithmetic} 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); @@ -172,7 +172,7 @@ module {:disableNonlinearArithmetic} 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); @@ -192,7 +192,7 @@ module {:disableNonlinearArithmetic} 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); @@ -215,7 +215,7 @@ module {:disableNonlinearArithmetic} 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); @@ -238,14 +238,14 @@ module {:disableNonlinearArithmetic} 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); @@ -266,7 +266,7 @@ module {:disableNonlinearArithmetic} 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); @@ -291,7 +291,7 @@ module {:disableNonlinearArithmetic} 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); @@ -312,7 +312,7 @@ module {:disableNonlinearArithmetic} 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); @@ -333,7 +333,7 @@ module {:disableNonlinearArithmetic} 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); @@ -351,7 +351,7 @@ module {:disableNonlinearArithmetic} 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); @@ -368,7 +368,7 @@ module {:disableNonlinearArithmetic} 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); @@ -386,7 +386,7 @@ module {:disableNonlinearArithmetic} 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); @@ -430,7 +430,7 @@ module {:disableNonlinearArithmetic} 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); @@ -452,7 +452,7 @@ module {:disableNonlinearArithmetic} 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); @@ -474,7 +474,7 @@ module {:disableNonlinearArithmetic} 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); @@ -494,7 +494,7 @@ module {:disableNonlinearArithmetic} 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); @@ -512,7 +512,7 @@ module {:disableNonlinearArithmetic} 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); From 463a5f62a09976716d9ef0afe07bd983b29d8e1c Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 3 Nov 2024 22:09:47 -0800 Subject: [PATCH 08/11] Adjust tests --- .../LitTest/cloudmake/CloudMake-ConsistentBuilds.legacy.dfy | 4 ++-- .../TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) 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/Parallel.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect index 2025fe08040..c64a67732f5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect @@ -1,3 +1,4 @@ +Parallel.dfy(267,11): Warning: parentheses around the forall-statement bound variables are deprecated and not needed 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 From 1ede1ce3b24d254d4df62b0a7d1c2422d53247d0 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 7 Nov 2024 10:21:22 -0800 Subject: [PATCH 09/11] Move deprecation tests to Deprecation.dfy --- .../LitTests/LitTest/dafny0/Deprecation.dfy | 56 +++++++++++++++++++ .../dafny0/Deprecation.dfy.verifier.expect | 6 ++ .../LitTests/LitTest/dafny0/Parallel.dfy | 39 ------------- .../LitTest/dafny0/Parallel.dfy.expect | 11 +--- 4 files changed, 65 insertions(+), 47 deletions(-) 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/Parallel.dfy index bb45f97a50e..4fdf67393f1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.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/Parallel.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect index c64a67732f5..d1712b548fc 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect @@ -1,7 +1,3 @@ -Parallel.dfy(267,11): Warning: parentheses around the forall-statement bound variables are deprecated and not needed -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 @@ -11,8 +7,7 @@ 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 +Parallel.dfy(303,9): Error: assertion might not hold +Parallel.dfy(290,32): Related location: this proposition could not be proved -Dafny program verifier finished with 19 verified, 10 errors +Dafny program verifier finished with 17 verified, 9 errors From e191c3611f4bbce8f5974b4b32937e56435ac502 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 7 Nov 2024 10:23:00 -0800 Subject: [PATCH 10/11] Rename Parallel* test files to ForallStmt* --- .../LitTests/LitTest/dafny0/{Parallel.dfy => ForallStmt.dfy} | 0 .../LitTest/dafny0/{Parallel.dfy.expect => ForallStmt.dfy.expect} | 0 .../{ParallelResolveErrors.dfy => ForallStmtResolveErrors.dfy} | 0 ...esolveErrors.dfy.expect => ForallStmtResolveErrors.dfy.expect} | 0 4 files changed, 0 insertions(+), 0 deletions(-) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/{Parallel.dfy => ForallStmt.dfy} (100%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/{Parallel.dfy.expect => ForallStmt.dfy.expect} (100%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/{ParallelResolveErrors.dfy => ForallStmtResolveErrors.dfy} (100%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/{ParallelResolveErrors.dfy.expect => ForallStmtResolveErrors.dfy.expect} (100%) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy.expect similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy.expect 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/ParallelResolveErrors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmtResolveErrors.dfy.expect similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParallelResolveErrors.dfy.expect rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmtResolveErrors.dfy.expect From 1dbad1b936bfd5d9481204b9cc74606ee20b8c2a Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 7 Nov 2024 10:27:25 -0800 Subject: [PATCH 11/11] Applying renaming in test files --- .../LitTest/dafny0/ForallStmt.dfy.expect | 22 ++-- .../dafny0/ForallStmtResolveErrors.dfy.expect | 110 +++++++++--------- 2 files changed, 66 insertions(+), 66 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy.expect index d1712b548fc..f31e392521b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmt.dfy.expect @@ -1,13 +1,13 @@ -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(303,9): Error: assertion might not hold -Parallel.dfy(290,32): Related location: this proposition could not be proved +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/ForallStmtResolveErrors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmtResolveErrors.dfy.expect index eee0d123d2c..1362eed332a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmtResolveErrors.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallStmtResolveErrors.dfy.expect @@ -1,55 +1,55 @@ -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 +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