B (mjukvaruutveckling) – Wikipedia

B är en mjukvaruutvecklingsmetod framtagen av Jean-Raymond Abrial, tillika ett språk och CASE-verktyg från B-Core (UK) Ltd..

B-metoden är nästan unik bland formella mjukvaruutvecklingsmetoder i det avseendet att den använder samma notation för specifikation, design och programmeringen.

Språket B byggs upp med hjälp av matematiska formler med vars hjälp det går att validera programmet. På detta sätt går det att ta fram matematiska bevis att programmet fungera innan det riktiga programmet skrivs.

Matematik	motsvarighet i B	Beskrivning
${\displaystyle P\wedge Q}$	P & Q	Konjunktion
${\displaystyle P\vee Q}$	P or Q	Disjunktion
${\displaystyle P\Rightarrow Q}$	P=>Q	Implikation
${\displaystyle P\Leftrightarrow Q}$	P<=>Q	Ekvivalens
${\displaystyle \neg P}$	not P	Negation
${\displaystyle \forall z\cdot P}$	!(z).P	Allkvantifikator
${\displaystyle \exists z\cdot P}$	#(z).P	Existenskvantifikator
${\displaystyle \left[G\right]P}$	[G]P	substitution

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   val INVARIANT   val ${\displaystyle \in }$ 0 .. maxint INITIALISATION   val := 0 OPERATIONS   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