RustanLeino
commented
2 years ago It would be nice to add, when possible, the information "not only is the verifier unable to verify your code, the code itself does not meet the specification". In general, an error message always means the verifier cannot do the proofs. Likewise, any counterexample is an example of a situation where the verifier is not able to complete the proof. It should not be understood as something that's wrong with the "code proper". We don't communicate this well enough to users. But note that the remedy is the same for the user--whether or not the "code proper" is correct, the user still needs to figure out a way to convince the verifier of this. Therefore, having a counterexample that highlights where the verifier struggles is desirable.
The counterexample generation feature is currently only a suggestion for a possible counterexample. This can help point users towards the bug in their code if there is one, but may not in fact be proof that there IS a bug.
It seems possible to at least attempt to verify that a counterexample does in fact violate an assertion. One potential approach is to augment a verification condition to assume the values in a counterexample, negate the possibly violated assertion, and run verification on the result. If the result verifies, Dafny could clearly communicate that an assertion is definitely not always true. Even if the counterexample is very difficult for users to understand, just knowing the difference between "verification failed because your code is wrong" and "verification failed, and you may just have to modify your proofs" would help users to know where to focus their attention.