A ma legelterjedtebb szoftverfejlesztő módszerek általában informális leírásokat adnak a problémára, az elvárásokra a rendszerrel kapcsolatban. Ezek, a leírás bármennyire legyen is strukturált, vagy köznapi, nem képesek absztrakt módon leírni az adott nyelv specifikációját, sőt legtöbbször az implementációt, vagy annak egy részét is mindenképpen tartalmazzák.
A formális nyelvek (köztük a B) arra törekszenek, hogy a specifikációtól kezdve több absztrakciós szinten át teljes és minél formálisabb leírást adjanak, és az egyes absztrakciós szintek jól elkülöníthetőek legyenek.
Egy másik fontos szempont a szoftverfejlesztésnél a helyesség, a specifikációnak megfelelő program előállítása. A formális nyelveknél lehet - éppen a jó elkülöníthetőség miatt - talán a legjobban ellenőrizni a specifikáció és absztrakció egyes szintjei között lépésenként a helyességet. A helyességbizonyító módszerek azonban inkább elméletiek lettek, és nem tudtak a programban minden lépést belátni, az utóbbi 10 évben kerültek ismét előtérbe. A B napjaink egyik legjobb helyességbizonyító rendszere is egyben - mi sem bizonyíthatja ezt jobban mint a párizsi metrórendszer, amit ennek segítségével írtak le, vezető nélkül szinte teljesen automatizálva működik teljesen megbízhatóan.
A B főbb tulajdonságai:
- Formális leírás több absztrakciós szinten.
- Specifikáció, és finomítások több szintű leírása.
- Implementáció teljes elkülönítése a specifikációtól (de azok alapján készül).
- Helyességbizonyítás lépésenként.
- Objektum alapú, de nem objektum elvű, absztrakt gépekből állnak a programok.
A B-módszer a B nyelvet használja a specifikáció, a finomítások és az implementáció leírására.
A nyelv története
Jean-Raymond Abrial 1985-ben mutatta be ezt a formális nyelvet a világnak. A B módszerhez segítették - és a fejlesztésre létrehozott alapítványhoz is csatlakoztak - az akkori legnevesebb formális nyelvekkel foglalkozó matematikusok, programozók, többek között Tony Hoare és Edgar Dijkstra például a leggyengébb előfeltétel vizsgálatával. 1988-ig Oxfordban folyt a fejlesztés, 1922-től már ipari felhasználásra is készült, majd 1994-ben jelentek meg a fejlesztést támogató nyelvi eszközök a B-Core: B-Toolkit nevű és a ClearSy: Atelier B nevű eszköze. 1998-ban épült a fent említett párizsi metró. A nyelv fontosságát mutatják az immáron több éve évente megrendezésre kerülő B illetve BZ konferenciák.