Enseñando métodos formales con COQ
En este trabajo presentamos una propuesta para apoyar la enseñanza de métodos formales en una currícula de grado (y postgrado) 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...
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Objeto de conferencia |
| Lenguaje: | Español |
| Publicado: |
2006
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/19181 |
| Aporte de: |
| Sumario: | En este trabajo presentamos una propuesta para apoyar la enseñanza de métodos formales en una currícula de grado (y postgrado) 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. |
|---|