This would be a nice stepping stone toward having /testContracts check assert statements at runtime. If we implemented what you propose, all that flag would need to do would be to add an attribute to each assert statement.

Question: if the expression in assert {:expect} e is ghost, should the expect be silently ignored or should it be an error. I had thought the latter, to avoid surprises but Aaron's use case would prefer the former.

In the existing implementation of /testContracts, such a situation is a warning.

I'd say assert {:expect} e; should be an error if e is ghost, just as expect e would be, but it's reasonable for /testContracts to just give a warning if it is asked to convert an assert e; to an assert {:expect} e;.

I'd initially tried to implement this in user code as a testing utility:

method AssertAndExpect(p: bool) requires p {
  expect p;
}

The only issue is that then when the expect fails the error message is attached to the same source line in that method, not the caller. We could consider somehow giving user code the power to fix that.

I'm not so fond of this suggestion. When, many moons ago, we were in discussion of what today is expect, a large part of the discussion was what to name the keyword. When "expect" was finally suggested, everything about the statement became clear (or at least to me).

I see the proposal here more as a variation of expect than a variation of assert. Foremost, the condition must be compilable, which expect already does and assert does not. Also, if you want a run-time test, then you probably want the ability to provide something to print in case of an error, and the optional second argument to expect already allows this.

An important consideration is how to explain a statement like this to a user. I think considerable confusion would arise from trying to explain

An assert is proved by the verifier before the compiler even runs, and long before your program will be deployed. But you can nevertheless request to have your program halt if it's detected during deployment that the property doesn't actually hold.

This would seem to imply that the verifier's proofs are not to be trusted. More plausible would be to give an explanation like

The expect statement says to halt program execution if the given condition is found not to hold. One use case of expect is to check conditions of non-verified, external code. It may be that the expected condition follows from the stated-but-not-verified assumptions about external code, in which case you can decorate the expect statement with {:assert}, which directs the verifier to prove the condition from the assumptions in the context. The statement will still compile like an ordinary expect statement, which will catch evidence that the enclosing assumptions are incorrect.

(It took my some effort to write that paragraph, and it still isn't great.)

If we're going to prove this functionality in the language (rather than just having a AssertAndExpect method in a standard library), then I'd rather consider something like:

• A new statement altogether. (Just like for the design of the expect statement, the name of this statement will play a crucial role in explaining and justifying the statement.)
• expect {:assert}
• expect assert. There is a related precedence in Dafny to follow a symbol with assert, assume, or expect. For example, you can write :| assume and :- assert. In a similar way, one could imagine following the expect keyword (even though it's not a symbol) with assert.

Thanks @RustanLeino, I agree with all of this. In particular I recall thinking of "expect" and everything suddenly clicked. :)

I suggested in #3458 that we could change the semantics of expect to also require proof. i.e. the default behavior would be both a verification check AND a runtime check. If you wanted the current behavior of only a runtime check, you would write expect {:axiom}. This would be a reasonable breaking change over Dafny 4.0: in the worst case a codebase can just insert {:axiom} on every expect to maintain current behavior.

How does that idea sit with you? The more I write tests in Dafny, the more I find that every expect statement I write should actually be provable, and if it's not it's often an indication that the code you are trying to test doesn't have a strong enough specification to be used in practice.

Here's a very rough attempt at the explanation for users:

An expect statement must be proven by the verifier as well, but also halts program execution if the given condition is found not to hold at runtime. The expect statement is useful for writing tests using the {:test} attribute, to ensure that code still behaves correctly when compiled and linked to unverified code.

Another use of expect is to check conditions of non-verified, external code, in which case it is not possible to prove the condition always holds. You can decorate the expect statement with {:axiom}, which directs the verifier to not attempt to prove the condition.

Note this forces us to address the awkward question of why you need to write tests even when your code is proven correct, but I think that's a good thing to build trust in the entire platform.

There is another use case -- actually my most common one. When developing code, not everything proves and not everything executes correctly. I find it helpful when an assert does not prove to put in an expect and run the code to see if the expect obviously fails (in which case it is not just that Z3 is having a hard time).

Plus if I were responsible for high-confidence code, I would want both static proof and dynamic test.

There is another use case -- actually my most common one. When developing code, not everything proves and not everything executes correctly. I find it helpful when an assert does not prove to put in an expect and run the code to see if the expect obviously fails (in which case it is not just that Z3 is having a hard time).

You can always run turn off verification right? Maybe --no-verify should turn all asserts into expects? Would you still need an assertAndExpect statement then?

I #3458 (comment) in #3458 that we could change the semantics of expect to also require proof. i.e. the default behavior would be both a verification check AND a runtime check. If you wanted the current behavior of only a runtime check, you would write expect {:axiom}. This would be a reasonable breaking change over Dafny 4.0: in the worst case a codebase can just insert {:axiom} on every expect to maintain current behavior.

We plan to have assume statements generate a warning unless {:axiom} is added. What you suggest would make adding {:axiom} to expect behave differently from adding it to assume. I also wonder when an attribute is preferable over a keyword.

What's the use-case for asserting and expecting at the same time? Wouldn't you want to expect exactly your axioms, at which point there is nothing to assert?

Closing this issue as it has mixed support.