Dafny is an imperative and functional compiled language that compiles to other programming languages such as C#, Java, JavaScript, Go and Python. It was created by K. Rustan M. Leino at Microsoft Research and first appeared in 2009 as a verification-aware language, meaning that verification is required alongside code development. Programmers state preconditions, postconditions, loop invariants and loop variants, and the tool discharges the resulting proof obligations automatically using the Boogie intermediate language and the Z3 theorem prover. It also offers object-oriented features such as generic classes, dynamic allocation and inductive datatypes. It is statically and strongly typed and released under the MIT license.
Facts
Classification
Typing Discipline Typing Discipline First Released Connections
Follows Typing Discipline
In Field
Licensed Under
In the Other Atlases
Developed By
Also in Business Atlas: the developer of this subject.
Sources
1. Dafny (Wikipedia)
Lead section
Dafny is an imperative and functional compiled language that compiles to other programming languages, such as C#, Java, JavaScript, Go, and Python.
Licensed Under: MIT License, Infobox: license
MIT
In Field: Programming Language Theory, Lead sentence
Dafny is an imperative and functional compiled language that compiles to other programming languages, such as C#, Java, JavaScript, Go, and Python.
View the Source2. Wikidata: Dafny
- Wikidata Q48989398, class allow-list match (w-wdresolver-0926)
- Wikidata Q48989398 P571 (inception)
View the SourceProgramming Language Database (PLDB): Dafny - PLDB
Programming Language Database (PLDB)In Group: General-Purpose Multi-Paradigm Languages, Page textQuote, In Group: General-Purpose Multi-Paradigm Languages, Page text
combines ideas primarily from the Functional and Imperative paradigms
Reader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.