AmateurB

Embedding formal methods in Clojure since 2016.

Quick Start

Introduction

lisb is a library that embeds the B and Event-B languages as well as the ProB constraint solver and model checker in Clojure. This allows you to programmatically

  • construct constraints in B and solve them using ProB's constraint solving capabilities;
  • construct and output state machines in ProB;
  • transform any B constraint or state machine.

General Concepts

lisb works on four different representation:

  • An internal DSL, such as (b (= :x (+ 1 2))), that represents the constraint x = 1 + 2. This is a representation that is close to Clojure's core language.
  • An intermediate representation (IR), that represents the same constraints, but in a map form. This is harder to write, but easier to process programmatically. The lisb.translation.lisb2ir namespace contains functions to create this IR as well. It is re-exported by lisb.translation.util.
  • A collection of AST nodes that are Java classes generated by the SableCC parser generator tool. This Java object representation is used in order to communicate with ProB's Java API. You do not ever want to actually see this representation, but generate it and pass it on. It can also be transformed into the internal DSL.
  • The B ASCII syntax that would be used in a .mch file. This can be fed into the parser to generate the AST, and the AST's pretty printer can emit this syntax.

Constraint Solving

This small example shows how one can construct a small constraint and solve it:

clj=> (use (quote lisb.core))
nil
clj=> (use (quote lisb.translation.util))
nil
clj=> (eval-ir-formula' (b (= :x (+ 1 2))))
{:x 3}

The internal DSL code will be evaluated and will wield the IR. The IR will be translated into the Java AST, passed to ProB and the constraint will be solved. This is all done by eval-ir-formula'.