The B Method for Programmers (Part 2)

In my previous post, I introduced the B method and showed the steps of writing a simple program for finding the n^th element of a sequence satisfying a given predicate p. While you may think the resulting program is correct, we can't just say so and be done with it. The whole point of the B method is that the resulting program can be formally proven correct.

The B software generates 69 so-called proof obligations for the code from the first part. These are assertions about the program actually behaving as specified. For example, let's look at PO69 which asserts that ll is correctly set. Recall first the relevant portion of the specification:

And the invariant of the implementation:

So what we have to prove is that given the preconditions, by the time the loop in the implementation terminates, the invariant makes sure ll is equal to its specified value. This is what's described (somewhat more verbosely) by the actual proof obligation below.

The B Method for Programmers (Part 1)

Last month, I had to use Atelier B, an implementation of the B method, for a university assignment. But what is the B method, and what does programming with B look like in practice?

I'm going to introduce B from the perspective of a traditional programmer. You can find documentation on the web, but most of it is from the viewpoint of designing complex state machines. However, B is also a Pascal-like language than can be used for imperative programming. The big added value of using B is that the resulting program can be proven to be correct. In fact, I first encountered B a year ago while working on my B.Sc. thesis, which was about deriving new correct programs from existing ones.

As for its theoretical backgrounds, B is based on the Hoare-Dijkstra model of imperative programming. I'm not going to delve into it; instead, let's look at a concrete example, and I'll guide you through the process of first writing a formal specification, then creating the implementation (this part), and then proving its correctness (in the next part).

Eliminating magic strings from ELisp's (interactive)

If you hate magic string API's as much as I do, you'll like this macro replacing Emacs's (interactive) declaration. It allows you to rewrite the following function definition:

into the much cleaner form below:

It currenty only supports :pos, :region and strings entered at the prompt, but the code is trivial to extend to other initializers.

Type inference for CLazy

CLazy now features Hindley-Milner type inference, the type calculus all the cool guys use. For example, given the following recursive definition of map:

the type inference engine of CLazy correctly reconstructs the following type signature:

Still to come: virtual functions like Haskell's typeclasses. The plan is to define abstract functions like (+ a) :: (fun a a a) and collect requirements for functions in the form of "this function has type (fun a b) as long as an overload for (+ a) exists".

CLazy interpreter and compiler

CLazy is my toy functional programming language featuring a Lisp-like syntax, lazy evaluation, and not much else at the moment. To get a taste of it, here's the definition of map in CLazy, using pattern matching:

(deftype list (t)
  nil
  (cons t (list t)))
   
(defun map (f nil)         nil)
(defun map (f (cons x xs)) (cons (f x) (map f xs)))

I've written the interpreter (in Lisp) back in November, and now I had this idea of writing a compiler. This compiler, instead of generating e.g. x86 assembly code, generates C# which is then compiled into .NET IL.

To do the actual code generation, instead of outright outputting text, the compiler (also written in Lisp) generates an s-expr representation of C# code. For example, the code generated for the type list, as defined above, is represented as the following: