B (mjukvaruutveckling)

Från Rilpedia

Hoppa till: navigering, sök
Wikipedia_letter_w.pngTexten från svenska WikipediaWikipedialogo_12pt.gif
rpsv.header.diskuteraikon2.gif
icon_anmal.gif
rp-wp-sv.gif

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ättet går det att ta fram matematiska bevis att programmet fungera innan det riktiga programmet skrivs.

Innehåll

Exempel på notation

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

Exempel på Substitutioner

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 \left[ G \right] Q Villkor Q måste uppfyllas medan G execueras.
[PRE P THEN G END] Q 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 \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		 \left( \left[ G \right] I \right) \wedge

\left( I \wedge \neg P \wedge \Rightarrow Q \right) \wedge
\left( I \Rightarrow E \in \mathbb{N} \right) \wedge
\left( I \wedge P \Rightarrow \left[ y:= E \right] \left[ H \right] E < y \right) \wedge
\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.

Exempel på program i B

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 \in 0 .. maxint
INITIALISATION
  val := 0
OPERATIONS
  set (xx) =
    PRE
      xx \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.

Böcker

Hämtad från "https://sv.rilpedia.org/wiki/B_(mjukvaruutveckling)"
Personliga verktyg
På andra språk