The B Method for Programmers (Part 1)

16 February 2010 (programming language math correctness)

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).

The problem that we're going to solve is finding elements of a sequence satisfying a given predicate. More precisely, we're interested in finding exactly the n^th such element, for a given value of n. Since the whole point of B is that whatever program we end up writing can be checked to solve the problem, we need to formalize this problem in a way that B understands, so let's first use mathematical notation. What we want to do is given an integer interval A := {a, a+1, .., b} ⊆ ℤ , a number n∈ℕ⁺ and a predicate p: ℤ → 𝕃, either find i∈A such that p(i) and |{k∈{a, a+1, ..., i-1} | p(k)}| = n-1, or determine that |{k∈A|p(k)}|<n.

Please take a minute to read that specification again and determine that it is indeed a formulation of the problem that we set out to solve. As with any formal system, we can only hope to get results as good as the specification.

Now let's write this down in B syntax (I've added some typing constraints as well):

Due to obscure technical reasons, variable names in B must be at least two characters long, which is why all the names seem so strange in the above code. INT does not actually mean ℤ in the above code (that would be INTEGER), instead, it is the subset of integers that are representable with 32 bits. card is the cardinality operator for finite sets. The rest of the above code should be self-explanatory.

Since this introduction is targeted at programmers, I'm taking for granted that you already have a general idea of how to solve this problem. Below is the B program that I wrote. Note how ii is initialized to aa-1, which is why we previously included the seemingly unneeded requirement aa-1 ∈ INT in the specification.

Except, this isn't actually B code above. Why? First of all, a checker would need to solve the halting problem to see if the above code returns anything at all, much less a correct answer. So we need to help the checker in this. And secondly, due to the possible complexity of the behaviour of loops, we need to provide a loop invariant for the checker.

To prove termination, B requires loops to have a VARIANT expression, which is an integer expression that evaluates to a non-negative value at the beginning of each iteration, and each iteration then decrements its value. Since the natural numbers are well-ordered by ≤, this ensures a finite number of iterations, and hence, termination. In this case, since we step through the interval one by one in order, the number of elements remaining, bb-ii, is a good variant function.

Coming up with a good invariant is a much harder task. The invariant is a predicate that is true at the start and end of every iteration. All that is known about the effect of the loop is that after it has finished, the invariant is true and the loop condition is false.

Obviously, we could choose a meaningless statement like 1=1 and it would be easy to guarantee its truthness. However, it wouldn't tell a lot about the actual effect of the loop, and thus, would make it impossible to prove that the calculated results match the specification.

A good invariant captures the way the loop works by specifying the sub-problem that is solved by previous iterations. With each iteration, this sub-problem gets closer and closer to the original problem, and hopefully, by the time the loop condition evaluates to false, the solved sub-problem is detailed enough that it also entails a solution to the problem. In our sample, the invariant we're going to come up with is actually the conjunction of several important properties:

• ii iterates over the interval aa..bb. Actually, since the invariant has to hold even at the start of the first iteration, we're going to go with ii ∈ (aa-1)..bb.
• cc is always set to the number of elements seen so far that satisfy the predicate: cc = card({kk | kk ∈ aa..ii ∧ pp(kk) = TRUE}). We also know that it never exceeds nn: cc ∈ 0..nn.
• ll gets set to TRUE at the instant we find the nn-th element satisfying the predicate. This is a tricky one to formalize. First, we'll say that ll is TRUE iff the slice of aa..ii contains exactly nn occurances: ll = bool(card({kk | kk ∈ aa..ii ∧ pp(kk) = TRUE}) = nn). We use the bool operator of B as the connection between the meta-level of predicates on the state and the meta-level of (boolean) values.
• When ll is set to TRUE, ii should hold the index of an element satisfying the predicate: ll = TRUE ⇒ ii ∈ aa..bb ∧ pp(ii)=TRUE
• We will also include some seemingly redundant assertions that will help us when writing the proofs.

Here's the finished implementation of find_nth:

And now comes the tricky part. Everything we've written so far, we could have written in any traditional imperative programming language. What B provides us with is the ability to formally prove the correctness of the above program. Correctness in this case means that the implementation ensures that for any input satisfying the preconditions of the specification, the program terminates and the results fulfill the requirements.

So what we set out to prove is that for any actual values of the variables aa, bb and pp that have correct types (as seen in the specification), the above program terminates and sets ll and ii correctly.

Unlike some formal methods like functional programming with dependent types, programs and proofs are not intertwined in B. Instead, developing a B program is a three-step process: first, the specification is written, then the actual implementation code. After that, at the click of a button, the B software generates the so-called proof obligations describing, in detail, the required relations between input and output. The third separate step, then, is writing these proofs - which I'm going to explain in the next post.