[Feature request]: Generate explicit assertions

[MikaelMayer]

What is the feature you would like to see in a future version of Dafny?

When the Dafny verifier fails, it's sometimes obvious what is failing, sometimes it's not. It would be good to provide a code action to explicit the assertion that is failing.
Consider the following simple case:

Dafny throws a "potential division by zero". If we add a suitable assertion, in VSCode IDE it becomes obvious thanks to the green check mark that now the division passes, and the assertion took ownership of the error.

Although this is one of the simplest cases, consider the following more complex cases:

Function preconditions

In the example above, the only error is "function precondition might not hold", and what is failing is given only in the command line. It would be good to be able to have a code action to insert the failing precondition, like this:

Decreases clause generation

Similarly, when Dafny complains that "Cannot prove termination", it's not obvious to new users what needs to be asserted. For example:

With a suitable code action, we could simply automatically add the missing assertion:

Assign such that assertion generation

"to be compilable, the value of a let-such-that expression must be uniquely determined"

We could insert the appropriate assertion as well:

Similarly, for the existential aspect of it

we could insert the appropriate assertion as well:

Subset type constraint

In the following code:

function method increment(i: int): int
  requires i > 0 { i + 1 }

method Call(fn: int -> int) {
    var x := fn(-1);
}

method Main() {
    // We could suggest this:
    // assert forall i: int :: increment.requires(i)
    Call(increment);
}

---

This issue is related to #2153

[keyboardDrummer]

Thanks for the write-up. Looks great!

I feel your if and invariant generation examples are different from the rest since they're not about making an implicit assertion explicit, but about applying weakest precondition rules to move an assertion.

For the sake of reducing scope, do you think we could split that WP-based assertion moving to a different issue?

Also, in your if example it seems the assertion is copied before it is moved, and this operation is repeated up to the start of the method, but I think there's other options too that we should consider. I see two choices we can play with:

• Copy and then move, or just move, removing the original assertion.
• Only move one statement up, or move up all the way to the start of the method.

[keyboardDrummer]

I think that in the "Invariant generation" example it would be better to generate the invariant according to WP rules, so you would get !(b > 5) ==> a <= b instead of a <= b, and then this example would also fit better in #3102

[MikaelMayer]

For the sake of reducing scope, do you think we could split that WP-based assertion moving to a different issue?

Done as of today. I moved both "if" and "invariant" to this other issue:
#3102

I think that in the "Invariant generation" example it would be better to generate the invariant according to WP rules, so you would get !(b > 5) ==> a <= b instead of a <= b, and then this example would also fit better in #3102

Yeah that's a very interesting and clever remark. I changed my example here:
#3102
What I like is that your default invariant is weaker than mine. A user could always remove the hypothesis and have a stronger invariant.

[atomb]

Now that we're actively working on this, I'm adding a list of assertion types so we can keep track of which are implemented:

• DivisorNonZero
• ShiftLowerBound
• ShiftUpperBound
• ConversionIsNatural
• ConversionSatisfiesConstraints
• OrdinalSubtractionIsNatural
• OrdinalSubtractionUnderflow
• CharOverflow
• CharUnderflow
• ConversionFit
• NonNegative
• ConversionPositive
• IsInteger
• NonNull
• IsAllocated
• IsOlderProofObligation
• PreconditionSatisfied
• AssertStatementDescription
• RequiresDescription
• EnsuresDescription
• LoopInvariant
• CalculationStep
• EnsuresStronger
• RequiresWeaker
• ForallPostcondition
• YieldEnsures
• TraitFrame
• TraitDecreases
• FrameSubset
• FrameDereferenceNonNull
• Terminates
• DecreasesBoundedBelow
• Modifiable
• FunctionContractOverride
• MatchIsComplete
• AlternativeIsComplete
• PatternShapeIsValid
• ValidConstructorNames
• DestructorValid
• NotGhostVariant
• IndicesInDomain
• SubrangeCheck
• WitnessCheck
• PrefixEqualityLimit
• ForRangeBoundsValid
• ForRangeAssignable
• ValidInRecursion
• IsNonRecursive
• ForallLHSUnique
• ElementInDomain
• DefiniteAssignment
• InRange
• SequenceSelectRangeValid
• ComprehensionNoAlias
• DistinctLHS
• ArrayInitSizeValid
• ArrayInitEmpty
• LetSuchThatUnique
• LetSuchThatExists
• AssignmentShrinks
• ConcurrentFrameEmpty
• BoilerplateTriple