Category:Dafny: Difference between revisions
Content added Content deleted
(Created page with "{{stub}}{{language|Ayrch}}") |
(Added basic information and links.) |
||
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{stub |
{{stub}} |
||
{{language|Daftny}} |
|||
'''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== |
|||
*[http://stackoverflow.com/tags/dafny/info Stack Overflow:Dafny] |
|||
*[https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ Dafny: A language and program verifier for functional correctness] at Microsoft |
|||
*[https://github.com/Microsoft/dafny Dafny at GitHub] |
|||
Latest revision as of 19:17, 4 May 2017
This programming language may be used to instruct a computer to perform a task.
| See Also: |
|
|---|
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
Pages in category "Dafny"
The following 4 pages are in this category, out of 4 total.