Dafny 3.3.0

[robin-aws]

Dafny 3.3 makes many usability improvements. The language server, along with the next release of the VS Code plugin, offers better performance, displays informational message less like errors and more like hints, enlarges the repertoire of values that can be displayed for counterexamples, adds outlining features, etc.

Dafny 3.3 also adds a facility for generating test input. New language features include function by method, which allows a function to be implemented by statements, and ghost tuples.

Language

• Add function by method (see section 13.4 of the reference manual)

• Add ghost tuples: In addition to previous tuple types like (A, B, C), there is now an additional tuple type for each possibility of marking the components as ghost. For 3-tuples, that means the addition of the types (ghost A, B, C), (A, ghost B, C), (A, B, ghost C), (ghost A, ghost B, C), (ghost A, B, ghost C), (A, ghost B, ghost C), and (ghost A, ghost B, ghost C). There is still no non-ghost 1-tuple, but there is a ghost 1-tuple, (ghost A). The syntax for writing literal values of these types has ghost in front of the respective components. For example, (ghost 10, 12, ghost true) is a value of type (ghost int, int, ghost bool).

• Allow fresh to take an @-label

• Add ghost allocations. new can now be called in ghost contexts, which can be thought of as allocating the object in a special "ghost region" of the heap. A class can now declare a constructor to be ghost. Ghost constructors are used with ghost allocations of the class. The first phase of a ghost constructor is allowed to assign to both ghost and non-ghost fields of the class, but after that first phase, any non-ghost fields of the class are in effect readonly. Analogously, after a ghost new to allocate an array, the array's elements are in effect readonly. As part of this language addition, a ghost method is now allowed to allocate objects and arrays, but a lemma (lemma, twostate lemma, least lemma, greatest lemma) is still not allowed to do so.

Resolution, type checking, and type inference

• fix: Check type equality in override signatures

• fix!: Enforce non-nullness and allocatedness for unchanged

• Improve error location reported for bad break labels

Verifier

• The statement assume false; can now be used inside a loop body without turning the loop into a non-loop. Consequently, an assume false; inside the loop will not affect the verification of code outside the loop.

• Fix parallel assignment to const fields in constructor

• Fix :- assignment to const fields in constructor

• (internal) Verification stabilization: Use predecessor count instead of topological order index to determine function heights

• (internal) Verification stabilization: Use a hierarchical scheme for generating names of Boogie variables

• (internal) Emit captureState attributes in generated Boogie only when using /mv

• Miscellaneous bug fixes

Compiler

• Fix implementation of multiset operations related to zero multiplicity (C#, JavaScript, Go)

• Fix implementation of proper multiset-subset (Go)

• Fix compilation of superset operations

• Generate cleaner C# code

Documentation

• Remove mention of rise4fun.com, which is no longer available

• Miscellaneous fixes

IDE

• Improve performance

• Enable document outlines and the breadcrumb navigation at the top of the editor

• Do not display "Verified" for documents with parser/resolver errors

• Fix code suggestions in language server

• Add support for concurrent document updates

• Add language-server option to set the number of verifier cores

• Change the default info severity to hint. That is, the previous conspicuous blue underlines that were often confused for warnings or errors are now shown as some faint dots.

• Support verification timeouts in language server

• Fix language-server diagnostics for Windows

Tool

• Add /verificationLogger option, which records verification results for reporting and analysis

• Add /extractCounterexample option, which makes counterexample extraction accessible via the command line

• Add /warningsAsErrors

• Add /showSnippets, which displays a few lines of the offending source text

• Add test-generation facility, see https://github.com/dafny-lang/dafny/tree/master/Source/DafnyTestGeneration

• Improve pretty printing (import, and tuple arguments to functions)

• Use Boogie 2.9.6. Among other things, this means that dafny can be invoked with /errorTrace:0, which suppresses the display of the (for Dafny users mostly useless Boogie) execution trace.

• Make release builds when publishing Dafny

• Update use-local-boogie.sh to use .NET 5.0

Implementation

• Add an xUnit-based test runner for all of the lit tests under Test

• Fix nondeterminism in some tests (by serializing some tests and by increasing some time limits)

• Move source location of DafnyPrelude.bpl from Binaries to Source/Dafny

• Improve the use of pre-commit

• Add dafny-lang/libraries as submodule, to include its source code as integration tests

• Remove unnecessary solution configurations

• For Ubuntu build, use version 18.04

• Make it easier to run a local Boogie, see https://github.com/dafny-lang/dafny/wiki/INSTALL#build-against-a-custom-boogie

• Apply whitespaces formatting rules to entire codebase and run dotnet-format in the build

• Various code movement and refactoring; for example, breaking up Translator.cs into multiple files

• Simplify DafnyServer code by making it Dafny-specific, dropping ancient support for VCC and BCT

• Add an .editorconfig file to define the syntax style of the project

---

This discussion was created from the release Dafny 3.3.0.