Suggest changes that could reduce brittleness

[atomb]

Summary

When there are changes that could potentially reduce brittleness, but aren't guaranteed to, it would be useful to have unobtrusive suggestions to help Dafny programmers more quickly learn what code patterns are often at fault in creating brittle verification.

Background and Motivation

Brittleness is a regular challenge in Dafny verification, and can sometimes block the development process indefinitely while trying to refactor code into a form that will verify.

Sometimes the reasons for brittleness are straightforward. Issue #5253 proposes a feature to warn about situations that essentially always lead to brittleness. However, sometimes the reasons are not as straightforward, and certain code changes may be helpful in one instance but unnecessary (or even detrimental) in others. When there are changes that would often help reduce brittleness, but aren't guaranteed to, it would be helpful to be able to quickly learn what they are when brittleness arises, or to use them to refactor code in advance when worried about brittleness arising.

Proposed Feature

Provide suggestions about how to refactor code to reduce brittleness when the following patterns occur:

• Functions with ensures clauses (and suggest moving them to lemmas)
• Transparent functions (and suggest using --default-function-transparency, making them opaque, or using current or future features that provide more fine-grained control over transparency)
• Contract clauses without labels (and suggest labeling them)
• Subset types with transparent/inline predicates (and suggest moving them to opaque functions or making them opaque inline if we implement a feature for doing that)

This would be enabled with a flag --suggest-brittleness-reduction. At the CLI, it would print textual messages pointing to the code in question and describing how one might want to refactor it. In the IDE, it would result in an unobtrusive dotted line under the relevant pieces of code that would show the same message when hovering over.

Alternatives

Like #5253, these suggestions could be static, in a document. But, like #5253, direct, active feedback, as long as it isn't obtrusive, would help accelerate the process.

[keyboardDrummer]

Provide suggestions about how to refactor code to reduce brittleness when the following patterns occur:

I feel like each of the listed items warrants its own discussion. I suggest having separate GH issues for them.

For example, looking at Contract clauses without labels (and suggest labeling them). Am I correctly understanding that each ensures clause can have a label? If so then I wonder:

• Why does the contract have multiple ensures clauses? If it's a lemma, why is it not split into two lemmas?
• What if the contract has only a single ensures clause but a conjunction, so only one label can be given? Should it be possible to label sub-expressions?
• If it's a function with multiple ensures clauses, what's the point of having this suggestion if we're driving towards functions without ensures clauses anyways?