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

Adventi Menger-szivacs

Az egész azzal kezdődött, hogy évekkel ezelőtt, amikor még nem is dolgoztam az ISC-nél, megkapták a kollégák a névjegykártyáikat, amikre persze semmi szükségük nem volt (egyébként azóta sincs). Mivel ez egy ilyen kreatív bagázs, csináltak belőle egy Menger-szivacsot, illetve annak egy elsőszintű közelítését. Ez ugyebár húsz darab, névjegykártyákból hajtogatott kockából áll.

Aztán pár hete, amikor megyek be, kiderült, hogy Maya és Encsé elkezdte a régi szivacs köré építeni a másodrendű közelítést, vagyis még tizenkilenc ugyanakkora, lyukas kockát. Ez már emberes feladat volt, a fél Netvisor hordta a felesleges névjegykártyákat, végül Zapéval és velem kiegészülve négyen fejeztük be, összesen három nap alatt (persze a három nap közben dolgoztunk is, ez nem a tiszta játékidő). A végeredmény elég impozáns lett:

Ezt az ötletet gondoltuk tovább Vikivel, és kitaláltuk, hogy készítünk egy hasonló adventi naptárat, persze ünnepi színes papírból:

Mivel 20 kis kocka van a nagyban, ezért még négyre szükségünk volt, hogy végül mind a 24 napra el tudjunk rejteni benne csokikat. Ezeket körben a tetejére raktuk, mert így oldalra lelógnak, és tök jól néznek ki.

A legnehezebb része a feladatnak az volt, hogy ne felejtsünk el minden dobozba berakni két kis csokit ahogy építjük, mert utólag nehéz lett volna pótolni. Nagyrészt belga csokit raktunk bele, kagylókat meg keserűcsokit meg narancsosat meg minden finomságot, közémixelve egy kis Rafaellót meg Rochét, hogy minden napra jusson valami meglepetés.

És most megyünk, és kibontjuk az első dobozt!

Update: Kikockáztam Encsét a fenti fotóból

Pierre Basieux: Top 7

Kicsit kiakasztott Pierre Basieux Top 7 című könyve, amely arra vállalkozik, hogy a Clay Intézet-féle milliódolláros matematikaproblémákat mutassa be. Mivel olvasmányos, ismeretterjesztő módon van megírva, gondoltam majd odaadom apámnak. Elkezdtem olvasni, és csak a baj van vele.

Előszöris maga a kontent. Bár a bevezetőben maga a szerző emlékezik meg róla, hogy a matematikához nem vezet királyi út, sokszor áldoz fel lényeges részleteket a közérthetőség oltárán. Például rögtön az első fejezetben képes a számhalmazok bemutatásában a valós számokat úgy bevezetni, mint x²-2 jellegű polinomok gyökeit. Mintha ℝ algebrai bővítése lenne ℚ-nak...

Aztán meg maszatol és összemos dolgokat -- például Gödel nemteljességi tételét a P = NP kérdésével. Az utolsó fejezetben, ami egyéb, mai napig megoldatlan kérdésekről szól, felveti, hogy senki sem konstruált még jólrendezést a valós számokhoz, pedig ilyen létezik. Namármost a jólrendezési "tétel" ekvivalens egy korábbi vendégünkkel, a kiválasztási axiómával, úgyhogy alapvetően nem érti a problémát, aki konstruktív megoldást akar -- hiszen ha ilyen létezne, pont a kiválasztási axiómára nem lenne szükség...

Bognár János silány magyar fordítása és az igénytelen kiállítás jól illeszkedik a könyv színvonalához. A fejezetek számozása teljesen elcseszett (valószínűleg egyszerűen \chapter*-ot használtak \chapter helyett a LaTeX forrásban), emiatt minden ábra és egyenlet számozása olyan, mintha a 0. fejezetben lenne, így hát az ötödik fejezetben találjuk a 0.18.. ábrát (így, két ponttal...), és a lábjegyzetek számozása is egészen 105-ig folyamatos. A fordítás pedig nem terjedt ki például a címekre, így aztán egy helyen a könyv hivatkozik Douglas Adams Per Anhalter durch die Galaxis című művére, ami persze a Galaxis útikalauz stopposoknak akart lenni. Néhány mondat pedig a fordítás eredményeképpen teljesen értelmetlen lett.

Az egyetlen vigasz, hogy a könyvet alig ezer forintért vettem, egy 50%-os akcióban.

Hacktivity 2008

Encsé hívta fel a figyelmemet, hogy most lesz az idei Hacktivity, amelyről ő már tavaly is tudósított. Átnéztem a programot, és cím alapján sok előadás igérkezett érdekesnek. Meg a hekkelős játékra is kiváncsi voltam.

Az előadások végül nagyon változó színvonalúak voltak: volt közte pár teljesen content-less (pl. az XSS-előadást ilyen szinten én is meg tudtam volna tartani úgy, hogy nem is értek hozzá), a kvantumkriptográfiai előadás egészen addig volt jó, amig ki nem derült, hogy az előadó nem érti a kérdésemet.

Volt viszont pár tényleg jó előadás is, ottvolt egy FPGA-val MD5-öt törő srác, állati érdekes volt az alacsonyszintű wifidriver-törés (buffer overrunt okozó AP advertising beacon csomagokkal), pedagógiailag nézve pedig a szivárványtáblás előadás vitte a prímet.

Ami meg a hekkelős wargame-et illeti, tavaly ugye le-DoSolták a pontszámokat nyilvántartó gépet, idén meg kb. félóránként tartottak amatőr félórat... Encsé kollégával együtt feszültünk neki a feladatoknak. Volt köztük egy-két vállalható, volt néhány, ami jópofa lett volna, csak sajnos általában nem működtek (az pl. elég jellemző volt az egészre, amikor odamentünk a rendezőkhöz a 10. feladathoz megszerzett jelszavunkkal hogy nem fogadja el a rendszer, erre kiderült hogy a kétszámjegyű feladatokhoz nem működik és kicsit még faragni kellett). Aztán volt egy pár SQL injection-ös, az nagyon nem az én világom, úgyhogy ezekkel Encsé próbálkozott.

Aztán persze az lett a dolog vége, hogy fölényesen megnyertük. Kaptunk egy Linksys wifi routert meg egy külső merevlemezt, majd holnap szétosztjuk. Viszont ami vicces volt, hogy utána odajöttek ketten is hogy elkérjék az email-címemet mindenféle ilyen hálózati biztonsági munkákkal, pedig baromira nem értek én ezekhez, meg kedvem sincs, el is hajtottam őket azzal, hogy én inkább programozó vagyok...