Dafny: Difference between revisions
Begun creating a page about the Dafny programming language. |
Add references and additional description |
||
| Line 13: | Line 13: | ||
}} |
}} |
||
'''Dafny''' is an |
'''Dafny''' is an imperative language which supports [[formal specification]] through [[preconditions]], [[postconditions]] and [[loop invariant]]s. The language combines features primarily from the [[functional programming|Functional]] and [[imperative programming|Imperative]] paradigms, and includes limited support for [[object-oriented programming|Object-Oriented Programming]]. The language supports ''generic classes'', ''dynamic allocation'', ''inductive datatypes'' and a variation of [[separation logic]] known as ''implicit dynamic frames''<ref>{{cite conference|title=Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic | doi=10.1007/978-3-642-03013-0_8 | conference=Proceedings of the Conference on European Conference on Object Oriented Programming | pages=148--172 | year=2009}}</ref> for reasoning about side effects<ref>{{cite conference|title=Dafny: An Automatic Program Verifier for Functional Correctness | doi=10.1007/978-3-642-17511-4_20 | conference=Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning | pages=348--370 | year=2010}}</ref>. Dafny was created by Rustan Leino after his previous work on developing ESC/Modula-3, [[ESC/Java]], and [[Spec Sharp|Spec#]]. Dafny is a [[compiled programming language|compiled language]] that compiles to [[C Sharp (programming language)|C#]]. |
||
== Example == |
== Example == |
||
Revision as of 20:38, 17 December 2017
| Paradigm | Imperative, Functional |
|---|---|
| Designed by | K. Rustan M. Leino |
| First appeared | 2009 |
| Stable release | 2.0.0
/ September 23, 2017 |
| Typing discipline | Static, strong, safe, structural, flow-sensitive |
| License | MIT |
| Website | research |
Dafny is an imperative language which supports formal specification through preconditions, postconditions and loop invariants. The language combines features primarily from the Functional and Imperative paradigms, and includes limited support for Object-Oriented Programming. The language supports generic classes, dynamic allocation, inductive datatypes and a variation of separation logic known as implicit dynamic frames[1] for reasoning about side effects[2]. Dafny was created by Rustan Leino after his previous work on developing ESC/Modula-3, ESC/Java, and Spec#. Dafny is a compiled language that compiles to C#.
Example
The following example illustrates many of the interesting features in Whiley, including the use of precconditions, postconditions, and loop invariants.
- ^ Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. Proceedings of the Conference on European Conference on Object Oriented Programming. 2009. pp. 148--172. doi:10.1007/978-3-642-03013-0_8.
- ^ Dafny: An Automatic Program Verifier for Functional Correctness. Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning. 2010. pp. 348--370. doi:10.1007/978-3-642-17511-4_20.