Cocktail is a tool for interactive development of imperative programs and their correctness proofs. It combines a Hoare-logic with an interactive theorem prover based on a typed lambda-calculus and an automated theorem prover (ATP) based on the tableau method. It is intended for use in an educational setting.

At present, most tools for correct programming support functional or logical programming paradigms. However, in practice, most programs are written using procedural languages (including object-oriented languages) like Pascal, C/C++ or Java. Tools for procedural languages usually provide only syntactical support.

The essence of algorithms in procedural languages can be expressed in Dijkstra's guarded command language (GCL), for which there is a formal basis that allows semantical support. In fact, programs written in GCL can be derived from their specification. So far, there are only few tools that support this approach to programming.

The goal of Cocktail is to provide semantical support for deriving programs from their specifications. The system is intended for programmers in an educational setting. Also, the system is set up to be extensible, flexible and easy to experiment with.

Cocktail is written entirely in Java and provides a modern graphical user interface. Proofs are graphically represented in Fitch-style natural deduction and can be manipulated by drag-and-drop operations. Forward reasoning is supported to a certain extend, allowing the user more flexibility than backward reasoning only.

Cocktail has been developed by Michael Franssen as part of his Ph.D. thesis work. For more information about Cocktail, see the Cocktail homepage.