Release Dafny 3.1.0 · dafny-lang/dafny

Dafny 3.1 is a minor update of Dafny 3.0. It mostly fixes some bugs, but it also adds some features.

Language

feature: Allow invocations of two-state functions/lemmas to indicate which "old state" to use. The syntax is
F@L(args), where F is the name of the function/lemma and L is a dominating label.
feature: Let any type with members refine its members.
Remove deprecated syntax NT(expr) for converting to a newtype NT. The current syntax is expr as NT.

fix: Added missing consistency checks for type characterstics ((!new), (00), (0), (==)).
fix: Check that all (ghost and non-ghost) const/var fields have initializers, when needed.
fix: Disallow decreases * on ghost methods.
If a * is used in a decreases or reads clause, no other expressions or *'s are allowed to be listed.
Update type-inference algorithm: meets and joins are now considered before making decisions about arbitrary numeric types.

feature: Expand guessing of decreases clauses for while loops. The new guessing look at sets, multisets, and sequences, and the guesses may be lexicographic tuples. The most useful of these changes is probably that while s != {} gives rise to the guess decreases s.
feature: Improve and expand auto-triggers for collections. Triggers for more expressions are now generated, so there will be fewer "no trigger" warnings. The changes also improve verifier performance for map comprehensions and fix some bugs.
fix: Remove some unintended differences between receiver parameters and ordinary parameters.
Fix encoding of map comprehensions.
Fix issue with labeled heap states.
fix: Detect and report Boogie out-of-resource errors.
Miscellaneous bug fixes

Fix initialization of let-such-that bound variables.
C#: Fix initialization issues related to extern opaque types.
Java: Fix compilation of datatype constructors with only ghost parameters, and other issues.
Java: Upon javac compilation failure, exit but don't crash.
Go: Fix compilation of map update.
C++: Support tuples with arbitrary arity.
C++: Fix some path-related problems.

feature!: Add command-line option /stdin that reads standard input as if it were a .dfy file. Remove the old support for this, which had been to mention stdin.dfy on the command line.
feature: Apply timeLimitMultipler to rlimit.
Fix/improve some scripts

Merge Language Server sources. This will help us better keep versions and refactorings in synch.
refactor: Improve UserDefinedType AST nodes by removing .ResolvedParam, and related changes.