search

dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

fix: Add missing type characteristics #154

Closed RustanLeino closed 5 months ago

RustanLeino commented 6 months ago

This PR primarily adds missing (!new) type characteristics in function declarations. These had gone undetected, because of a latent bug that has now been fixed. The bug fix requires these fixes in the libraries.

This PR also cleans up some library files: removing deprecated semi-colons, removing unnecessary parentheses, stylizing order of specification clauses, and removing explicit triggers that are saying the same thing as those triggers that are automatically inferred.

The PR also changes forall ensures ... statements with no bound variables into assert ... by statements. (I think we attempted this change once before, only to find that the change tickled some brittleness issue. Let's see if they verify this time.)

Finally, the PR improves some reads fn clauses, where fn is some function. In one case, such a reads clause was probably accidentally (and I changed it to the more specific reads fn(this)). In the other cases, the reads fn clause had ended up reading more than the enclosing function's precondition could support. The new reads clauses are more specific than the previous, so, semantically, they should not affect callers. I'm surprised how these were not detected before (am I perhaps running the wrong version of Dafny when running the libraries test suite?). In fact, I also received an error, which I think is due to that a previous version of Dafny didn't assume requires clauses when checking reads clauses in lambda expressions (or was it perhaps the other way around?). If there's still a problem with my modifications, I hope CI will discover them.

Hint to reviewers: If you want to see each of the simple modifications, I suggest looking at each commit individually.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

RustanLeino commented 5 months ago

Note, this libraries repository was recently deprecated (https://github.com/dafny-lang/libraries/pull/155). Still, I think it makes sense to roll in this PR, since it contains valid changes and is otherwise ready to go.