Presentación | Participantes | Bibliografía (DML-E) | Bibliografía adicional | Enlaces de interés | Otros proyectos DML | Ayuda  
INICIO | 28 de marzo de 2024
  

Cocktail: a tool for deriving correct programs.

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.
Icono pdf Acceso al artículo completo
Equipo DML-E
Instituto de Ciencias Matemáticas (ICMAT - CSIC)
rmm()icmat.es