B (mjukvaruutveckling)

Kompilatorn i B omvandlar språkets olika element i matematiska formler. Nedan följer exempel på några sådana Substitutioner

Psedu-program	Regel	Beskrivning
[BEGIN G END] Q	${\displaystyle \left[G\right]Q}$	Villkor Q måste uppfyllas medan G execueras.
[PRE P THEN G END] Q	${\displaystyle P\wedge \left[G\right]Q}$	Innan programmet G execuerats måste villkoret P uppfyllas och villkoret Q måste uppfyllas under hela execueringen.
[IF P THEN G ELSE H END] Q	${\displaystyle \left(P\Rightarrow \left[G\right]Q\right)\wedge \left(\neg P\Rightarrow \left[H\right]Q\right)}$	Om villkoret P uppfylls execueras kod G, annars H. Oavsett vilken kod som execueras måste villkor Q uppfyllas hela tiden.
[G ; WHILE P DO H VARIANT E INVARIANT I END] Q	${\displaystyle \left(\left[G\right]I\right)\wedge }$ ${\displaystyle \left(I\wedge \neg P\wedge \Rightarrow Q\right)\wedge }$ ${\displaystyle \left(I\Rightarrow E\in \mathbb {N} \right)\wedge }$ ${\displaystyle \left(I\wedge P\Rightarrow \left[y:=E\right]\left[H\right]E<y\right)\wedge }$ ${\displaystyle \left(I\wedge P\Rightarrow \left[H\right]I\right)}$	Efter att kod G execuerats execureras kod H så länge villkor P uppfylls. Loopvariabel är E och under hela tiden måste villkor I uppfyllas.

Detta program definierar en maskin Positive som representera ett naturligt tal mellan 0 och maxint med startvärde 0. Till maskinen finns operationerna set (för att ändra värde), read (för att läsa värde) och incr (för att öka med ett).

MACHINE  Positive (maxint)VARIABLES  valINVARIANT  val ${\displaystyle \in }$  0 .. maxintINITIALISATION  val := 0OPERATIONS  set (xx) =    PRE      xx ${\displaystyle \in }$  0 .. maxint    THEN      val := xx    END  ;  vv ← read =    vv := val  ;  incr =    PRE      val < maxint    THEN      val := val + 1    END  ;END

Det som mest skiljer detta programmet från vanliga program är INVARIANT som måste uppfyllas under hela programmets gång och PRE som måste uppfyllas vid execuering. Om det finns någon matematisk sannolikhet att dessa villkor inte uppfylls någon gång under programmets gång misslyckas kompileringen. På så sätt går det att redan under kompileringen få reda på om det finns någon bugg i programmet som annars kanske skulle ha upptäckts först efter att ha kört programmet under lång tid.

• [Wordsworth, J.B. ] (1996) Software Engineering with B, ISBN 0-201-40356-0