Cocktail: A tool for deriving correct programs (Q2711194)

It is given a careful description of a tool for deriving correct programs from their formal specification by simultaneous construction of the program, and its correctness proof based on Dijkstra-Hoare calculus. Part I gives a balanced look to the design goals from the perspective of a programmer, a logician and a system designer. Part II gives an excellent description of the needed theoretical background and formal systems. Part III describes the system and tool design, including a graphical interface. In an appendix a small demo session shows, how a program computing the factorial function can be designed with the tool. The tool is named ``Cocktail'' because the tool implements a cocktail of formalisms, mixing PTSs (pure type systems), tableau methods (from automated proof systems) and Hoare logic. The book is clearly written, pleasantly readable, clearly structured and has amusing illustrations.