Cocktail: a tool for deriving correct programs.
Michael Franssen; Harrie De Swart
RACSAM (2004)
- Volume: 98, Issue: 1, page 95-111
- ISSN: 1578-7303
Access Full Article
top
Abstract
topHow to cite
topFranssen, Michael, and De Swart, Harrie. "Cocktail: a tool for deriving correct programs.." RACSAM 98.1 (2004): 95-111. <http://eudml.org/doc/41041>.
@article{Franssen2004,
abstract = {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.},
author = {Franssen, Michael, De Swart, Harrie},
journal = {RACSAM},
language = {eng},
number = {1},
pages = {95-111},
title = {Cocktail: a tool for deriving correct programs.},
url = {http://eudml.org/doc/41041},
volume = {98},
year = {2004},
}
TY - JOUR
AU - Franssen, Michael
AU - De Swart, Harrie
TI - Cocktail: a tool for deriving correct programs.
JO - RACSAM
PY - 2004
VL - 98
IS - 1
SP - 95
EP - 111
AB - 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.
LA - eng
UR - http://eudml.org/doc/41041
ER -
NotesEmbed ?
topYou must be logged in to post comments.
To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.