Dafny 3.2.0

Dafny 3.2 introduces three new language features: run-time type tests for reference types (is), default parameter values, and for loops.

Language

• Permit as for reference types. For example, the expression a as object can be used to upcast an array a to type object, and o as array<int> can be used to downcast an object o to an integer array. There is a proof obligation that the expression evaluates to a value of the given type.

• Introduce is for reference types. For example, if C is a class that extends a trait Tr and t is a variable of type Tr, then t is C says whether or not the dynamic type of t (that is, the allocated type of t) is C. Any type parameters given in the target type must be uniquely determined from the static type of the expression; this maintains type parametricity in the language. Compilation support is provided for the C#, Java, JavaScript, and Go targets.

• Arguments to functions, methods, object constructors, and datatype constructors can be passed in not just positionally, but also by naming the parameter. For example, a call might look like GetIceCream(Vanilla, whippedCream := false, cherryOnTop := true).

• Allow parameters to be declared with nameonly, which says the parameter is not allowed to be passed in positionally.

• Allow parameters to be declared with a default-value expression.

• Introduce for loops. For example, you can now write

  for i := 0 to a.Length {
    print a[i];
  }
  

• Accept attributes in more places (e.g., on loops and cases).

Resolution, type checking, and type inference

• Fix method/function override detection.

• Fix omitted resolution of some attributes.

• Fix crash related to bitvectors.

Verifier

• Fix soundness issue where types were not cardinality-preserving.

• Improve/fix issues in matching-pattern expressions.

• Remove a matching loop in integer multiplication.

• Improve issues in dealing with function values.

• Fix bug that caused omission of some precondition checks.

• Fix omitted well-formedness checks on modifies and modify.

• Fix some malformed Boogie code.

• Additional bug fixes.

Compiler

• Compilation to Go sets flag to request pre-module behavior in Go. (In the future, the Go compiler will change to make use of Go modules.)

• For C#, fix rewriting of the name Main.

• Bug fixes for traits in Go.

• Tuple fixes in C++.

• Fix construction of large integers in Java.

• Fix comparison of some large integers in JavaScript.

• For C++, customize g++ warning settings and null printing based on underlying OS.

Documentation

• Some fixes.

IDE

• Upgrade the LSP Implementation of the Language Server.

Tool

• Make timeLimitMultiplier more specific.

• Fix and improve pretty printing.

Implementation

• In the compilers, TargetWriter is now named ConcreteSyntax. It has several new features for making it easier to generate well-formatted target code.

• Move some files into Verifier folder.

• Swap names Join and Meet.