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.
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.
@article{urn:eudml:doc:41041,
title = {Cocktail: a tool for deriving correct programs.},
journal = {RACSAM},
volume = {98},
year = {2004},
pages = {95-111},
zbl = {1103.68464},
language = {en},
url = {http://dml.mathdoc.fr/item/urn:eudml:doc:41041}
}
Franssen, Michael; De Swart, Harrie. Cocktail: a tool for deriving correct programs.. RACSAM, Tome 98 (2004) pp. 95-111. http://gdmltest.u-ga.fr/item/urn:eudml:doc:41041/