dafny-lang/dafny v3.0.0-PreRelease2

Dafny 3.0.0 PreRelease2

on GitHub

Publishing release 3.0.0-PreRelease2

Language

• Improve auto-ghost declarations of local or bound variables: if the variable is declared with a initializing RHS and the RHS requires the variable to be ghost, then it is made ghost even if the declaration uses var, not ghost var.

• Allow :- assignments to have multiple LHSs and corresponding RHS. Only the first value on the RHS is treated specially via its failure-compatible type.

• The :- can now optionally be followed by assert or assume, not just expect. Each of these makes a claim about the success of the operation (i.e., assert !r.IsFailure();, assume !r.IsFailure();, expect !r.IsFailure();). When any of these keywords is used, there is no requirement for the failure-compatible type to have a PropagateFailure() member, since it will not be used.

• At the module scope, prefer local names over opened-imported names.

• Through constant folding, detect more constant bounds in type declarations. For example, newtype uint32 = x | 0 <= x < UINT32_LIMIT is now allow given const UINT32_LIMIT := 0x1_0000_0000.

• Allow negative literals for integer- and real-based types. More precisely, a - token follows by a digits-token is interpreted as a negative literal for integer- and real-based types. case-patterns in match constructs can use these negative literals. For bitvectors, such a - is still considered a unary-minus expression. For ORDINAL, such a - would be unary minus, but ORDINAL does not support unary minus, so it's an error.

• Rename inductive predicate, copredicate, inductive lemma, and colemma to least predicate, greatest predicate, least lemma, and greatest lemma, respecitvely. Deprecation warnings are emitted upon coming across the old syntax. In each of the 4 cases, the new syntax is a reserved keyword phrase. However, least and greatest are not reserved keywords by themselves.

• Allow object in list of parent traits.

• Allow a refinement module to extend members of all types that can have members, not just classes.

• Improved name resolution.

  • Imported types with the same name are not considered ambiguous if they refer to the same type .
  • Allow C. to refer to a datatype constructor, but only if C does not resolve to anything else.
  • Allow import A.B even without import A.

• Removed some deprecated features that have been marked as deprecated for a long time.

  • int(_) and real(_) conversions
  • parallel, comethod, free, and protected keywords
  • the optional ; at the end of type and import declarations

Type checking

• Resolution and type checking is applied also in redundant case branches

• Include functions in datatype cyclicity checks

Verification

• Verify type members of opaque types

• Fix to subset checks for sequences

Compilation

• In the compilers to JavaScript and Go, support all co- and contra-variant type parameters.

• In the compilers to C# and Java, support co- and contra-variant type parameters, but not yet for datatypes.

• The previous C# and Java error message "not supported: trait as type parameter" is now emitted only for co- and contra-variant type parameters of. (This will also be removed when co- and contra-variant type parameters have been implemented for datatypes in these compilers.)

• Use type descriptors for C# (as was already done for Java, JavaScript, and Go). Update type descriptors for those other compilers, too (for example, rename _dafny.Type to _dafny.TypeDescriptor for Go, and similarly for Java). This fixes issues with auto-initialization.

• Fix some incorrect uses of nil in Go

• Fix array coercions in Java

• Fix eta-expansion of instance members

• Fix name-capture problems in lambdas, quantifiers, set/map comprehensions, and tail-recursive functions/methods

Documentation

• Many additions to the Dafny Language Reference Manual

• Some fixes in the rise4fun tutorial

Tool

• Migrate to .NET Core v2

  If you used to use mono Dafny.exe to run Dafny before, use dotnet Dafny.dll now. This is automated in the dafny script in the Binaries folder.

• Allow and ignore duplicated filenames on the command line and via include directives. Such duplicates are determined using case-sensitive canonical path names.

• Clarify -countVerificationErrors help message

• Improved error message for missing Z3

Implementation

• Various refactorings to improve code structure, especially across the compilers

Miscellaneous

• Various bug fixes