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)