Általános értékadások és helyettesítések
B-ben a műveletek specifikációi úgynevezett általános értékadások. Az általános értékadások szemantikája pontosan definiálva van helyettesítések segítségével. Ennek a szemantikának a segítségével lehet helyességbizonyítást végezni.
A helyettesítéseket [S] P alakban írjuk le, ahol a P egy predikátum, S pedig egy általános értékadás; a helyettesítés értéke egy újabb predikátum. A helyettesítés szemléletes jelentése, hogy az [S]P predikátum az állapottérnek pontosan azon pontjaira igaz, amelyere igaz az, hogy az S általános értékadás után P biztosan teljesülni fog; vagy formálisabban az ⌈ [S]P ⌉ azon pontok halmaza, amiket az S általános értékadás ⌈ P ⌉-be visz. (A ⌈ P ⌉ a P predikátum igazsághalmaza az állapottérben.)
A helyettesítés tehát definiálva van minden S B-beli általános értékadásra. Például:
- [x:=E] P, ahol x változó, E kifejezés, P predikátum. A helyettesítés elvégzésekor az x összes szabad előfordulását a P-ben E-re cseréljük.
- [x: ∈ S] P ⇔ ∀ y (y ∈ S ⇒ [x:=y] P), ahol x változó, S halmaz, P predikátum. Ez azt fejezi ki, hogy az x bármely S elem értékét veszi is fel, a P-nek teljesülnie kell.
- [x:P] Q ⇔ ∀ y ([x:=y] P ⇒ [x:=y]Q), ahol x változó vagy változólista, P és Q predikátum. Az x:P azt jelenti, hogy az x változó vagy változólista bármilyen értéket megkaphat, amire P teljesül. (Példa a változólistás esetre: (a,b:(a ∈ 0..20 ∧ b ∈ 0..20 ∧ a*b=100)), azaz ,,a és b legyen olyan, hogy mindkettő a 0..20 intervallumban van és a szorzatuk 100'').
- [IF P THEN G ELSE H] Q ⇔ (P ⇒ [G] Q) ∧ (¬ P ⇒ [H] Q), ahol P és Q predikátum, H és G általános értékadás. Szemléletesen: a P teljesülése esetén a G végrehajtásával, ellenkező esetben a H végrehajtásával kell a Q-ba jutnunk.
- [PRE P THEN G END] Q ⇔ P ∧ [G] Q, ahol P és Q predikátum, G általános értékadás. Ezzel a formulával tudjuk felírni a műveletek elő-utófeltételes alakját. Ha egy műveletet ilyen alakban adunk meg, akkor meghívásakor a P-nek, az előfeltételnek teljesülnie kell, és ilyenkor az is igaz, hogy a G-t végrehajtva Q igaz lesz.
- [ANY x WHERE P THEN G END]Q ⇔ ∀ x (P ⇒ [G] Q), ahol az x változó vagy változólista, P és Q predikátum, G általános értékadás. Szemléletesen: minden olyan x-re, amire P teljesül, G végrehajtásával Q-ba kell jutnunk.
Bizonyítás
A bizonyítás során ezen definíciók alapján lesz legenerálva a bizonyítandó tételek.
A B-ben elválasztják egymástól a bizonyítandó tételek generálását és a bizonyítás elvégzését. Ez a két tevékenység valóban teljesen más jellegű, hiszen az elsőt a B szemantikájának ismeretében automatikusan el tudják végezni a fejlesztőeszközök. A bizonyításhoz viszont sokszor emberi beavatkozásra van szükség; ez viszont már nem kapcsolódik szorosan a B-hez, itt "mindössze" elsőrendű logikai formulákról kell belátnunk, hogy az logikailag igazak.
Azt az eszközt, ami a bizonyítandó tételeket generálja a forráskódból, Proof Obligation Generatornak nevezzük. A bizonyítást végző programot egyszerűen bizonyítónak (prover) nevezzük.