Cocktail: A tool for deriving correct programs
Proof theory and constructive mathematics (03F99) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60)
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.
- scientific article; zbMATH DE number 2177628
- scientific article; zbMATH DE number 194510
- The correctness-by-construction approach to programming
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A program refinement tool
This page was built for publication: Cocktail: A tool for deriving correct programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2711194)
