Dafny 1.7.0
Dafny 1.7.0 summary
Dafny 1.7.0 screenshot
Dafny 1.7.0 description
Dafny will provide developers with a programming language alongside a program verifier. With Dafny, as you type in your program, the verifier makes sure that your code is error-free.
Dafny itself draws multiple pieces of influence from:
· Euclid (from the mindset of a designing a language whose programs are to be verified)
· Eiffel (like the built-in contract features)
· CLU (like its iterators, and inpiration for the out-parameter syntax)
· Java and C# (like the classes, although Dafny does not support subclassing)
· ML (like the module system, and its functions and inductive datatypes, but Dafny does not support higher-order features)
· Coq (like the ability to include co-inductive datatypes and being able to write inductive and co-inductive proofs)
What's New in This Release:
· This version includes several bug fixes and other improvements (e.g., (co-)lemma keyword, field names can be sequences of digits, allow calls to ghost methods from expressions). It also adds several new features to the Visual Studio extension for Dafny (e.g., on-demand re-verification, parallelization, BVD integration, visualization for counterexamples).
Dafny 1.7.0 keywords
Dafny 1.7.0 for Developers
masocongty