Reporte técnico
Taller de especificación, construcción y verificación formales de Programas :propuesta y experiencias
Fecha
2005Registro en:
LUNA, C. "Taller de especificación, construcción y verificación formales de Programas :propuesta y experiencias". Reportes Técnicos 05-04. UR. FI – INCO, 2005.
0797-6410
Autor
Luna, Carlos
Institución
Resumen
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.