Quickstart

Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Auto

Light

Rust

Coal

Navy

Ayu

Quickstart

Coma (which stands for Continuation Machine) is an<br>Intermediate Verification Language implemented as a plugin<br>in the Why3 platform.

Specification annotations in Coma take the form of assertions mixed with<br>the executable program code. A special programming construct representing the<br>abstraction barrier is used to separate, inside a subroutine, the “interface” part<br>of the code, which is verified at every call site, from the “implementation” part,<br>which is verified only once, at the definition site. In comparison with traditional<br>contract-based specification, this offers us an additional degree of freedom, as we<br>can provide separate specification (or none at all) for different execution paths.

Continuation-passing style allows us to devise an extremely economical abstract<br>syntax for a generic verification language.<br>This syntax is flexible enough to naturally express conditionals, loops,<br>(higher-order) function calls, and exception handling. It is type-agnostic and<br>state-agnostic, which means that we can combine it with a wide range of type<br>and effect systems.

Schiele — Four Trees