Ha B-ben szeretnénk fejleszteni, az eszközeinknek a következő feladatokat kell ellátniuk:
- Szintaktikus elemzés (beleértve a változók típusának levezetését).
- Szemantikus elemzés: bizonyítandó tételek generálása.
- A tételek bebizonyítására automatikus és/vagy interaktív felület.
- Az implementációból kód generálása.
A B-módszer alkalmazására vannak professzionális keretrendszerek, amik a szoftverfejlesztés összes fázisát támogatják: a követelmények formális megfogalmazását, a tervezést, a B nyelvű implementáció elkészítését, a bizonyítandó lemmák generálását és bebizonyítását, végül a bizonyítottan helyes kód generálását. Két ilyen keretrendszer az Atelier-B és a B-Toolkit. Ezeket a rendszereket ipari környezetekben használják.
Ezek helyett három ingyenes programot is lehet használni: a B4free-t, a Click'n'Prove-ot és a jBTools-t.
A B4free kezeli a projekteket, szintaktikusan és szemantikusan elemzi a kódot, generálja a bizonyítandó lemmákat, tartalmazza a bizonyítókat és C forráskódot generál az implementációból(azaz ellátja az összes feladatot). Ez egy konzolos program. Ingyenesen letölthető innen, de a letöltéshez regisztrálni kell az oldalra.
A Click'n'Prove grafikus interfészt nyújt a B4free-hez. Az XEmacs szövegszerkesztőben fut, elég kényelmesen lehet vele végezni az interaktív bizonyításokat. (A B4free-t Click'n'Prove-on keresztül érdemes használni). Ingyenesen letölthető innen, ahol található egy telepítési útmutató és egy tutorial a B4free-hez és a Click'n'Prove-hoz. A program forráskódjához is hozzáférünk.
A jBTools Java-kódot generál a B-implementációkból, tehát az 1. és 4. feladatot látja el (az elsőt azért, mert természetesen arra is szükség van a 4-hez). A három közül ez a legkevésbé kiforrott, sajnos nem minden programot tud lefordítani, amit a B4free jóváhagy. Ingyenesen letölthető innen egy jEdit-be integrálódó plugin formájában. Letölthető a forráskódja is, aminek a segítségével konzolosan is lehet használni, jEdit nélkül.