Título inglés |
Cocktail: a tool for deriving correct programs. |
Título español |
Cocktail: una herramienta para obtener programas correctos. |
Autor/es |
Franssen, Michael ; De Swart, Harrie |
Organización |
Dep. Comput. Sci. Eindhoven Univ. Technol., Eindhoven, Holanda;Fac. Phil. Tilburg Univ., Tilburg, Holanda |
Revista |
1578-7303 |
Publicación |
2004, 98 (1): 95-111, 19 Ref. |
Tipo de documento |
articulo |
Idioma |
Inglés |
Resumen español |
Cocktail es una herramienta para la obtención de programas correctos a partir de sus especificaciones.
La versión actual de la herramienta tiene una potencia suficiente para su uso con fines educativos. La herramienta proporciona soporte a la lógica de predicados de primer orden multivariada,
formulada en un sistema puro de tipos con constantes paramétricas (CPTS), como el lenguaje de especificación, un sencillo lenguaje While, una lógica de Hoare representada en el mismo CPTS para la obtención de programas a partir de sus especificaciones, y un demostrador automático de teoremas sencillo, basado en tableaux para la verificación de obligaciones de prueba. |
Resumen inglés |
Cocktail is a tool for deriving correct programs from their specifications. The present version is powerful enough for educational purposes. The tool yields support for many sorted first order predicate logic, formulated in a pure type system with parametric constants (CPTS), as the specification language,
a simple While-language, a Hoare logic represented in the same CPTS for deriving programs from their
specifications and a simple tableau based automated theorem prover for verifying proof obligations. |
Acceso al artículo completo |