| 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)
|
| 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)
|
