| dbo:abstract
|
- 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 , 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 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 , 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)
|
| rdfs:comment
|
- 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 , 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 (es)
- 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 , 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 (es)
|
