A B formális nyelv (B-method, B formal method)

Példák

Az összes példa egy fájlban letölthető innen.

Hello World

A szokásos legegyszerűbb példa:

Specifikáció gép (Hello.mch)
MACHINE Hello OPERATIONS main = skip END
Implementáció gép (Hello_imp.imp)
IMPLEMENTATION Hello_imp REFINES Hello IMPORTS BT_IO OPERATIONS main = writeString("Hello World!") END END

A BT_IO az alapvető kiíró/beolvasó műveletekért felelős. Ennek metódusa a writeString, ami a standard outputra ír. A főprogram egy egyszerű üres program.

A példa letölthető innen.

Array

Egy példa a lehetséges típuskonstrukciókra a jEdit beépített B fordítójához adott példák közül.

Specifikáció gép(Array.mch)
MACHINE ARRAY CONCRETE_VARIABLES T1, T2, T3 INVARIANT T1 ∈ -5..5 → INT & T2 ∈ -5..5 → INT & T3 ∈ (1..2)×(1..2) → BOOL INITIALISATION T1 :∈ -5..5 → INT || T2 :∈ -5..5 → INT || T3 :∈ (1..2)×(1..2) → BOOL OPERATIONS yy, zz ← op (xx) = PRE xx ∈ 1..2 THEN yy :∈ BOOL || zz :∈ INT || T2(3) := 4 END END

3 függvényt deklarál, ezek CONCRETE-ak, azaz definiálni kell őket. A függvény xx-re tesz megkötést, és a visszatérési értéket specifikálja (szorítja meg) típusokra.

Implementáció gép(Array_imp.imp)
IMPLEMENTATION ARRAY_imp REFINES ARRAY INITIALISATION T1 := (-5..5)×{0}; T2 := T1; T3 := {1|->1|->TRUE,1|->2|->FALSE,2|->1|->FALSE,2|->2|->TRUE} OPERATIONS yy, zz ← op (xx) = BEGIN yy := T3(1 |-> xx) ; T2(3) := 4 ; zz := T1(3) END END

Itt meg van adva a konkrét inicializáció (itt kötelező is), és a függvény konkrét leírása, ami megfelel a specifikációnak. Ezt a megfelelést a B típusellenőrzők vizsgálják.

Az ezt felhasználó gép
Specifikáció gép(BUsingArray.mch)
MACHINE BUsingARRAY OPERATIONS main = skip END

Egyszerű üres gép.

Implementáció gép(BUsingArray_imp.imp)
IMPLEMENTATION BUsingARRAY_imp REFINES BUsingARRAY IMPORTS BT_IO, ARRAY OPERATIONS main = VAR rr1, rr2 IN rr1, rr2 ← op (2) ; writeBoolean (rr1) ; writeString ("\n") ; writeInteger (rr2) END END

A gép egyszerűen kiírja a kapott logikai, és egész értéket. A kapott eredmény FALSE és 0.

Egy nagyobb lélegzetű példa. A Singleton (egyke) tervminta megvalósítása gépekkel. Ebből is látható, hogy ugyan nem objektumorientált a láthatóságok így is jól kezelhetőek, és az öröklődés is megoldható így.

A példa letölthető innen.

Singleton

Specifikáció gép(Singleton.mch)
MACHINE SINGLETON CONCRETE_VARIABLES exist, singletonData INVARIANT singletonData∈NAT ∧ exist∈BOOL INITIALISATION singletonData:∈NAT || exist:=FALSE OPERATIONS singletonOp(adat)= PRE adat∈NAT THEN SELECT exist=TRUE THEN singletonData:=adat WHEN exist=FALSE THEN exist:=TRUE || singletonData:=adat END END; data←getSingletonDat = PRE exist=TRUE THEN data:=singletonData END; bbool←isExist = bbool:=exist END

Ez a gép felel meg a Singleton osztálynak. Adott benne egy adat, ehhez hasonlóan bármennyi adattagot fel lehet használni. Az osztály objektumának létezését, vagy nem létezését itt egy boolean típusú adattaggal helyettesítjük. Ezekre az implementált programban is szükség lesz, így CONCRETE_VARIABLES részben deklaráljuk őket. Kezdetben nem létezik példányosított osztály, így az "exist" hamis értékű, az adattag tetszőleges.

3 művelete van a gépnek. Az első kettő az osztály eljárásait helyettesíti (művelet a Singleton adattagján, jelen esetben értékadás, valamint lekérdezés), az utolsó megadja, hogy már létezik-e az Egyke (ez utóbbi egy egyszerű lekérdezés). Az adattag lekérdezését csak létező Egyke esetén értelmezzük, ekkor ez is egyszerű adattag lekérdezés. Az adaton értelmezett művelet ebben a példában egy egyszerű értékadás, azzal a módosítással, hogy ha még nem létezett az Singleton, akkor az "exist" értékét igazra állítja.

Ebben az esetben nem lett volna szükség két esetre bontani a műveletet, de ha nem egyszerű értékadás történik, akkor szükség lehet erre. A szimultán értékadást az implementáció során ki kell küszöbölni.

Implementáció gép(Singleton_imp.imp)
IMPLEMENTATION SINGLETON_imp REFINES SINGLETON INITIALISATION exist:=FALSE; singletonData:∈NAT OPERATIONS singletonOp(adat)= BEGIN IF exist=TRUE THEN singletonData:=adat ELSE BEGIN exist:=TRUE; singletonData:=adat END END END; data←getSingletonDat = BEGIN data:=singletonData END; bbool←isExist = BEGIN bbool:=exist END END

Az előzőleg definiált absztrakt alapgép implementációja. Az inicializációt meg kell ismételni, és a műveleteket új formában kell megadni (felül is lehetne definiálni ezeket). Itt nem szerepelhetnek nem determinisztikus műveletek, és szimultán értékadások.

Az eljárások implementációja:

Értékadás: az alapprogrambeli SELECT-es szerkezetet itt más programnyelvekből ismertebb IF-THEN-ELSE szerkezettel írjuk le, a szimultán értékadást pedig több egyszerű értékadást szekvenciájaként (a sorrend jelen esetben nem számít).

A két másik művelet egyszerű lekérdezés az implementációnak megfelelő szintaxissal.

A feltételeket implementált gépeknél nem kell kiírni. A fordító az alapgépek alapján ellenőriz.

Specifikáció gép(Singintface.mch)
MACHINE SINGINTFACE SEES SINGLETON OPERATIONS singletonOperation(adat)= PRE adat∈NAT THEN skip END; data←getSingletonData = data:=0 END

Az interface látja a Singleton gépet, a SEES működése biztosítja, hogy ez a gépet akár SEES, akár INCLUDE tagban szerepel, csak ő példányosodik esetleg többször a Singleton gép nem, abból mindig csak 1 marad.

A két művelet az Egyke gép műveleteinek lehetséges interfaceket deklarálnak (a lekérdezésnél vissza kell adni valamilyen értéket, hogy a visszatérési érték típusát meg lehessen határozni, ezért adok vissza 0-t (NAT típus)).

Specifikáció gép(Singintface.mch)
IMPLEMENTATION SINGINTFACE_imp REFINES SINGINTFACE IMPORTS SINGLETON OPERATIONS singletonOperation(adat)= BEGIN singletonOp(adat) END; data←getSingletonData = BEGIN data←getSingletonDat END END

Az előző gép megvalósítása. Inicializálja a Singleton gépet. A műveleteknek adhat egy új külső felületet. Jelen esetben ezek a felületek egyszerűen csak meghívják az Egyke megfelelő műveleteit, de itt bármilyen változtatás, akár eltérő paraméterezés is lehetséges.

A példa letölthető innen.

Példa specifikációra és a bizonyítandó tételek generálására

Az alábbiakban mutatunk egy példát a specifikációra és arra, hogy milyen lemmák generálódnak belőle, ha a B4free programot használjuk.

A Proof Obligation Generator a helyettesítésekkel definiált szemantika segítségével generálja a bebizonyítandó lemmákat. A B-módszer által meghatározott (a szemantikából következő) lemmákat a lehető legegyszerűbb alakra hozza. A legegyszerűbb esetekben maga a Proof Obligation Generator is beláthatja egy lemmáról, hogy teljesül, például, ha az egyszerűsítések során a formula az azonosan igazra egyszerűsödik.

A forráskód:

MACHINE mch VARIABLES rfree INITIALISATION rfree := 1..5 /* Kezdetben az {1,2,3,4,5} halmaz lesz az rfree. */ INVARIANT rfree ⊆ 1..10 /* Az rfree a mindig az 1..10 halmaz egy részhalmaza lesz. A typechecker ebből tudja kikövetkeztetni az rfree típusát. */ OPERATIONS alloc(r) = /* Egy olyan művelet, aminek egy paramétere van.*/ PRE r∈rfree /* Az r paraméter az rfree egy eleme kell legyen a művelet végrehajtásának megkezdésekor. */ THEN rfree := rfree - {r} END END
A példa-specifikációból a Proof Obligation Generator (többek között) két tételt generál.
Első tétel

Közvetlenül az inicializáció után az invariánsnak igaznak kell lennie, ami az [I]P formulával fogalmazható meg, ahol az I az inicializáló értékadás, a P pedig az invariáns.

Esetünkben az állítás a következő:
[rfree := 1..5] (rfree ⊆ 1..10)
A Proof Obligation Generator elvégzi a helyettesítést, így lesz a bizonyítandó lemma végleges alakja:
(1..5 ⊆ 1..10)

Második tétel

A műveleteknek meg kell őrizniük az invariánst.

Általánosan: I ∧ P ⇒ [S]I, ahol az I az invariáns, az S a művelet törzse, P pedig a művelet előfeltétele, ha a művelet PRE-THEN-ELSE alakú (esetünkben ilyen alakú).

A példában a bizonyítandó állítás:
rfree ⊆ 1..10 ∧ r ∈ rfree ⇒ [PRE r ∈ rfree THEN rfree := rfree - r END] (rfree ⊆ 1..10)

A PRE-THEN-END szerkezet definíciója: [PRE P THEN G END] Q ⇔ P ∧ [G] Q

A Proof Obligation Generator elvégzi a helyettesítést és egy triviális egyszerűsítést:
rfree ⊆ 1..10 ∧ r ∈ rfree ⇒ r ∈ rfree ∧ [ rfree := rfree - {r} ] (rfree ⊆ 1..10)
rfree ⊆ 1..10 ∧ r ∈ rfree ⇒ [ rfree := rfree - {r} ] (rfree ⊆ 1..10)
rfree ⊆ 1..10 ∧ r ∈ rfree ⇒ (rfree - {r} ⊆ 1..10)

A bizonyítandó lemma alakja tehát a következő:
rfree ⊆ 1..10 ∧ r ∈ rfree ⇒ (rfree - {r} ⊆ 1..10)

Annak az ellenőrzése, hogy a művelet előfeltétele teljesül-e (esetünkben r∈rfree igaz-e), minden olyan helyen megtörténik, ahol a műveletet meghívjuk, ami azt jelenti, hogy a műveletet felhasználó komponens bizonyításakor olyan bebizonyítandó lemmák fognak generálódni, amik azt állítják, hogy a program adott helyén teljesül az előfeltétel.