Skip to content

Dafny 2.3.0
Compare
Choose a tag to compare
@RustanLeino RustanLeino released this 06 May 23:22
· 3501 commits to master since this release
v2.3.0
6f48c4a

The biggest change in version 2.3.0 from version 2.2.0 is the support of compilation to JavaScript and Go, in addition to the previously existing compilation to .NET. There are also some languages changes and other improvements, as described below.

Version 2.3.0 of Dafny requires the included Boogie version 2.4.1 and has been tested to work with Z3 version 4.5.0 and the included Z3 version 4.8.4.

Language

  • Datatype updates are now allowed to update shared destructors. However, updates are now restricted to those that don't change the value's constructor. Also, updates where a candidate result constructor has anonymous parameters are no longer allowed. A precise description of datatype update is found in Test/dafny0/SharedDestructors.dfy, starting at line 65. Improved error messages and /rprint option for datatype updates.

  • Added labeled assertion statements and labeled method/iterator preconditions. The syntax is like assert L: Expr; and requires L: Expr. The assumption that usually comes from an assertion or precondition is suppressed when these are labeled. To use the assumption, a reveal L; statement or expression must be used.
    See Test/dafny3/CalcExample.dfy for some examples.

  • Labels, both in the statement label L: and in the new labeled assertions and preconditions, are now allowed to look like numeric literals (as was already allowed for field names and datatype destructors).

  • reveal statements can now take a list of arguments.

  • Allow more types with non-0 initializers to be passed as type parameters (supported by the compiler's
    new use of run-time type descriptors).

  • Allow a module's submodules to be given in separate files: A module can now be declared with a qualified name. This is a just a syntactic shorthand for inserting the module into the indicated parent module. For example,

    module A {
  module B { }
}

    must be written in one file, or else the curly braces won't match up. But these declarations can now be provided as:

    module A { }
module A.B { }

    which allows A and A.B to be declared in separate files.

  • A non-abstract module is not allowed to import or use (as in dereferencing the name of) an abstract module. However, any non-abstract module is allowed to contain or refine abstract modules.

Type checking

  • Temporarily, added a {:termination false} attribute that can be placed on trait declarations to unsoundly ignore termination checking for dynamic method dispatch that goes to other modules. A better and sound solution will come in the future.

  • Various bug fixes

Verifier

  • Added specialized (extensional) equality for inductive datatypes.

  • Various bug fixes

Compiler

  • Compilation now targets not just .NET (via C#), but also JavaScript and Go. These are selected with the command-line switch /compileTarget:<language>, where <language> is one of cs, js, or go.

  • For compilation to JavaScript, also accept files with extension .js on the command line.

  • Improved {:extern} for methods and function:
    {:extern} says to use the Dafny method name as the external name.
    {:extern "M"} and {:extern "Q", "M"} say to use M as the external name.
    In the 0- and 1-argument forms, qualified forms of the method name are constructed according
    to the enclosing class and modules in Dafny (and those enclosing declarations may have
    :extern attributes themselves, which are be taken into account).
    In the 2-argument form, Q.M is used as the qualified name and the names of enclosing classes
    and modules are not consulted. If needed, Q can contain dots; for example,
    {:extern "R.S.T", "M"} will cause the qualified name of the extern to be R.S.T.M.

  • An {:extern} constructor is now called using C#'s constructor mechanism.

  • Improved {:extern} for modules:
    {:extern} says to use the module name as the extern name.
    {:extern "N"} says to use "N" as the extern name.
    {:extern "N", "L"} for JavaScript says to use "N" as the extern name and to initialize it to
    require("L").
    For compilation to Go, {:extern ""} indicates Go's built-in "module", which contains types
    like error. (For more information about using externs with Go, see Docs/Compilation/Go.md.)

  • Support for interacting with C code on .NET. The {:dllimport} attribute translates to the .NET DllImportAttribute. Attribute {:handle} can be placed on some reference types to cause their translation to turn into uninterpreted machine words.

  • Deprecated extern keyword. Use the {:extern} attribute instead.

  • Allow program entry point (Main method) to take any number of ghost in- and out-parameters.

  • Added command-line option /compile:4, which is like /compile:3 but compiles/runs regardless of how the verification turned out.

  • Added command-line option /compileVerbose, which can suppress some information compiler output.

  • Removed the struct that was previously used in the C# compilation of datatypes. Also, compilation of datatypes with only one constructor are special-cased.

  • Renamed tuple types in the compiled code to something more straightforward and human readable.

  • Improvements in identifier-protection schemes (which avoid clashes with keywords in the target language).

  • Compilation to C# uses /nowarn:0168 to suppress warnings about unused variables under Mono.

  • Improved printing of real numbers.

  • Various improvements in compiled code.

  • Various bug fixes

Assets 7
Loading