Dafny (original) (raw)
Dafny is an imperative and functional compiled language that compiles to other programming languages, such as C#, Java, JavaScript, Go and Python. It supports formal specification through preconditions, postconditions, loop invariants, loop variants, termination specifications and read/write framing specifications. The language combines ideas from the functional and imperative paradigms; it includes 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#.
| Property | Value |
|---|---|
| dbo:abstract | Dafny is an imperative and functional compiled language that compiles to other programming languages, such as C#, Java, JavaScript, Go and Python. It supports formal specification through preconditions, postconditions, loop invariants, loop variants, termination specifications and read/write framing specifications. The language combines ideas from the functional and imperative paradigms; it includes 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 because it provides a simple, integrated introduction to formal specification and verification; it is regularly featured in software verification competitions (e.g. VSTTE'08, VSCOMP'10, COST'11, and VerifyThis'12). Dafny was designed as a verification-aware programming language, requiring verification along with code development. It thus fits the "Correct by Construction" software development paradigm. Verification proofs are supported by a mathematical toolbox that includes mathematical integers and reals, bit-vectors, sequences, sets, multisets, infinite sequences and sets, induction, co-induction, and calculational proofs. Verification obligations are discharged automatically, given sufficient specification. Dafny uses some program analysis to infer many specification assertions, reducing the burden on the user of writing specifications. The general proof framework is that of Hoare logic. Dafny builds on the Boogie intermediate language which uses the Z3 automated theorem prover for discharging proof obligations. (en) Dafny es un lenguaje compilado imperativo enfocado a C# y permite especificación formal a través de precondiciones, postcondiciones, invariantes de bucles y variantes de bucles. El lenguaje combina ideas principalmente de los paradigmas funcional e imperativo, e incluye soporte limitado para Programación Orientada a Objetos. Las características incluyen genéricos, asignación dinámica, tipos de datos inductivos y una variación de lógica de separación conocida como marcos implícitos dinámicamente para inferencia de efectos colaterales. Dafny fue creado por Rustan Leino en Microsoft Research tras su trabajo previo desarrollando ESC/Modula-3, ESC/Java, y Spec#. Dafny es empleado ampliamente en la enseñanza y aparece regularmente en competiciones de verificación de software (p. ej. VSTTE'08, VSCOMP'10, COST'11, y VerifyThis'12). Dafny fue diseñado para proporcionar una introducción simple a ala especificación formal y la verificación y ha sido empleado ampliamente en la enseñanza. Dafny sigue la línea de muchas herramientas previas, incluyendo SPARK/Ada, ESC/Java, Spec#, Whiley, Why3 y Frama-C. Estas herramientas dependen del uso de probado automático de teoremas para desempeñar obligaciones de prueba, a diferencia de, por ejemplo, aquellas basadas en tipos dependientes (p. ej. Idris, Agda) que requieren mayor intervención humana. Dafny se compila en el lenguaje intermediario Boogie, que usa el probador automático de teoremas Z3 para desempeñar obligaciones de prueba. (es) Dafny C# lengoaiara bideratuta dagoen eta , , begizta-inbarianteen eta bidez espezifikazio formala bermatzen duen programazio lengoaia konpilatu inperatiboa da. Lengoaiak nagusiki paradigma funtzional eta inperatiboen ideiak konbinatzen ditu, eta objektuetara bideratutako programaziorako euskarri mugatu bat eskaintzen du. Lengoaiaren ezaugarrien artean hauek dira aipagarrienak: klase generikoak, esleipen dinamikoa, datu-mota induktiboak eta aldakuntza bat, alboko efektuekin arrazoitzeko balio duen eta marko dinamikoki inplizituak izena duena. Dafny lengoaia Rustan Leinok sortu zuen -en , eta -en garapenean lan egin ondoren. Dafny irakaskuntzan oso erabilia da eta softwarearen egiaztapeneko txapelketetan maiz agertzen da (adb. VSTTE'08, VSCOMP'10, COST'11 eta VerifyThis'12). Dafny espezifikazio formalerako eta egiaztapenerako sarrera erraz bat eskaintzeko diseinatu zen. Dafny-k aurretik sortutako hainbat erremintaren ildoari jarraitzen dio, erreminta horien artean , ESC/Java, Spec#, , Why3 eta daude. Erreminta horiek teoremen frogapen automatikoaren menpe daude frogapenak egin ahal izateko, adibidez, giza parte-hartze handiagoa behar duten mota dependenteetan onarritutakoak (adb. , ). Dafny-n idatzitako programak konpilatzeko Boogie erabiltzen da, erabiltzen duena. (eu) |
| dbo:developer | dbr:AWS dbr:Microsoft_Research |
| dbo:latestReleaseDate | 2022-07-14 (xsd:date) |
| dbo:latestReleaseVersion | 3.7.2 |
| dbo:license | dbr:MIT_License |
| dbo:thumbnail | wiki-commons:Special:FilePath/Dafny_logo.jpg?width=300 |
| dbo:wikiPageExternalLink | https://dafny.org/ https://github.com/dafny-lang/dafny https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ |
| dbo:wikiPageID | 56073623 (xsd:integer) |
| dbo:wikiPageLength | 13396 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1109644898 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:AWS dbr:Proof_assistant dbr:Python_(programming_language) dbr:NOP_(code) dbr:Design_by_contract dbr:ESC/Java dbr:Loop_invariant dbc:Microsoft_free_software dbc:Software_using_the_MIT_license dbr:Mathematical_induction dbr:Object-oriented_programming dbr:Separation_logic dbr:Go_(programming_language) dbr:Structural_induction dbr:Z3_Theorem_Prover dbr:Functional_programming dbr:Static_program_analysis dbr:C_Sharp_(programming_language) dbr:Type_system dbc:Microsoft_programming_languages dbr:Formal_specification dbr:Lemma_(mathematics) dbr:Functional_programming_language dbr:Proof_by_exhaustion dbr:Pure_function dbr:JavaScript dbr:Java_(programming_language) dbc:Academic_programming_languages dbc:Proof_assistants dbc:Statically_typed_programming_languages dbr:Access_modifiers dbc:Microsoft_Research dbc:Experimental_programming_languages dbr:Hoare_logic dbc:Programming_languages_created_in_2009 dbr:Springer_Science+Business_Media dbr:Intermediate_language dbr:Microsoft_Research dbr:Loop_variant dbr:MIT_License dbr:Side_effect_(computer_science) dbr:Imperative_programming dbr:Programming_language dbr:Postconditions dbr:Compiled_programming_language dbr:Preconditions |
| dbp:designer | K. Rustan M. Leino (en) |
| dbp:developer | Microsoft Research, AWS (en) |
| dbp:fileExt | .dfy (en) |
| dbp:latestReleaseDate | 2022-07-14 (xsd:date) |
| dbp:latestReleaseVersion | 3.700000 (xsd:double) |
| dbp:license | dbr:MIT_License |
| dbp:logo | Dafny logo.jpg (en) |
| dbp:logoSize | 128 (xsd:integer) |
| dbp:name | Dafny (en) |
| dbp:paradigm | dbr:Functional_programming_language dbr:Imperative_programming |
| dbp:typing | dbr:Type_system |
| dbp:website | https://dafny.org/ |
| dbp:wikiPageUsesTemplate | dbt:Cite_book dbt:Cn dbt:Infobox_programming_language dbt:Microsoft_FOSS dbt:Microsoft_Research dbt:Microsoft_development_tools dbt:Reflist dbt:Short_description dbt:Start_date_and_age dbt:Unreferenced_section |
| dct:subject | dbc:Microsoft_free_software dbc:Software_using_the_MIT_license dbc:Microsoft_programming_languages dbc:Academic_programming_languages dbc:Proof_assistants dbc:Statically_typed_programming_languages dbc:Microsoft_Research dbc:Experimental_programming_languages dbc:Programming_languages_created_in_2009 |
| rdf:type | owl:Thing dbo:Language schema:Language wikidata:Q315 wikidata:Q9143 dbo:ProgrammingLanguage |
| rdfs:comment | Dafny is an imperative and functional compiled language that compiles to other programming languages, such as C#, Java, JavaScript, Go and Python. It supports formal specification through preconditions, postconditions, loop invariants, loop variants, termination specifications and read/write framing specifications. The language combines ideas from the functional and imperative paradigms; it includes 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#. (en) Dafny es un lenguaje compilado imperativo enfocado a C# y permite especificación formal a través de precondiciones, postcondiciones, invariantes de bucles y variantes de bucles. El lenguaje combina ideas principalmente de los paradigmas funcional e imperativo, e incluye soporte limitado para Programación Orientada a Objetos. Las características incluyen genéricos, asignación dinámica, tipos de datos inductivos y una variación de lógica de separación conocida como marcos implícitos dinámicamente para inferencia de efectos colaterales. Dafny fue creado por Rustan Leino en Microsoft Research tras su trabajo previo desarrollando ESC/Modula-3, ESC/Java, y Spec#. Dafny es empleado ampliamente en la enseñanza y aparece regularmente en competiciones de verificación de software (p. ej. VSTTE'08, (es) Dafny C# lengoaiara bideratuta dagoen eta , , begizta-inbarianteen eta bidez espezifikazio formala bermatzen duen programazio lengoaia konpilatu inperatiboa da. Lengoaiak nagusiki paradigma funtzional eta inperatiboen ideiak konbinatzen ditu, eta objektuetara bideratutako programaziorako euskarri mugatu bat eskaintzen du. Lengoaiaren ezaugarrien artean hauek dira aipagarrienak: klase generikoak, esleipen dinamikoa, datu-mota induktiboak eta aldakuntza bat, alboko efektuekin arrazoitzeko balio duen eta marko dinamikoki inplizituak izena duena. Dafny lengoaia Rustan Leinok sortu zuen -en , eta -en garapenean lan egin ondoren. Dafny irakaskuntzan oso erabilia da eta softwarearen egiaztapeneko txapelketetan maiz agertzen da (adb. VSTTE'08, VSCOMP'10, COST'11 eta VerifyThis'12). (eu) |
| rdfs:label | Dafny (en) Dafny (es) Dafny (eu) |
| owl:sameAs | wikidata:Dafny dbpedia-es:Dafny dbpedia-et:Dafny dbpedia-eu:Dafny https://global.dbpedia.org/id/4YCb7 |
| prov:wasDerivedFrom | wikipedia-en:Dafny?oldid=1109644898&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/Dafny_logo.jpg |
| foaf:homepage | https://dafny.org/ |
| foaf:isPrimaryTopicOf | wikipedia-en:Dafny |
| foaf:name | (en) Dafny (en) |
| foaf:page | https://dafny.org/ |
| is dbo:wikiPageRedirects of | dbr:Dafny_(programming_language) |
| is dbo:wikiPageWikiLink of | dbr:Bosque_(programming_language) dbr:Microsoft_and_open_source dbr:Timeline_of_programming_languages dbr:Whiley_(programming_language) dbr:Dafny_(programming_language) dbr:Grigore_Roșu dbr:Interference_freedom |
| is foaf:primaryTopic of | wikipedia-en:Dafny |
