|
Título: Razonando acerca del uso de primitivas de modificación de estados: Un caso de estudio Marco de Trabajo: MAESTRÃA Área de desarrollo: Componentes, Objetos, Arquitecturas y Lenguajes Autor: Andrés Vignaga Contacto: avignaga@fing.edu.uy Día: MIÉRCOLES Hora: 11:30:00 Palabras Claves: Sistemas orientados a objetos, correctitud de programas, verificación formal, teoría de tipos, asistente de pruebas Coq Resumen: El estado de un sistema orientado a objetos puede ser manipulado a un nivel conceptual mediante primitivas de manipulación de estados. Las posibles formas de manipular un estado incluyen tanto consultas como modificaciones. Las primitivas de modificación pueden ser utilizadas para representar el comportamiento de manipulaciones de estados más complejas, como por ejemplo operaciones de sistema. En base a una especificación de dichas primitivas se creó un framework que permite razonar acerca del uso de las mismas. Su posterior formalización en el Cálculo de Construcciones Inductivas, el lenguaje formal del asistente de pruebas Coq, provee una herramienta la cual asiste al usuario del framework en el razonamiento y verifica mecánicamente la correctitud del mismo. En esta presentación se muestra esta herramienta en acción, donde se prueba la correctitud de programas y la preservación de invariantes sobre un caso de estudio no trivial planteado en la bibliografía. |
| Ultima modificacion 5 de Octubre 2004 16:30 |