Category:Dafny

From Rosetta Code
This page is a stub. It needs more information! You can help Rosetta Code by filling it in!
Language
Dafny
This programming language may be used to instruct a computer to perform a task.
See Also:


Listed below are all of the tasks on Rosetta Code which have been solved using Dafny.
Your Help Needed
If you know Dafny, please write code for some of the tasks not implemented in Dafny.

Dafny is a programming language developed and maintained by Microsoft. It includes built-in specification constructs which can be used to verify the functional correctness of programs.

The Dafny programming language is designed to support the static verification of programs. It is imperative, sequential, supports generic classes, dynamic allocation, and inductive datatypes, and builds in specification constructs. The specifications include pre- and postconditions, invariants, frame specifications (read and write sets), and termination metrics.

Citations[edit]

Pages in category "Dafny"

The following 4 pages are in this category, out of 4 total.