Implementing an optional argument for the :expect attribute

Source/DafnyCore/AST/Statements/ExpectStmt.cs

@@ -4,6 +4,7 @@
 namespace Microsoft.Dafny;
 
 public class ExpectStmt : PredicateStmt, ICloneable<ExpectStmt> {
+ public static string DefaultMessage = "expectation violation";
  public Expression Message;
 
  public ExpectStmt Clone(Cloner cloner) {
@@ -32,4 +33,4 @@ public ExpectStmt(RangeToken rangeToken, Expression expr, Expression message, At
  }
  }
  }
-}
+}

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -3066,7 +3066,8 @@ public class CheckHasNoAssumes_Visitor : BottomUpVisitor {
  expr = expectStmt.Expr;
  } else {
  var assertStmt = (AssertStmt)stmt;
- msg = new StringLiteralExpr(stmt.Tok, "expectation violation", false);
+ var expectAttr = Attributes.Find(stmt.Attributes, "expect");
+ msg = expectAttr.Args.Count > 0 ? expectAttr.Args[0] : new StringLiteralExpr(expectAttr.Tok, ExpectStmt.DefaultMessage, false);
  expr = assertStmt.Expr;
  }
  // TODO there's potential here to use target-language specific features such as exceptions

Source/DafnyCore/Resolver/GhostInterestVisitor.cs

@@ -72,29 +72,33 @@ class GhostInterestVisitor {
  Contract.Assume(!codeContext.IsGhost || mustBeErasable); // (this is really a precondition) CodeContext.IsGhost ==> mustBeErasable
  Contract.Assume(mustBeErasable || proofContext == null); // (this is really a precondition) !mustBeErasable ==> proofContext == null 
 
- if ((stmt is AssertStmt && !Attributes.Contains(stmt.Attributes, "expect")) || stmt is AssumeStmt) {
+ if (stmt is AssumeStmt) {
  stmt.IsGhost = true;
+
+ } else if (stmt is AssertStmt) {
+ var expectAttr = Attributes.Find(stmt.Attributes, "expect");
+ stmt.IsGhost = expectAttr == null;
  var assertStmt = stmt as AssertStmt;
  if (assertStmt != null && assertStmt.Proof != null) {
  Visit(assertStmt.Proof, true, "an assert-by body");
  }
-
- } else if (stmt is ExpectStmt || (stmt is AssertStmt && Attributes.Contains(stmt.Attributes, "expect"))) {
- stmt.IsGhost = false;
- Expression msg;
- Expression expr;
- if (stmt is ExpectStmt) {
- var expectStmt = (ExpectStmt)stmt;
- msg = expectStmt.Message;
- expr = expectStmt.Expr;
- } else {
- var assertStmt = (AssertStmt)stmt;
- if (assertStmt.Proof != null) {
- Visit(assertStmt.Proof, true, "an assert-by body");
+ if (expectAttr != null) {
+ if (mustBeErasable) {
+ Error(stmt, "assert with {{:expect}} statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+ } else {
+ Expression expr = assertStmt.Expr;
+ Expression msg = expectAttr.Args.Count > 0 ? expectAttr.Args[0] : new StringLiteralExpr(expectAttr.Tok, ExpectStmt.DefaultMessage, false);
+ ExpressionTester.CheckIsCompilable(resolver, reporter, expr, codeContext);
+ Contract.Assert(msg != null);
+ ExpressionTester.CheckIsCompilable(resolver, reporter, msg, codeContext);
  }
- msg = new StringLiteralExpr(assertStmt.Tok, "expectation violation", false);
- expr = assertStmt.Expr;
  }
+
+ } else if (stmt is ExpectStmt) {
+ stmt.IsGhost = false;
+ var expectStmt = (ExpectStmt)stmt;
+ Expression msg = expectStmt.Message;
+ Expression expr = expectStmt.Expr;
  if (mustBeErasable) {
  Error(stmt, "expect statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
  } else {

Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs

@@ -4384,10 +4384,18 @@ public XConstraint_EquatableArg(IToken tok, Type a, Type b, bool allowSuperSub,
  enclosingStatementLabels = prevLblStmts;
  loopStack = prevLoopStack;
  }
+ if (assertStmt != null) {
+ var attr = Attributes.Find(assertStmt.Attributes, "expect");
+ if (attr != null) {
+ if (attr.Args.Count > 1) {
+ reporter.Error(MessageSource.Resolver, attr.tok, ":expect attribute may have at most one argument");
+ }
+ }
+ }
  var expectStmt = stmt as ExpectStmt;
  if (expectStmt != null) {
  if (expectStmt.Message == null) {
- expectStmt.Message = new StringLiteralExpr(s.Tok, "expectation violation", false);
+ expectStmt.Message = new StringLiteralExpr(s.Tok, ExpectStmt.DefaultMessage, false);
  }
  ResolveExpression(expectStmt.Message, resolutionContext);
  Contract.Assert(expectStmt.Message.Type != null); // follows from postcondition of ResolveExpression

Test/git-issues/git-issue-3410/git-issue-3410f.dfy

@@ -6,3 +6,12 @@ method Main() {
  assert {:expect} i == 41;
  print "Done\n";
 }
+
+method m() {
+ ghost var b: bool := true;
+ if b { assert {:expect} true; }
+}
+
+ghost method mm() {
+ assert {:expect} true;
+}

Test/git-issues/git-issue-3410/git-issue-3410f.dfy.expect

@@ -1,2 +1,4 @@
 git-issue-3410f.dfy(6,19): Error: ghost variables such as i are allowed only in specification contexts. i was inferred to be ghost based on its declaration or initialization.
-1 resolution/type errors detected in git-issue-3410f.dfy
+git-issue-3410f.dfy(12,9): Error: assert with {:expect} statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+git-issue-3410f.dfy(16,2): Error: assert with {:expect} statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+3 resolution/type errors detected in git-issue-3410f.dfy

Test/git-issues/git-issue-3410/git-issue-3410g.dfy

@@ -0,0 +1,7 @@
+// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method m() {
+ assert {:expect "",""} true;
+ assert {:expect 10} true;
+}

Test/git-issues/git-issue-3410/git-issue-3410g.dfy.expect

@@ -0,0 +1,2 @@
+git-issue-3410g.dfy(5,11): Error: :expect attribute may have at most one argument
+1 resolution/type errors detected in git-issue-3410g.dfy

Test/git-issues/git-issue-3410/git-issue-3410h.dfy

@@ -0,0 +1,8 @@
+// RUN: %exits-with 1 %baredafny run --no-verify --use-basename-for-filename "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+ var i: int := 42;
+ assert {:expect "expecting 42" } i == 41;
+ print "Done\n";
+}

Test/git-issues/git-issue-3410/git-issue-3410h.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier did not attempt verification
+[Program halted] git-issue-3410h.dfy(6,2): expecting 42

Test/git-issues/git-issue-3410/git-issue-3410k.dfy

@@ -0,0 +1,8 @@
+// RUN: %exits-with 1 %baredafny run --no-verify --use-basename-for-filename "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+ var i: int := 42;
+ assert {:expect i } i == 41;
+ print "Done\n";
+}

Test/git-issues/git-issue-3410/git-issue-3410k.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier did not attempt verification
+[Program halted] git-issue-3410k.dfy(6,2): 42

docs/DafnyRef/Attributes.md

@@ -623,6 +623,11 @@ method doSplitHere(x: bool) returns (y: int) {
 ### 23.3.3. `{:subsumption n}`
 Overrides the `/subsumption` command-line setting for this assertion.
 
+### 23.3.4. `{:expect s}`
+This attribute is recognized on an assert statement. If present, the statement's expression is both checked by the verifier and
+is compiled to a run-time test (like an expect statement). The optional argument of the attribute is used as
+the optional message provided by the equivalent expect statement.
+
 ## 23.4. Attributes on variable declarations
 
 ### 23.4.1. `{:assumption}`

docs/DafnyRef/Statements.md

@@ -1662,6 +1662,12 @@ their purpose -- to assist in proving the given assertion -- is manifest in the
 
 Examples of this form of assert are given in the section of the [`reveal`](#sec-reveal-statement) statement and in [_Different Styles of Proof_](http:https://leino.science/papers/krml276.html)
 
+An assert statement recoognizes an optional attribute `{:expect}`. If present, the statement acts as an `expect` statement as well as an assert, with the same expression.
+That is, the `assert {:expect}` statement will be iverified by the verifier and tested at runtime. 
+The `{:expect}` attribute may take an argument, which serves the same purpose as the 
+optional message in an [expect statement](#sec-expect-statement). If `{:expect}` is present, the tested expression may not be ghost, nor may the statement be in a ghost context.
+An `assert {:expect} P;` is equivalent to `assert P; expect P;`, but avoids replicating an identical expression P.
+
 ## 20.17. Assume Statement {#sec-assume-statement}
 ````grammar
 AssumeStmt =