Cocktail II

M.G.J. Franssen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

Cocktail II is an interactive tool for deriving programs from specifications. Instead of verifying a program after it was constructed, Cocktail II aids the goal oriented derivation of a program. First, the user provides a pre- and postcondition. Then, the program to fill the gap between these condition is constructed by manually inserting statements between them. The tool computes the sub specifications of the new gaps, which can then be manually refined further. Finally, when a precondition of a gap implies its postcondition, the gap can be closed. Cocktail II also provides support for constructing the required proof. The program is complete when all gaps are closed.
Original languageEnglish
Title of host publicationProceedings of the 3rd International Workshop on Invariant Generation (WING 2010), July 21, 2010, Edinburgh, UK
EditorsA. Voronkov, L. Kovacs, N. Bjorner
Place of PublicationS.l.
PublisherEasyChair
Pages92-93
Publication statusPublished - 2012
Eventconference; WING 2010 -
Duration: 1 Jan 2012 → …

Publication series

NameEPiC Series
Volume1
ISSN (Print)2040-557X

Conference

Conferenceconference; WING 2010
Period1/01/12 → …
OtherWING 2010

Fingerprint Dive into the research topics of 'Cocktail II'. Together they form a unique fingerprint.

  • Cite this

    Franssen, M. G. J. (2012). Cocktail II. In A. Voronkov, L. Kovacs, & N. Bjorner (Eds.), Proceedings of the 3rd International Workshop on Invariant Generation (WING 2010), July 21, 2010, Edinburgh, UK (pp. 92-93). (EPiC Series; Vol. 1). EasyChair.