About: Dafny

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: Dafny Goto Sponge NotDistinct Permalink

An Entity of Type : wikidata:Q9143, within Data Space : el.dbpedia.org associated with source document(s)

Dafny is an imperative and functional compiled language that compiles to other programming languages such as C# or Java, and supports formal specification through preconditions, postconditions, loop invariants and loop variants. The language combines ideas primarily from the functional and imperative paradigms, and includes limited support for object-oriented programming. Features include generic classes, dynamic allocation, inductive datatypes and a variation of separation logic known as implicit dynamic frames for reasoning about side effects. Dafny was created by Rustan Leino at Microsoft Research after his previous work on developing ESC/Modula-3, ESC/Java, and Spec#. Dafny is widely used in teaching and is regularly featured in software verification competitions (e.g. VSTTE'08, VSCOMP

Attributes	Values
rdf:type	Thing language programming language schema:Language wikidata:Q315 wikidata:Q9143
rdfs:label	Dafny (en)
rdfs:comment	Dafny is an imperative and functional compiled language that compiles to other programming languages such as C# or Java, and supports formal specification through preconditions, postconditions, loop invariants and loop variants. The language combines ideas primarily from the functional and imperative paradigms, and includes limited support for object-oriented programming. Features include generic classes, dynamic allocation, inductive datatypes and a variation of separation logic known as implicit dynamic frames for reasoning about side effects. Dafny was created by Rustan Leino at Microsoft Research after his previous work on developing ESC/Modula-3, ESC/Java, and Spec#. Dafny is widely used in teaching and is regularly featured in software verification competitions (e.g. VSTTE'08, VSCOMP (en)
dbp:wikiPageUsesTemplate	dbt:Cite_book dbt:Infobox_programming_language dbt:Microsoft_FOSS dbt:Microsoft_Research dbt:Reflist dbt:Start_date_and_age dbt:Unreferenced_section dbt:Microsoft_development_tools
foaf:homepage	http://research.microsoft.com/dafny
Subject	Experimental programming languages Programming languages created in 2009 Proof assistants Software using the MIT license Statically typed programming languages Microsoft Research Microsoft free software Academic programming languages Microsoft programming languages
Link from a Wikipage to an external page	http://research.microsoft.com/dafny https://github.com/dafny-lang/dafny https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/
latest release date	2021-02-03 (xsd:date)
latest release version	3.0.0
foaf:name	(en) Dafny (en)
thumbnail	wiki-commons:Special:FilePath/Dafny_logo.jpg?width=300
foaf:depiction
prov:wasDerivedFrom	http://en.wikipedia.org/wiki/Dafny?oldid=1061858678&ns=0
Wikipage page ID	56073623 (xsd:integer)
page length (characters) of wiki page	12180 (xsd:nonNegativeInteger)
Wikipage revision ID	1061858678 (xsd:integer)
Link from a Wikipage to another Wikipage	Formal specification NOP (code) Proof assistant Proof by exhaustion Access modifiers Separation logic Static program analysis C Sharp (programming language) Experimental programming languages Programming languages created in 2009 Proof assistants Software using the MIT license Statically typed programming languages Microsoft Research Lemma (mathematics) Object-oriented programming Postcondition Precondition Pure function Springer Science+Business Media Compiled language ESC/Java Hoare logic Microsoft Research Functional programming Imperative programming Design by contract Intermediate representation Type system Microsoft free software Structural induction Z3 Theorem Prover Loop invariant Loop variant MIT License Mathematical induction Side effect (computer science) Academic programming languages Microsoft programming languages
developer	Microsoft Research
license	MIT License
foaf:page	http://research.microsoft.com/dafny
has abstract	Dafny is an imperative and functional compiled language that compiles to other programming languages such as C# or Java, and supports formal specification through preconditions, postconditions, loop invariants and loop variants. The language combines ideas primarily from the functional and imperative paradigms, and includes limited support for object-oriented programming. Features include generic classes, dynamic allocation, inductive datatypes and a variation of separation logic known as implicit dynamic frames for reasoning about side effects. Dafny was created by Rustan Leino at Microsoft Research after his previous work on developing ESC/Modula-3, ESC/Java, and Spec#. Dafny is widely used in teaching and is regularly featured in software verification competitions (e.g. VSTTE'08, VSCOMP'10, COST'11, and VerifyThis'12). Dafny was designed to provide a simple introduction to formal specification and verification and has been used widely in teaching. Dafny builds on the Boogie intermediate language which uses the Z3 automated theorem prover for discharging proof obligations. (en)
foaf:isPrimaryTopicOf	http://en.wikipedia.org/wiki/Dafny
is Wikipage redirect of	Dafny (programming language)
is Link from a Wikipage to another Wikipage of	Grigore Roșu Bosque (programming language) Dafny (programming language) Microsoft and open source Daphne (disambiguation) Design by contract F* (programming language)
is influenced by of	F*
is foaf:primaryTopic of	http://en.wikipedia.org/wiki/Dafny

Faceted Search & Find service v1.17_git151 as of Feb 20 2025

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Nov 11 2024, on Linux (x86_64-ubuntu_focal-linux-gnu), Single-Server Edition (72 GB total memory, 923 MB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2025 OpenLink Software