This HTML5 document contains 84 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n12https://github.com/dafny-lang/
dcthttp://purl.org/dc/terms/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
n14https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/
n11http://research.microsoft.com/
dbthttp://dbpedia.org/resource/Template:
schemahttp://schema.org/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n17http://dbpedia.org/resource/ESC/
n15http://commons.wikimedia.org/wiki/Special:FilePath/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n19http://en.wikipedia.org/wiki/
dbchttp://dbpedia.org/resource/Category:
dbphttp://dbpedia.org/property/
provhttp://www.w3.org/ns/prov#
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
dbrhttp://dbpedia.org/resource/

Statements

Subject Item
dbr:Dafny
rdf:type
schema:Language wikidata:Q9143 wikidata:Q315 dbo:ProgrammingLanguage owl:Thing dbo:Language
rdfs:label
Dafny
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
dbp:wikiPageUsesTemplate
dbt:Microsoft_FOSS dbt:Microsoft_Research dbt:Unreferenced_section dbt:Cite_book dbt:Reflist dbt:Infobox_programming_language dbt:Start_date_and_age dbt:Microsoft_development_tools
foaf:homepage
n11:dafny
dct:subject
dbc:Microsoft_programming_languages dbc:Statically_typed_programming_languages dbc:Software_using_the_MIT_license dbc:Academic_programming_languages dbc:Experimental_programming_languages dbc:Programming_languages_created_in_2009 dbc:Proof_assistants dbc:Microsoft_Research dbc:Microsoft_free_software
dbo:wikiPageExternalLink
n12:dafny n11:dafny n14:
dbo:latestReleaseDate
2021-02-03
dbo:latestReleaseVersion
3.0.0
foaf:name
Dafny
dbo:thumbnail
n15:Dafny_logo.jpg?width=300
foaf:depiction
n15:Dafny_logo.jpg
prov:wasDerivedFrom
n19:Dafny?oldid=1061858678&ns=0
dbo:wikiPageID
56073623
dbo:wikiPageLength
12180
dbo:wikiPageRevisionID
1061858678
dbo:wikiPageWikiLink
dbr:Springer_Science+Business_Media dbr:Compiled_language dbr:Design_by_contract dbr:Intermediate_representation dbc:Experimental_programming_languages dbr:Mathematical_induction dbr:Loop_variant dbc:Programming_languages_created_in_2009 dbr:Imperative_programming dbr:Microsoft_Research dbr:Static_program_analysis dbc:Microsoft_free_software dbr:Separation_logic dbr:Proof_by_exhaustion dbc:Statically_typed_programming_languages dbr:Functional_programming dbc:Microsoft_programming_languages dbr:Lemma_(mathematics) dbr:Pure_function dbr:Proof_assistant dbc:Microsoft_Research dbr:Structural_induction dbr:Type_system dbc:Academic_programming_languages dbr:Z3_Theorem_Prover dbr:C_Sharp_(programming_language) dbr:Loop_invariant dbr:Object-oriented_programming dbc:Proof_assistants dbr:Postcondition dbr:Side_effect_(computer_science) dbc:Software_using_the_MIT_license dbr:MIT_License dbr:Hoare_logic n17:Java dbr:NOP_(code) dbr:Access_modifiers dbr:Precondition dbr:Formal_specification
dbo:developer
dbr:Microsoft_Research
dbo:license
dbr:MIT_License
foaf:page
n11:dafny
dbo: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.
foaf:isPrimaryTopicOf
n19:Dafny