dafny-lang/dafny v3.0.0-Prerelease4

Dafny 3.0.0 Prerelease4

on GitHub

Language

• A subset type or newtype now supports the following witness clauses:
  • witness E says that E is a compiled expression that is a value of the type
  • the absence of a witness defaults to
    -- witness 0 for types based on integers or bitvectors,
    -- witness 0.0 for real-based types,
    -- witness {} for set-based types,
    -- etc.
  • ghost witness E says that E is a ghost expression that is a value of the type
  • witness * opts out of witness checking; instead, the type is treated as being possibly empty

Type checking

• Improve type inference for imported modules.

Resolution

• Enforce give type-characteristics for type synonyms and opaque types.

Verification

• Add /induction:4 option and make it the default. This new mode applies automatic
  induction to lemmas, but not to quantifiers. Use the {:induction} attribute to apply
  automatic induction to individual quantifiers.

Compilation

• Mature the support for Main methods. Check that the main method is unique, allow {:main}
  attribute, introduce /Main command-line switch.

• Make /compile and /spillTargetCode command-line options work consistently for the
  5 compilers: C#, JavaScript, Go, Java, C++. The /compile option controls whether or not an
  executable target is generated, and also controls whether or not to run the program upon
  successful compilation.

  • Option /compile:0 generates no executable target.
  • Option /compile:1 generates an executable target that can be run.
  • Option /compile:3 compiles and runs the program, but doesn't generate an executable target unless necessary for running.

  The /spillTargetCode option controls whether or not textual target code is generated.
  This can be useful if the Dafny program is to be manually compiled with handwritten code in the
  target language.

  The test file Test/comp/compile1quiet/CompileRunQuietly.dfy shows how to run the executable target
  generated by Dafny.

  The test file Test/comp/manualcompile/ManualCompile.dfy shows manual compiler calls that can be applied
  to the textual target code generated.

Documentation

• Improve Dafny Language Reference Manual.

Tool

• Retire /ironDafny and /dafnycc command-line options.

Implementation

• Use .NET 5.0 version of Coco/R.