Komponensek

Az absztrakt gépek című részben már szerepeltek azok a fogalmak és nyelvi elemek, amiknek segíségével egy B model komponenseit megadjuk. Ebben a részben pontosítjuk, és részletezzük ezekt a fogalmakat és nyelvi elemeket. A B nyelv teljes egésszében a sepecifikáció hierarchikus leírására szolgál. A legfelső szint, amit absztrakt modelnek is nevezünk. Ezt a modelt, absztrakt gépet, finomítjuk lépésenként, ezek a finomított modelek. A finomítás során a specifikáció egyre konkrétabbá válik abban az értelemben is, hogy közelebb kerűl a szokásos programnyelvekhez. A finomítás legalsó szintje a megvalósítható, vagy implementációs model, amelyből automatikusan futtatható forráskód generálható. Egy feladat modelje több komponensből épül föl. Ezek között a gépek között különböző kapcsolatok lehetnek. Az absztrakt gép, a finomítások, beleértve a megvalósítható modelt is, egy feladat specifikációjának a különböző szintjei. Egy összetett feladat megoldására több különböző absztrakt modelből és finomításaiból álló rendszer alkalmas. Ennek a rendszernek a komponensei közötti kapcsolatok leírásával is foglakozunk a továbbiakban. Bár utalni fogunk a objektum elvű nyelvekhez kapcsolódó analógiákra, a B mint biztonság kritikus feladatok megoldására szolgáló eszköz, alapvetően nem objektum elvű. Például nincs öröklődés. Ez csökkenti a hatékonyságot, de növeli a megbízhatóságot.

Absztrakt gépek

Az absztrakt gépeket különböző elemek segítségével definiálhatjuk, így hozzájuk tartozó adatokat és műveleteket is. Az absztrakt gép az őt tartalmazó modul specifikációja. Két részből áll: a fejrészből(header) és az elemekből (clause). Az elemek sorrendje nem kötött. Minden elem egyszer szerepelhet az absztrakt gépben. Ha az absztrakt gép tartalmazza a CONCRETE_CONSTANTS vagy ABSTRACT_CONSTANTS elemeket, akkor tartalmaznia kell a PROPERTIES elemet is. Ha hasonlóan szerepel az absztrakt gépben a CONCRETE_VARIABLES vagy ABSTRACT_VARIABLES elem, akkor az INVARIANT és INITIALISATION elemeknek is szerepelniük kell benne. A speciális művelet olyan művelet, amelynek törzse az OPERATIONS elemben van definiálva.

Fejrész

A komponens fejrésze annak nevéből, és a hozzá tartozó formális paraméterek listájából áll, amely lista nem változik a komponens finomítása során. A formális paraméter lehet késleltetett halmaz vagy skalár. A komponens nevének egyedinek kell lennie a projektben. A halmaz paraméterek nevében nem szerepelhet kisbetű, míg a skalár paraméterek nevében szerepelnie kell kisbetűnek. Ha valamely absztrakt gép példányát beilleszti vagy importálja valamely másik komponens, akkor a formális paraméterek értékét az aktuális paraméterek alapján állítja be. A formális paraméterek deklarációja a CONSTRAINTS elemben szerepel. A formális paraméterek olvashatók az INVARIANT , az ASSERTIONS , az INCLUDES (mint a beillesztett absztrakt gép aktuális paramétere), az INITIALISATION és az OPERATIONS elemekben, azonban nem használhatóak a PROPERTIES elemben.

Finomított modell

A finomított modellben nem használható a USES és a CONSTRAINTS elem. Minden elem egyszer használható a finomított modellben.

Megvalósítható modell

A megvalósítható modell a finomítás utolsó lépése. Két új elem használható: az IMPORTS elem és a VALUES elem. Az IMPORTS elem más modulok konkrét példányait hozza létre a projektben. A VALUES elem értéket ad a késleltetett halmazoknak és a konkrét konstansoknak. Az EXTENDS elem az IMPORTS elemnhez, míg absztrakt gép vagy finomított modell esetén az INCLUDES elemhez hasonló. Az INITIALISATION és OPERATIONS elemek csak konkrét kifejezéseket és helyettesítéseket tartalmazhatnak (az absztrakt gép és finomított modell azonos elemeivel ellentétben). A CONSTRAINTS , az INCLUDES , a USES , az ABSTRACT_CONSTANTS és az ABSTRACT_VARIABLES (vagy VARIABLES ) elemek nem használhatóak megvalósítható modellben.

CONSTRAINTS elem

A CONSTRAINTS elem típust ad a skalár paramétereknek, és megszorításokat definiál rajtuk. Kétféle paraméter lehet: skalár paraméter és halmaz paraméter. A skalár paraméter olyan azonosító, amelyben van kisbetű, és amelynek típusa lehet , BOOL vagy valamely paraméterként kapott halmaz. A halmaz paraméter olyan azonosító, amelyben nem szerepel kisbetű, és amely késleltetett halmaz lehet (amely integer intervallumnak felel meg). A halmaz paramétereknek nem kell típust adni.

REFINES elem

A REFINES elem a finomított komponens (azaz az absztrakció) nevét tartalmazza.

IMPORTS elem

Az import kapcsolat megvalósítható modell és absztrakt gép között jön létre. A megvalósítható modell létrehozza az absztrakt gép példányát, hogy használja annak adatait és műveleteit saját adatainak és műveleteinek megvalósítására. Így a megvalósítható modellt tartalmazó modul lesz az importgráfban az importált modul példányának az apja. Csak egy megvalósítható modell szerepelhet a modulban, amely modell módosíthatja az importált gép változóit. Az IMPORTS elemben szereplő azonosítóknak absztrakt gépre kell hivatkozniuk. Átnevezés esetén csak egy prefix használható. Minden név után annyi aktuális paraméternek kell lennie, ahány formális paramétere van az absztrakt gépnek. Ha a megvalósítható modell valamely konkrét konstansa, illetve konkrét változója azonos a modell által importált gép valamely konkrét konstansával, illetve konkrét változójával, akkor az általuk meghatározott adatoknak, illetve azok típusának is azonosaknak kell lenniük. Semelyik gép példányát sem lehet többször is importálni a projektben. Csak egy olyan fejlesztett modul lehet a projektben, amelyet nem importál semelyik másik modul. Minden komponens csak egyféle kapcsolatban lehet bármely másik komponenssel. Nem lehet kör a projekt függőségi gráfjában. Az aktuális paramétereknek ki kell elégíteniük az importált gép CONSTRAINTS elemében meghatározott megszorításokat. Az aktuális skalár paraméter lehet Boolean érték, a megvalósítható modell, vagy az általa látott példány felsorolási halmazának eleme, illetve Z vagy BOOL típusú konkrét konstansa, a megvalósítható modell formális skalár paramétere, vagy aritmetikai kifejezés. Az aktuális halmaz paraméter lehet a megvalósítható modell formális halmaz paramétere, késleltetett vagy felsorolási halmaza, illetve a látott példány hasonló halmaza, vagy esetleg aritmetikai kifejezéssel meghatározott nem-üres intervallum. Magas szintű programozási nyelvek esetén is hasonlóan össze kell kapcsolni a program különböző részeit az osztályokkal, hogy azok elérhetőek legyenek, azonban ekkor az osztály publikus változói, konstansai és műveletei mind elérhetőek, valamint ezek olvashatóak és írhatóak is. A privát adatok és műveletek viszont nem érhetőek el, így különbséget lehet tenni közöttük. Erre itt nincs lehetőség. Mivel minden változó csak olvasható közvetlenül (mint a publikus változók), de csak az importált példány műveletein keresztül lehet módosítani (mint a privát változókat). Viszont minden műveletet meg lehet hívni.

SEES elem

A SEES kapcsolat segítségével olyan absztrakt gép adatait lehet olvasási módban elérni, amely a projekt valamely más ágán lett importálva. Tehát a komponens által látott gép példányát valamely más, a projektben szereplő komponensnek be kell importálnia. Ha a fejlesztett modul valamely komponense látja valamely másik komponens példányát, akkor ennek finomításainak is látniuk kell azt. A modul komponensei nem láthatnak olyan példányt, amely a modul import algráfjához tartozik. A komponens nem láthatja az általa látott példány import algráfjához tartozó valamely másik példányt. A komponensek nem kapcsolódhatnak többféleképpen valamely példányhoz (SEES , IMPORTS ). Nem lehet kör a projekthez tartozó függőségi gráfban. A fentiek a moduloknál is említett feltételek. A látott példányokat át lehet nevezni, viszont nem kell aktuális paraméterekkel hivatkozni rájuk, mivel nem hoznak létre új példányt, mint az INCLUDES és IMPORTS elemek esetében, csak használják a már meglévőt. Átnevezés esetén a prefix azonos a projekt importgráfjában a komponens és a látott példány első közös ősétől a példányig található prefixek kompozíciójával. Azaz amennyiben az MA komponens látja az ME importált példányát, és első közös ősük MB, ahol MB a c prefixszel importálja az MC komponenst, amelynek leszármazottja (nem feltétlenül gyereke) az MD komponens, és az MD komponens az e prefixszel importálja az ME komponenst, akkor az MA komponensben a c.e.ME kifejezés kerül a SEES elembe. Ha a látott példányhoz tartozik a fenti módon meghatározott prefix, akkor ezt a prefixet kell használni annak változói esetén is. A SEES kapcsolat nem tranzitív, azaz amennyiben MA látja MB-t, amely látja MC-t, akkor MA nem feltétlenül látja MC-t, csak akkor, ha szerepel a SEES elemében.

INCLUDES elem

A beillesztés során az aktuális skalár paraméterek típusa azonos kell legyen a beillesztett gép formális skalár paramétereinek típusával, illetve az aktuális halmaz paraméterek típusa P(T ) kell legyen, ahol T a STRING -től különböző alaptípus. Csak egy prefix lehet a gép neve előtt átnevezés esetén. Annyi aktuális paraméternek kell szerepelnie, ahány formális paraméter van. Az aktuális paramétereknek ki kell elégíteniük a példányban meghatározott, formális paraméterekre vonatkozó megszorításokat. Az aktuális skalár paraméter lehet Z, BOOL vagy Set típusú, illetve az aktuális halmaz paraméter lehet P(Z), P(BOOL ) vagy P(Set) típusú, ahol Set késleltetett vagy felsorolási halmaz. A finomított modell beillesztheti a valamely korábbi finomítási lépés során már beillesztett példányt. Ekkor azok a késleltetett halmazok, felsorolási halmazok, konkrét konstansok és konkrét változók, amelyek a korábbi beillesztés hatására kerültek a finomított modellbe, „összeragadnak” a beillesztett példányban szereplőkkel, illetve azok az absztrakt konstansok és absztrakt változók, amelyek hasonló módon kerültek a finomított modellbe, a beillesztett példányban szereplő adatokkal „ragadnak össze”. Ha az MA modul valamely komponense beilleszti az MB modulhoz tartozó absztrakt gép példányát, akkor többféle megvalósítható modell tartozhat az MA modulhoz. A megvalósítható modell importálhatja a beillesztett példányt Az INCLUDES kapcsolat tranzitív, azaz amennyiben MA beilleszti MB-t, amely beilleszti MC-t, akkor az MB-ben elérhetőek lesznek az MC-hez tartozó halmazok, konstansok, változók és az MC-ben lévő tulajdonságok (MB hasonló adataihoz hozzáveszi azokat úgy, mintha eredetileg is az MB-ben lettek volna), így MA-ban is elérhetőek lesznek, azonban a műveletek esetén ez nem igaz. Ha konkrét változók is szerepelnek MC-ben vagy MB-ben, akkor az MA-hoz tartozó megvalósítható modellben inicializálni kell azokat úgy, mintha MA-beliek lennének. A valamely komponensben bevezetett, vagy beillesztett konkrét változót minden olyan komponensben inicializálni kell, amely ennek finomítási lépései során szerepel, és beillesztett konkrét változó esetén nem illeszti be, vagy importálja a korábban beillesztett példányt, mivel ekkor az abban szereplő inicializációs rész megteszi azt. Absztrakt változót csak akkor kell inicializálni, ha az adott komponensben szerepel a változók között.

PROMOTES elem

A komponens kitüntetheti a beillesztett (absztrakt gép vagy finomított modell esetén), vagy importált (megvalósítható modell esetén) példány valamely műveletét, azaz tulajdonképpen azonossá teheti azzal a művelettel, amely a komponens OPERATIONS elemében azonos névvel (esetleg prefixszel kiegészítve), jelöléssel és törzzsel lenne definiálva. Minden olyan kitüntetett művelet nevének azonosnak kell lennie valamely absztrakt gép műveletének nevével, amely finomított modellben lett definiálva. A kitüntetett művelet nem különbözik a komponens többi, OPERATIONS elemben deklarált művelettől azt kivéve, hogy használható az INITIALISATION és OPERATIONS elemekben, mert itt beillesztett példány műveleteként viselkedik.

EXTENDS elem

Absztrakt gép vagy finomított modell esetén az EXTENDS elem ekvivalens az INCLUDES elem hatásával, és a beillesztett példány összes műveletének kitüntetésével (PROMOTES elem), míg megvalósítható modell esetén az IMPORTS elem hatásával, és az importált példány összes műveletének kitüntetésével ekvivalens.

USES elem

A beillesztett példányok adatainak megosztására használható a USES kapcsolat, azaz amennyiben az MA beilleszti MB-t, MC-t és MD-t, illetve MB és MD használja MC-t, akkor MC-ben osztja meg az adatokat MB és MD. Ha valamely gép valamely másik gép példányát használja, akkor lennie kell a projektben olyan gépnek, amely beilleszti ezen két gép példányait. Azt a gépet nem lehet finomítani, amely másik gépet használ, illetve másik komponens nem láthatja vagy importálhatja. Absztrakt modulban kell lennie annak a gépnek, amely más gépeket használ. A USES elem nem tranzitív.

SETS elem

A SETS elem a komponens késleltetett és felsorolási halmazait definiálja. A finomított modellhez (illetve megvalósítható modellhez) tartozó felsorolási halmaz nevének különböznie kell az általa látott vagy beillesztett (illetve importált) absztrakt gépekhez tartozó felsorolási halmazok neveitől, kivéve akkor, ha a finomított modell (illetve megvalósítható modell) valamely absztrakciójában szereplő felsorolási halmaz neve és elemei azonosak a finomított modell (illetve megvalósítható modell) által látott vagy beillesztett (illetve importált) absztrakt gépekhez tartozó valamely felsorolási halmaz nevével és elemeivel. A késleltetett és felsorolási halmazok megmaradnak a komponens finomítása során a megvalósítható modellig. A késleltetett halmaz olyan nem-üres halmaz, amelynek megvalósítását a felhasználó nem akarja meghatározni valamely specifikációs szinten, azonban a megvalósítható modellben értéket kell neki adni, amely véges, nem-üres intervallum lehet. A felsorolási halmaz tulajdonképpen elemek listája. Az absztrakt gép késleltetett és felsorolási halmazai a saját halmazai, kiegészítve a beillesztett példányokhoz tartozó gépekben definiáltakkal, a finomított modell hasonló halmazai a saját halmazai, illetve az absztrakciójához tartozó halmazok, a megvalósítható modell halmazai a finomított modell halmazaihoz hasonlóan határozhatóak meg, azonban ebben az esetben az importált példányokhoz tartozó gépekben szereplő halmazok tartoznak ide. Az absztrakt gép késleltetett halmazai, felsorolási halmazai és felsorolási halmazainak elemei a gép INCLUDES , EXTENDS , PROPERTIES , INVARIANT , ASSERTIONS, INITIALISATION és OPERATIONS elemeiben, illetve a gépet látó, beillesztő, használó vagy importáló komponensekben érhetőek el. A finomított modell késleltetett halmazai, felsorolási halmazai és felsorolási halmazainak elemei a finomított modell hasonló elemeiben érhetőek el. A megvalósítható modell késleltetett halmazai, felsorolási halmazai és felsorolási halmazainak elemei a megvalósítható modell IMPORTS , EXTENDS , PROPERTIES , VALUES , INVARIANT , ASSERTIONS , INITIALISATION és OPERATIONS elemeiben érhetőek el.

CONCRETE_CONSTANTS elem

A konkrét konstans olyan adat elem, amely megvalósítható valamely programozási nyelvben. Az értéke a finomítás során megmarad a megvalósítható modellig. A konkrét konstans lehet integer vagy Boolean érték, absztrakt vagy felsorolási halmaz eleme, véges, nem-üres intervallum, késleltetett halmaz, vagy tömb. A finomított vagy megvalósítható modellben bevezetett új konkrét konstans nevének különbözni kell a modell absztrakciójában szereplő konstansok (konkrét vagy absztrakt) nevétől, kivéve akkor, ha az absztrakcióban szereplő valamely absztrakt konstans finomítása, azonban ekkor azonos típusúaknak kell lenniük. Az absztrakt gép által elérhetőek a saját, illetve a beillesztett példányokhoz tartozó gépek konkrét konstansai. A finomított modell által elérhetőek a saját, az absztrakció, illetve a beillesztett példányokhoz tartozó gépek konkrét konstansai. A megvalósítható modell által elérhetőek a saját, illetve az absztrakció konkrét konstansai, valamint az importált példányokhoz tartozó konkrét konstansok. A konkrét konstansok típusát és tulajdonságait a PROPERTIES elem határozza meg. Minden komponens konkrét konstansának a komponenshez tartozó megvalósítható modell VALUES eleme ad értéket. Minden absztrakt gépben definiált konkrét konstansnak a PROPERTIES elem ad típust, finomított modellben, illetve megvalósítható modellben bevezetett új konkrét konstans esetén is így van, azonban ha ez a konkrét konstans valamely az absztrakcióban szereplő absztrakt konstans finomítása, akkor implicit módon, annak megfelelő típusa lesz. Az absztrakt gép konkrét konstansai olvashatóak a PROPERTIES , INVARIANT , ASSERTIONS , INCLUDES és EXTENDS elemekben illetve az inicializációs rész és a műveletek törzsében, valamint azokban a komponensekben, amelyek látják, beillesztik, használják vagy importálják a gép példányát. A finomított modell konkrét konstansaira hasonlóak igazak (elemek, inicializációs rész, műveletek). A megvalósítható modell konkrét konstansaira a finomított modellnél leírtak teljesülnek kivéve, hogy itt az INCLUDES elem helyett az IMPORTS elem szerepel, és a konkrét konstansokat írhatja a VALUES elem.

ABSTRACT_CONSTANTS elem

A finomítottmodellhez tartozó absztrakt konstans neve különbözik az absztrakció minden konstansának (konkrét vagy absztrakt) nevétől kivéve akkor, ha a valamely absztrakt konstanssal azonos. Az absztrakt konstans típusát és tulajdonságait a PROPERTIES elem határozza meg. A finomított modellben szereplő absztrakt konstans lehet új (ekkor a PROPERTIES elemben szerepe a fent említett), illetve valamely az absztrakcióban szereplő absztrakt konstans finomítása. Utóbbi esetben nem kell típust adni a konstansnak, azonban új tulajdonságokat lehet hozzá definiálni a PROPERTIES elemben. Ha valamely komponens absztrakt konstansát nem finomítja az őt finomító komponens, akkor az nem tartozik a finomító komponens konstansai közé, azaz „eltűnik” benne. Az ABSTRACT_CONSTANTS elem nem használható a megvalósítható modellben. Az absztrakt gép absztrakt konstansa olvasható az INCLUDES , EXTENDS , PROPERTIES , INVARIANT , ASSERTIONS , INITIALISATION és OPERATIONS elemekben, valamint a gép példányát importáló, látó, beillesztő és használó komponensekben. A finomított modell absztrakt konstansaira és elemeire hasonló igaz.

VALUES elem

A VALUES elemben lehet értéket adni konkrét konstansoknak és késleltetett halmazoknak. Minden konkrét konstansnak és késleltetett halmaznak csak egyszer lehet értéket adni. Ha a VALUES elemben kapnak értéket, akkor explicit, különben implicit értékadásról van szó. Implicit értékadás esetén azonosnak kell lenniük valamely látott vagy importált példányhoz tartozó gépben deklarált konkrét konstanssal vagy késleltetett halmazzal. Ebben az esetben a konkrét konstansok típusa azonos kell legyen. Ha az értékadásnál a jobb oldalon szerepel valamely konkrét konstans vagy késleltetett halmaz, akkor annak már korábban értéket kell kapnia. Késleltetett halmaz értékadásakor az értékként kapott halmaz típusára változik a típusa. A megvalósítható modell által látott vagy importált példányokhoz tartozó gépekben szereplő késleltetett halmazzal (ekkor a típusa P(AbsSet) lesz), azaz implicit módon (ekkor a típusuk azonos lesz), nem-üres integer intervallummal (ekkor a típusa P(Z) lesz) vagy már értékkel rendelkező késleltetett halmazzal lehet értéket adni késleltetett halmaznak. Tulajdonképpen minden késleltetett halmaz integer intervallum.

CONCRETE_VARIABLES elem

A konkrét változó olyan adatelem, amely megvalósítható valamely programozási nyelvben. A megvalósítható modellben az importált példányokhoz tartozó gépek konkrét változói közvetlenül olvashatók, annak absztrakt változóival ellentétben. A gépekben deklarált konkrét változókat nem kell átnevezni. A finomított modellben vagy megvalósítható modellben bevezetett új konkrét változóknak különbözniük kell a modell absztrakciójában szereplő többi változótól (konkrét vagy absztrakt), kivéve azt az esetet amikor az absztrakcióban szereplő absztrakt változó finomítása, mivel ekkor a két változó azonos lesz. Az absztrakt gép által elérhető konkrét változók a saját konkrét változói, illetve a beillesztett példányokhoz tartozó gépekben bevezetett konkrét változók. A finomított modell által elérhetőek a saját és a beillesztett konkrét változókon kívül az absztrakcióban bevezetett konkrét változók is. A megvalósítható modell által is a fenti konkrét változók érhetőek el, a beillesztett változók kivételével, valamint az importált konkrét változók. A változók típusát és tulajdonságait az INVARIANT elem határozza meg. Minden konkrét változónak kezdeti értékét az INITIALISATION elem állítja be. A finomított modellben vagy megvalósítható modellben szereplő, az absztrakcióban lévő változót finomító konkrét változónak nem kell meghatározni a típusát (skalár vagy tömb), mivel azonos a finomított változóéval.

ABSTRACT_VARIABLES elem

Az ABSTRACT_VARIABLES elem új absztrakt változókat deklarál absztrakt gépekben és finomított modellekben. Az absztrakt változó olyan adatelem, amely a komponens finomítási lépésein keresztül finomítva lesz. Az absztrakt változót nem kell átnevezni. A finomított modellben bevezetett új absztrakt változónak különböznie kell az absztrakció változóitól (konkrét vagy absztrakt), kivéve abban az esetben, ha valamely az absztrakcióban szereplő változó finomítása, mivel ekkor azonos vele. A konkrét változókhoz hasonlóan az absztrakt változók típusát és tulajdonságait az INVARIANT elem, míg kezdeti értékét az INITIALISATION elem határozza meg. A finomított modellben szereplő absztrakt változó lehet új, azaz különbözik az absztrakcióban lévő változóktól, amely esetben nem kell átnevezni. Az absztrakt változó azonban lehet valamely beillesztett példányhoz tartozó gépben bevezetett változó finomítása. Ebben az esetben a beillesztésénél (a tranzitivitást is figyelembe véve) használt átnevezést kell a változó esetén is alkalmazni. Ekkor is lehet a változóhoz tartozó új tulajdonságokat megfogalmazni az INVARIANT elemben. Azon absztrakt változók, amelyek valamely finomítási lépés során nem lettek finomítva absztrakt vagy konkrét változó által, azok „eltűnnek”, azaz nem lesznek elérhetőek a finomítási lépés utáni komponens további finomításaiban (a korábbiakban említett „eltűnő” adatokra is ez igaz). Azoknak a finomított modellben szereplő absztrakt változóknak is kezdeti értéket kell adni, amelyek nem beillesztett példány hatására kerültek a komponensbe. Megvalósítható modellben nem szerepelhet absztrakt változó. A finomított modellben bevezetett absztrakt változók nem érhetőek el a modulon kívüli komponens számára.

INVARIANT elem

Az INVARIANT elemben szereplő predikátum határozza meg a komponensben szereplő változók típusát és tulajdonságait. Az INITIALISATION elemben meghatározott kezdeti értékadásnak és a műveletek végrehajtása után beállított új értékeknek ki kell elégíteniük az invariáns tulajdonságot. Ezért más komponensek csak olvashatják a konkrét, illetve az absztrakt változókat, de nem írhatják azokat. Finomított modell és megvalósítható modell esetén az INVARIANT elemben szereplő invariáns tulajdonságot az absztrakcióban és a komponensben szereplő változók közti kapcsolat leírására is lehet használni, amelyet ezért „ragasztó” invariáns tulajdonságnak (gluing invariant) is neveznek. Minden olyan változónak a típusát az INVARIANT elemnek kell meghatároznia, amely nem azonos valamely az absztrakcióban szereplő változóval, azonban azon változókét nem kell, amelyek azonosak az absztrakcióban szereplő valamely változóval, mivel ekkor elég az azonosságukat meghatározó „ragasztó” predikátumot (gluing predicate) leírni, így a típusuk is azonos lesz. Ha a finomított modellben és az általa beillesztett példányhoz tartozó gépben szereplő változók (konkrét vagy absztrakt) azonosak, akkor azonos adatot kell meghatározniuk, és típusaiknak is azonosaknak kell lenniük. Hasonló igaz a megvalósítható modell esetén is, azzal a kivétellel, hogy importált példányokról van szó.

ASSERTIONS elem

Az ASSERTIONS elem tulajdonképpen olyan lemmákat tartalmaz, amelyeket az invariáns tulajdonság, és a megelőző lemmák segítségével kell bizonyítani. Így a predikátumok sorrendje fontos. Később ezeket az invariáns tulajdonság ellenőrzésekor feltételezésként használhatjuk.

INITIALISATION elem

Az INITIALISATION elemnek a komponens azon változóinak kezdeti értékét kell beállítania, amelyek különböznek minden a beillesztett és importált példányokhoz tartozó gépekben bevezetett változóktól. Tulajdonképpen felfogható úgy, mint egy paraméter nélküli művelet, amelynek ki kell elégítenie az invariáns tulajdonságot. A projekt futtatásakor a függőségek alapján az összes modul ezen speciális műveletét hajtja végre, mielőtt a projekt belépési pontját (entry point) meghívná. Lehetséges a beillesztett példányokhoz tartozó gépek változóinak módosítása a gép műveletein keresztül ebben az elemben. Ez akkor különösen fontos, ha ezen változók szerepelnek az invariáns tulajdonság változókat összekapcsoló (gluing predicate) részében. Látott vagy importált példányokhoz tartozó gépek változóinak kezdeti értéke már be van állítva. A változók kezdeti értékét helyettesítéssel, illetve megvalósítható modell esetén instrukcióval lehet beállítani. Megvalósítható modell esetén a konkrét változóknak közvetlenül, illetve közvetett módon lehet értéket adni. Az első esetben explicit értékadás történik, míg az utóbbiban valamely az importált példányhoz tartozó gépben szereplő konkrét változó azonos a modell saját változójával, így annak kezdeti értékét az importált példányhoz tartozó gépben kell beállítani. A kezdeti értékek beállításához nem lehet használni a komponens saját műveleteit.

OPERATIONS elem

Az OPERATIONS elem tartalmazza a műveletek leírását. A műveletek formális input és output paramétereinek különbözőeknek kell lenniük. Absztrakt gépben deklarált műveleteket nem kell átnevezni. A művelet formális input paramétereinek típusát a törzs elején lévő előfeltételes helyettesítéssel kell meghatározni. Az output paraméterek típusát a törzsben kell meghatározni. Finomított modellben nem lehet új műveletet definiálni. Megvalósítható modellben minden absztrakt géphez tartozó műveletnek szerepelnie kell az OPERATIONS elemben, vagy kitüntetettnek kell lennie. A finomított modellben és a megvalósítható modellben a műveletek neve és paraméterei azonosak valamely az absztrakcióban szereplő műveletével, így nem kell a paraméterek típusát meghatározni,mivel az absztrakcióban ez már megtörtént. A megvalósítható modell OPERATIONS elemében csak az absztrakcióban, vagy a LOCAL_OPERATIONS elemben szereplő műveletek definíciói lehetnek, illetve minden a LOCAL_OPERATIONS elemben szereplő műveletet definiálni kell az OPERATIONS elemben. Az OPERATIONS elem helyi műveleteinek (local operations) megvalósításához tartozó helyi művelet hívások gráfjának nem szabad kört tartalmaznia. A műveletek a B nyelv dinamikus részét írják le, mivel segítségükkel módosíthatóak a változók értékei. A modulokhoz tartozó műveletek specifikációját határozzák meg az absztrakt gépek műveletei. Fontos, hogy a finomítás utáni művelet konzisztens legyen a finomítás előtti művelettel. Az absztrakt géphez a kitüntetett műveletek, illetve a saját műveletei tartoznak. A fejlesztett modulhoz, és az alapmodulhoz tartozó komponensek műveleteinek paraméterei megvalósítható típusúak (azaz azonos a konkrét változók lehetséges típusaival, illetve megengedett a STRING típus is), mivel ezekhez tartozik forráskód, ellentétben az absztrakt modullal, amelyhez tartozó komponensek műveleteinek paraméterei bármilyen típusúak lehetnek. A műveletek fejrészből és törzsből állnak. A fejrész a művelet nevéből, input illetve output paramétereiből áll. Az érték szerinti paraméterátadást használják a műveletek (azaz a formális illetve aktuális paraméterek értékét átmásolják a nekik megfelelő aktuális illetve formális paraméterekbe). A paraméterek hatóköre a művelet törzse. Az input paraméterek csak olvashatók, az output paraméterek olvashatók (írás után) és írhatók a helyettesítésekben. A törzsben nem lehetséges az OPERATIONS elem, vagy a használt példányhoz tartozó gép valamely műveletének meghívása. Magas szintű programozási nyelvek esetében többféle paraméterátadási mód is létezik (cím szerinti paraméterátadás, név szerinti paraméterátadás, stb.). Illetve alapvető, hogy az osztályok függvényeik definiálásakor meghívhatják az osztályban már definiált más függvényeket, valamint az osztályhoz kapcsolt valamely példány függvényeit. Magas szintű programozási nyelvben általában a függvény azon komponens adatain hajt végre változtatásokat, amelyben definiálták. Ebben az esetben azonban a beillesztett és importált példányok adatait is lehet módosítani a műveletekkel, amely a magas szintű programozási nyelvek esetében saját adat, hiszen a programhoz kapcsolt osztályt, mint típust használja saját objektumaihoz. Ha a finomítandó művelet az OPERATIONS elemben át van nevezve, akkor a finomított művelet prefixe azonos lesz az eredeti prefixszel. Ha a kitüntetett művelethez tartozó gép példánya átnevezve van beillesztve, akkor a kitüntetésnél is megmarad az átnevezés első prefixe. Finomított modell esetén a műveletben szereplő helyettesítéseknek „determinisztikusabbaknak” kell lenniük az absztrakcióban használt helyettesítéseknél, megvalósítható modell esetén csak determinisztikus helyettesítéseket használhatnak a műveletek. A finomított modell műveleteinek előfeltétele gyengülhet az absztrakcióhoz képest, megvalósítható modell esetén viszont nem szerepelhet előfeltétel a műveletben. A finomított modell műveleteinek helyettesítései „konkrétabbak” az absztrakcióban szerepl ő helyettesítéseknél, megvalósítható modell műveleteiben viszont csak konkrét helyettesítések (instrukciók) lehetnek, amelyek futtathatóak valamely programozási nyelvben.

LOCAL_OPERATIONS elem

A LOCAL_OPERATIONS elemben a megvalósítható modell helyi műveleteinek specifikációi találhatóak. A helyi műveleteket az inicializációs rész, illetve a megvalósítható modell más műveletei használhatják (helyi vagy nem-helyi). Ezek megvalósításai az OPERATIONS elemben találhatóak. A helyi művelet formális paramétereinek különbözőeknek kell lenniük. A helyi műveleteket nem kell átnevezni. A formális input paraméterek típusát a törzs elején lévő előfeltételben kell meghatározni. Az output paraméterek típusát a törzsben kell meghatározni. A helyi műveleteket a projekt méretének csökkentésére használják. A specifikációban szereplő helyettesítések az absztrakt gépeknél is használható, korábban már látott helyettesítések. A szimultán helyettesítés megengedett, azonban nem lehet használni a szekvenciális helyettesítést. Az absztrakcióban szereplő, a megvalósítható modell által finomított komponens, illetve a látott vagy importált példányokhoz tartozó gépek konstansai és absztrakt változói elérhetőek a specifikációban, sőt az importált példányokhoz tartozó gépek változói közvetlenül módosíthatóak. A helyi műveletek OPERATIONS elemben található megvalósításai a nem-helyi műveletekhez hasonlóan írhatóak le. Konzisztensnek kell lennie a specifikációval. A szimultán helyettesítés nem használható, a szekvenciális helyettesítés viszont használható. A konstansok és absztrakt változók nem érhetőek el az instrukciókban. A helyi művelet módosíthatja az importált példányokhoz tartozó gépek változóit közvetlenül a specifikációs részben, és közvetett módon, azaz művelet hívásokkal a megvalósítási részben. A helyi műveletet tartalmazó megvalósítható modellel ekvivalens az a megvalósítható modell, amelyben nem szerepel a helyi művelet, azonban importálja a helyi műveletet nem helyi műveletként deklaráló absztrakt gép példányát. Ebben az absztrakt gépben a helyi művelet specifikációja szerepel, míg a hozzá tartozó megvalósítható modellben a művelet finomításaként a helyi művelet megvalósítása szerepel. Ha eredetileg a megvalósíthatómodell importálta valamely gép példányát, akkor ezt most az előbb említett megvalósítható modellnek kell importálnia.