Dafny icon

Dafny

3.0/5 4
MIT License   

A fairly new programming code language for those developers always on the lookout for something new when it comes to the environment they work in. #Programming language  #Code language  #Program verifier  #Language  #Code  #Verifier  

Description

changelog

Free Download

Dafny is a programming language inspired by Euclid, Eiffel, CLU, Java, C#, ML and Coq. It features pre- and post-conditions, along with loop variants and invariants. Limited support is provided for object-oriented programming. It's free and open-source, released under MIT License.

Among its list of features are generic classes, inductive data types, dynamic allocation, along with implicit dynamic frames (derivative from separation logic). The language is primarily being used in teaching formal specification and verification. It's also typically used in contests for verifying software.

Because it builds on the Boogie intermediate language, it uses Z3, which is included in the downloaded package. After unzipping the archive, you can run "dafny /help" to view a list of supported commands.

For instance, you can pick the Dafny prelude file  (/dprelude:<file>), print the Dafny program after resolving it (/rprint:<file>), specify the filename and location for the output .cs, .dll or .exe files (/out:<file>), ignore include directives (/noIncludes) and external attributes (/noExterns), as well as allow the implicit class called "_default" to contain fields, instance methods and functions (/allowGlobals).

Boogie options are available too, like allowing only parsing (/noResolve) or only parsing and resolving (/noTypeCheck). Additional commands can be used for inference, debugging and general tracking, CIVL, verification-condition generation and splitting, and so on.

What's new in Dafny 4.5.0:

  • New features:
  • Add the option --include-test-runner to dafny translate, to enable getting the same result as dafny test when doing manual compilation. (#3818)
  • Fix: verification in the IDE no longer fails for iterators
  • Fix: the IDE now provides feedback when verification fails to run, for example due to a bad solver path
Read the full changelog
User Comments
This enables Disqus, Inc. to process some of your data. Disqus privacy policy

Dafny 4.5.0

add to watchlist add to download basket send us an update REPORT
PRICE: Free
  runs on:
Windows 11
Windows 10 64 bit
  file size:
60.3 MB
  filename:
dafny-4.5.0-x64-windows-2019.zip
  1 screenshot:
Dafny - Dafny will provide users with a A fairly new programming code language for those of you always on the lookout for something like this
  main category:
Programming
  developer:
  visit homepage