From B Specifications to $\{log$\}$ Forgrams

TL;DR

The paper demonstrates how B specifications can be translated into {log} forgrams to yield executable prototypes that support early validation of requirements. Using the Birthday Book as a running example, it details how invariants, initializations, and operations are mapped to {log} clauses, including typing and the use of extensional sets and set unification. It also covers simulation, symbolic execution, and automated theorem proving via verification-condition generation, illustrating how forgrams can discharge proof obligations and serve as certified prototypes. Overall, the approach provides a bridge from formal specification to executable models, enabling interactive verification and early feedback in software development.

Abstract

In this class notes students can learn how B specifications can be translated into $\{log$\}$ forgrams, how these forgrams can be executed and how they can be proved to verify some properties.