Taller de especificación, construcción y verificación formales de programas : Propuesta y experiencias

En este trabajo presentamos una propuesta para apoyar la enseñanza de métodos formales en una currícula de grado usando el asistente de pruebas Coq y conceptos del área de Teoría de Tipos. Proponemos un taller de especificación, construcción y verificación de sistemas en los paradigmas de programaci...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Luna, Carlos Daniel
Formato: Objeto de conferencia
Lenguaje:Español
Publicado: 2004
Materias:
Coq
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/22418
Aporte de:
Descripción
Sumario:En este trabajo presentamos una propuesta para apoyar la enseñanza de métodos formales en una currícula de grado usando el asistente de pruebas Coq y conceptos del área de Teoría de Tipos. Proponemos un taller de especificación, construcción y verificación de sistemas en los paradigmas de programación funcional e imperativo, que también abarca el análisis de sistemas críticos: sistemas reactivos y de tiempo real. Describimos algunas experiencias en el desarrollo del taller y planteamos cambios y extensiones.