A Th tételek halmazát, amelyet egy jellemzésben definiált szavakra be tudunk látni, a jellemzés elméletének hívjuk. Ez az elmélet végtelenül nagy és a jellemzés axiómáiból egy logikai rendszer használatával vezethető le. Egy logika rendszer szintaktikusan helyes állítások halmazából, amit wff-eknek vagy jól-formált formuláknak nevezzük, és a wff-k helyességének belátásának módszeréből áll. Egy bizonyítás (proof) ennek a módszernek az alkalmazásából áll. Célszerű egy bizonyításra úgy gondolni, mint wff-k sorozatára, amelyekből az utolsó a bizonyítandó wff. A bizonyításbeli wff-ek mindegyike vagy egy axióma vagy pedig a bizonyításban a megelőző wff-ekből és egy rákövetkezési szabályból következik. Axiómának nevezzük azokat a wff-ket, amelyeket igaznak tekintünk. A rákövetkezési szabályok segítségével következtethetünk egy wff érvényességére, a konklúzióra, más wff-k érvényességéből, a hipotézisekből.

Egy segéd specifikáció célja egy elmélet definiálása. Egy specifikációhoz végtelen sok wff tartozik, amelyek lehetnek

1. a BOOL fajta bármelyik szava, pl

TRUE

IS_IN(NEW, "a")

2. bármilyen t1 = t2 alakú egyenlőség, ahol t1 és t2 egyforma fajtájúak, pl.

3 = (3 - 3)

SIZE(NEW) = 0

3. más wff-kből és és az elsőrendű predikátum kalkulus kvantoraiból felépített kifejezés, pl.

forall s:STING [ ~IS_IN(NEW, s) ]

Egy specifikációra vonatkozó elmélet a fenti halmaz egy részhalmaza. Ez a részhalmaz zárt a rákövetkezési szabályok egy halmazára, azaz tartalmazza az összes wff-t, amelyek levezethetők egy axióma- és egy rákövetkezési szabályhalmazból. Ez a fejezet a beépített rákövetkezési szabályokról szól, arról a módszerről, melyben a specifikáció új axiómákat vezet be, és két szerkezetet, melyekkel a specifikáció új rákövetkezési szabályokat vezet be.

Egy jellemzés axiómáit arra használjuk, hogy megvizsgáljuk a szavak által jelölt értékek egyenlőségét, azaz a t1= t2 egyenlőségeket, ahol t1 és t2 egyforma fajtájú. Egy példát már láttunk erre a vizsgálatra, amikor a DELETE-t tartalmazó kifejezést oly módon redukáltuk, hogy ne tartalmazzon DELETE-t. Az ilyen vizsgálatok formalizálása egyszerű. Az jellemzésekben megjelenő egyenlőségek az axiómák. Az öt alapszabály a következő:

Reflexivitás:
    minden t szóra: t = t
Szimmetria:
    minden t1 és t2 szóra: t1 = t2 => t2 = t1
Tranzitivitás:
    minden t1, t2 és t3 szóra: t1 = t2 & t2 = t3 => t1 = t3
Helyettesíthetőség:
    minden N változós f függvényre: t = s => f(t1,...,t,...tN) = f(t1,...,s,...tN)
Példányosítás:
    minden t, t1, t2 szóra, és x változóra: t1 = t2 => t1[t for x] = t2[t for x] 
    ahol t[s for x]: t-ben x minden szabad előfordulása az s szóval helyettesítve

Egy példa a példányosításra:

(SIZE(t) = 0)[NEW for t] = (SIZE(NEW) = 0)

A fenti szabályok mellett a specifikációs nyelvünkben szerepelnek még a BOOL fajta axiómái és a rákövetkezési szabályok halmaza. A BOOL axiómák definiálják a jelentését például a & (és) és | (vagy) függvényeknek, amelyek formális specifikációját nem adjuk meg. Továbbá használjuk még az elsőrendű predikátum kalkulus axiómáit és rákövetkezési szabályait, amelyekkel többek között a kvantorokat fejthetjük ki.

Ebből az egyszerű konstrukcióból következik, hogy egy jellemzés elmélete közvetlenül levezethető a jellemzés axiómáiból. Nincs arra vonatkozó metaszabály, hogy ha két szó nem bizonyíthatóan egyező, akkor nem egyezőnek kell őket tekinteni, de ennek az ellenkezőjére sincs metaszabály. Belátható, hogy a fenti alapszabályokkal a STRING_TABLE ismertetett specifikációja alapján

SIZE(ADD(ADD(NEW, x, y), x, z) = 1

Bonyolultabb elméletek bizonyításához szükség van további eszközökre. A generated by és a partitioned by két ilyen eszköz. Azt mondjuk, hogy egy S fajtát egy F függvényhalmaz generál (generated by), ha a fajta minden szava ekvivalens egy olyan szóval, amelynek legkülsőbb függvénye az F eleme. Például a természetes számokra mondhatjuk, hogy

generated by [0, successor]

és az egészekre, hogy

generated by [0, successor, predecessor]

Azt mondjuk, hogy egy S fajtát egy F függvényhalmaz particionál (partitioned by), hogy ha két nem-egyenlő szó esetén a különbséget mindig meg tudjuk vizsgálni az F elemeivel. Ekkor két szó egyenlő, ha F elemeivel nem tudunk különbséget tenni köztük.

A STING_TABLE_SPEC specifikációja nem teljes, ugyanis nem-definiált fajtákon és függvény azonosítókon alapul. Korábban említettük, hogy számos más fajta szerepel a STRING_TABLE_SPEC jellemzésében - pl. INT, STING és STRING_TABLE. Ezen fajták mindegyike rendelkezik hozzá tartozó függvényekkel, amelyekből néhányat a STING_TABLE_SPEC-ben is felhasználtunk - pl. a + az INT, az ó STRING és a FALSE BOOL fajta függvénye. A BOOL fajtának és függvényeinek előre definiál jelentésük van a specifikációs nyelvben, így minden BOOL függvénynek ismerjük a jelentését. Ezen kívül mást nem tekintünk definiáltnak egy jellemzésben. Jelen esetben a STRING és az INT jelentése nem definiált a STING_TABLE_SPEC-ben,

A legegyszerűbb megoldás a specifikáció kibővítése lenne a szükséges definíciókkal. Tehát az INT függvények axiómáit hozzáadhatnánk a STING_TABLE_SPEC specifikációjához. Ez azonban csökkentené a modularitást; olyan lenne, mintha egy eljárás implementációját is meg kéne adnunk az eljárás hívása esetén. Amit tenni szeretnénk, az az, hogy egy megadott jellemzést más jellemzésekben felhasználunk. Ezt jellemzés importálással tehetjük meg. Példáu a STING_TABLE_SPEC jellemzésében a

imports INT_SPEC, STING_SPEC

kifejezés hozzáadásával tehetjük meg. Amikor egy jellemzést importálunk egy másik jellemzésbe, akkor az importáló jellemzés megkapja az importált jellemzés minden függvény deklarációját, egyenlőségét, generated by és partitioned by kifejezéseit.

Az importálást elsősorban a specifikációk átláthatóságának növelésére használjuk. Ezen kívül további ellenőrzést ad: az importált jellemzés függvényeit nem szoríthatjuk meg sem az importáló sem az más importált jellemzésekben. Minden importált jellemzés önmagában is értelmezhető. Ebből következik, hogy például a + függvény pontosan ugyanazt jelenti a STRING_TABLE_SPEC-ben és az INT_SPEC-ben.

Egy segéd specifikáció helyességének alapvető kritériuma, hogy felhasználhassuk interfész specifikációk írására. Ez a feltétel nem formalizálható. Van azonban két formális fogalom, amelyek nagy segítséget nyújtanak a segéd specifikációk kiértékelésében és így a konstrukciójukban is: belső konzisztencia és elégséges-teljesség.

Ha a TRUE=FALSE egyenlőséget tartalmazza egy jellemzés elmélete, akkor a jellemzést belsőleg inkonzisztensnek nevezzük. Ha a TRUE=FALSE egyenlőséget bevezetjük egy jellemzéshez kapcsolódó elméletben, akkor minden jól-formált formula az elmélet részévé válik. Röviden, ha be tudjuk látni, hogy TRUE=FALSE, akkor mindent be tudunk látni. Világos, hogy minden belső inkonzisztencia kerülendő.

A belső inkonzisztenciák abból adódnak, ha egy jellemzésről túl sokat állítunk, azaz , ha két szót egyenlőségét és nem egyenlőségét is megszorítjuk. Az is problémát okozhat, ha nem mondunk eleget egy jellemzésben.

Az elégséges-teljesség a jellemzések számára egy hasznos teljesség fogalom. Azokra a jellemzésekre alkalmazható, amelyek tartalmaznak generated by részt. A generated by egy olyan függvényhalmazt definiál, amely elégséges a fajta minden értékének generálásához. Egy

S generated by [f1, ..., fn]

generated by részt tartalmazó specifikáció elégséges-teljességéhez be kell hogy lássuk, hogy
1. A S fajta minden változó mentes, S értékkészletű függvényt tartalmazó szavai, bizonyíthatóan egyenlőek azon szavakkal, amelyek minden S értékkészletű függvényei csak az f1, ..., fn lehetnek.
2. Minden változó mentes, nem S fajtájú szavak bizonyíthatóan egyenlőek azokkal a szavakkal, amelyek nem tartalmaznak S értékkészletű függvényt.

Ha ez a két feltétel teljesül, akkor elég axiómánk van.

A következő példa az INT_ARRAY_SPEC jellemzést definiálja, amit felhasználhatunk egy általános CLU-s egész tömb definiálására. Ezt a jellemzést a későbbiekben egy interfész specifikációjában felhasználjuk. Az INT_ARRAY_SPEC jellemzésben számos észrevételt tehetünk. A jellemzésben specifikált függvényhalmaz nem minimális. Vegyük észre, hogy a specifikáció nem elégséges-teljes. A FETCH(NEW(1), 1) vagy a REMOVEH(NEW(1)) szavakat nem tudjuk redukálni. Ez a nem teljesség azonban ártatlan, ugyanis nem érinti az INT_ARRAY_SPEC-et használó interfész specifikációjának jelentését.

INT_ARRAY_SPEC: trait
  
  imports INT_SPEC
  
  introduces
    NEW: INT -> INT_ARRAY
    APPENDH: INT_ARRAY, VAL -> INT_ARRAY
    REMOVEH: INT_ARRAY -> INT_ARRAY
    ASSIGN: INT_ARRAY, INT, VAL -> INT_ARRAY
    FETCH: INT_ARRAY, INT -> VAL
    IS_IN: VAL, INT_ARRAY -> BOOL
    LBOUND: INT_ARRAY -> INT
    HBOUND: INT_ARRAY -> INT
    LENGTH: INT_ARRAY -> INT
    IS_DEFINED: INT_ARRAY, INT -> BOOL
    SAME_BOUNDS: INT_ARRAY, INT_ARRAY -> BOOL
    
  constrains INT_ARRAY so that
    INT_ARRAY generated by [APPENDH, NEW]
    INT_ARRAY partitioned by [FETCH, SAME_BOUNDS]
    for all [a, a1, a2: ARRAY, v, v1: VAL, i, j: INT]
    
      LBOUND(NEW(i)) = i
      LBOUND(APPENDH(a, v)) = LBOUND(a)
      
      HBOUND(NEW(i)) = i + 1
      HBOUND(APPENDH(a, v)) = HBOUND(a) + 1
      
      LENGTH(a) = HBOUND(a) - LBOUND(a) + 1
      
      IS_IN(v, NEW(i)) = FALSE
      IS_IN(v, APPENDH(a, v)) = ((v = v1) | IS_IN(v, a))
      
      IS_DEFINED(a, j) = (J >= LBOUND(a) & j <= HBOUND(a))
      
      FETCH(APPENDH(a, v), j, v1) = if i = HBOUND(a) then v else FETCH(a, i)
      
      SAME_BOUNDS(a1, a2) = (LBOUND(a1) = LBOUND(a2) & HBOUND(a1) = HBOUND(a2))
      
      REMOVEH(APPENDH(a, v)) = a
      
      ASSIGN(NEW(i), j, v) = NEW(i)
      ASSIGN(APPENDH(a, v), j, v1) = if j = HBOUND(a) + 1 
          then APPENDH(a, v1)
          else APPENDH(ASSIGN(a, j, v1), v)

A következőkben CLU eljárások és típusok specifikációjával foglalkozunk. Egy eljárás formális specifikációja három részből áll:
1. A fejléc megadja a nevét, az inputjainak és outputjainak típusát, és a szignálokat, amelyeket kiválthat.
2. A body megfogalmazza az inputokkal kapcsolatos feltételeket és specifikálja az eljárás hatásait, ha a feltételek teljesülnek.
3. A segéd specifikáció. Ebben a fejezetben feltesszük, hogy a segéd specifikáció az eljárás argumentumainak és eredményeinek típusaihoz kapcsolódó jellemzések uniója.

A fejléc ugyanazokat az információkat tartalmazza, mint egy informális eljárás specifikációja tartalmaz. Szintaktikus megszorításokat specifikál, amelyeknek teljesülnie kell az eljárás minden implementációjában.

A body ugyanolyan fajta információkat tartalmaz, mint egy informális specifikáció body-ja, csak a leírás módja szigorúbb. A body megszorításokat fogalmaz meg az argumentumokra, amelyekkel az eljárás meghívódik és definiálja a megfelelő argumentumokkal meghívott eljárás viselkedésének lényeges aspektusait. A body-ra úgy gondolhatunk, mint két predikátumra, az egyik megszorításokat ad meg melyeknek az eljárás hívásakor teljesülniük kell, a másik az implementációra tesz kikötéseket. A szignatúrák:

Pre: Arguments -> BOOL
Post: Arguments, Results -> BOOL

A

requires Pre
effects Post

alakú body azt jelenti, hogy ha a Pre predikátum fennáll az eljárás hívásakor, akkor az eljárás lefut és befejezéskor a Post predikátum fog fennállni. A specifikáció nem szól az eljárás viselkedéséről abban az esetben, ha a Pre nem teljesül; azaz a két predikátum pontosan megegyezik a Pre => Post predikátummal.

Háromféle azonosító és függvényszimbólum jelenhet meg a requires és effects predikátumokban:
1. lokálisan kötött logikai változók
2. formális argumentumok és
3. a segéd specifikáció által definiált azonosítók és szimbólumok.

Például a

div = proc(i, j: int) returns (ans: int)
  requires j >= 0
  effects i >= ans * j & ~exist k: INT [ k > ans & i >= j *k ]

specifikációban k egy logikai változó, i , j és ans formális argumentumok és 0, >, >=, * és INT az int típusnak megfelelő segéd specifikációból (INT_SPEC) jönnek. A specifikáció body-jában a formális argumentumok lehetnek nem minősítettek vagy a pre, post és obj minősítők által minősítettek. Egy obj által minősített formális argumentum, pédául x_obj, a formális objektumhoz kötött objektumot jelenti. Egy pre által minősített formális argumentum, például x_pre, az eljárás hívásakori értékét jelenti a formális argumentumhoz kötött objektumnak. Egy post által minősített formális argumentum, például x_post, eljárás visszatéréskori értékét jelenti a formális argumentumhoz kötött objektumnak. A nem minősített argumentum a pre-vel minősített argumentum rövidítése. A nem minősített visszatérési érték a post-al minősített rövidítése.

A következő specifikáció egy olyan eljárást definiál, ami az x tömbből eltávolítja az elemeket, átrakja az y tömbbe és az x alsó határát beállítja i-re:

move = proc(x, y: int_array, i: int)
  requires ~(x_obj = y_obj)
  effects x_post = x & y_post = NEW(i)

Ebben a specifikációban az x-nek és az y-nak különböző objektumokat kell jelenteniük; arról nem, szól, hogy hogyan viselkedik a move, ha x és y megegyezik. A requires feltételben az egyenlőség az objektumok egyenlőségéről és nem az értékek egyenlőségéről szól. Az értékek egyenlőségét például a

y_post = x

feltétel jelentené.

A CLU rendelkezik öt beépített jelöléssel, amellyel a gyakran használt predikátumokat írhatunk le. Annak leírására, hogy egyes objektumokat nem változtat meg az eljárás a

modifies at most (o1, ..., on)

predikátum szolgál. Jelentése, hogy az eljárás legfeljebb az {o1, ..., on} halmaz részhalmazát változtatja meg. Ez a predikátum mindig objektumokról szól, úgyhogy mindig használnunk kell az obj módosítót, például

modifies at most (x_obj)

A

modifies nothing

a

modifies at most ()

predikátummal ekvivalens.

A

new (o)

predikátum azt állítja, hogy, amikor az eljárás visszatér, akkor egy új, o objektum keletkezett a hívó fél környezetében elérhető objektumok univerzumában. A new predikátum, a modifies-hoz hasonlóan csak objektumokra értelmezett.

A

returns

predikátum azt állítja hogy az eljárás normálisan tér vissza, azaz nem abortál, nem fut örökké és nem vált ki szignált.

A

signals name

ahol a név egy, a specifikáció fejlécében felsorolt kivétel, azt állítja, hogy az eljárás kiváltja a név kivételt.

Ebben a fejezetben egy olyan módszert mutatunk be, amely elsősorban az általánosan használt specifikációk olvasásának megkönnyítésére szolgál. Először a modifies predikátumot választjuk el az effects állítástól. Így a

requires Pre
modifies M
effects Post

alakú body jelentése

Pre => (modifies M & Post)

A modifies predikátum azon objektumoknak a halmazát adja meg, amelyeket az eljárás megváltoztathat. Ez vagy

modifies nothing

vagy

modifies (o1, ..., on)

alakú.

A requires és effects predikátumok jelentős belső struktúrával rendelkeznek, amely a következőkből épülhet fel:
1. a specifikáció segéd részében definiált függvény szimbólumok
2. formális argumentumok és azok módosítója
3. az elsőrendű predikátum kalkulus kötőszavai és kvantorai
4. CLU-specifikus predikátumok
5. speciális kötőszavak: if-then, if-then-else (mindkettő a requires és effects predikátumokban is előfordulhat) és case (csak az effects predikátumban)

Az "if P then Q" predikátum megegyezik a "P=>Q" predikátummal. Az "if P then Q else R" predikátum pedig megegyezik a "(P->Q) & (~P=>R)" predikátummal. Ezek az alakok elsősorban a beágyazott feltételek esetén hasznosak. A case predikátum általános alakja:

normally PostPred
except signals exc_1 when PrePred_1 ensuring PostPred_1
  ...
  signals exc_n when PrePred_n ensuring PostPred_n

(returns | signals exc_1 | ... | signals exc_n ) &
(returns => PostPred & ~(PrePred_1 | ... | PrePred_n) ) & 
(signals exc_1 => (PrePred_1 & PostPred_1) ) &
...
(signals exc_n => (PrePred_n & PostPred_n) )

Ez a szemantika megengedi a szignálok nem-determinisztikus kiváltódását. Ha az előfeltételek implikálnák az eredményeket, azaz

PrePred_i => signals exception_i & PostPred_i

lenne a formalizált leírásban akkor a nem-determinizmusra nem lenne lehetőség.

Ha egy ensuring állítás "ensuring TRUE" alakú, akkor elhagyhatjuk azt.

Az itt ismertetett szintaxissal egy példa, illusztrálva a nem-determinisztikus specifikációt is:

find_in_range = proc(a: int_array, x, y: int)
    signals (els_too_small, els_too_big, wrong_xy)
  requires for all i, j: INT [ (i <= j & IS_DEFINED(a, i) & IS_DEFINED(a, j)) =>
    FETCH(a, i) <= FETCH(a, j) ]
  modifies nothing
  effects
    normally exist i: INT [ FETCH(a, i) = z ] & x < z & z < y
    except
      signals els_too_small when ~exist i: INT [ IS_DEFINED(a, i) & a[i] > x ]
      signals els_too_big when ~exist i: INT [ IS_DEFINED(a, i) & a[i] < y ]
      signals wrong_xy when ~(x < y)

Egy adatabsztrakció interfész specifikációjának legnagyobb részét a hozzá tartozó segéd specifikáció és műveleteinek specifikációja adja. A specifikáció három részből áll: 1. A fejléc adja meg a típus nevét, hogy az objektumok megváltoztathatók-e és a műveletek nevét. 2. A kapcsolat rész köti össze a specifikációban megjelenő típusokat a segéd specifikációban megjelenő fajtákkal. 3. Minden egyes művelet specifikációja. Ezek az eljárások interfész specifikációi, amit az előző részben láttunk.

A fejlécben található információ megegyezik az informális leírás fejlécében található információkkal.

A kapcsolat rész az informális leírás overview részének helyét veszi át. Egy segédsepcifikációt a jellemzés nevével illesztünk be. A kapcsolat rész az interfész specifikációbeli típusok és az importált jellemzések között is kapcsolatot teremt. Általában a típus nevek nagyon hasonlóak a hozzájuk tartozó fajták nevéhez. Ez egy tervezési egyezés, nincs formális jelentése, Így ezeket a kapcsolatokat explicit módon meg kell adni.

Végül álljon itt az 9.2-es fejezetben szereplő INT_ARRAY_SPEC segédspecifikáció felhasználásával az int_array interfész specifikációja:

int_array mutable type
  exports [create, addh, remh, high, store, fetch, equal, similar]
  
  based on sort INT_ARRAY from INT_ARRAY_SPEC with [int for INT]
  
  create = proc(i: int) returns (a: int_array)
    modifies nothing
    effects new(a_obj) & a = NEW(i)
  
  addh = proc(a: int_array, i: int)
    modifies at most (a_obj)
    effects a_post = APPENDH(a, v)
  
  remh = proc(a: int_array) returns (v: int) signals (bounds)
    modifies at most (a_obj)
    effects
      normally a_post = REMOVEH(a) & v = FETCH(a, HBOUND(a))
      except signals bounds when HBOUND(a) - LBOUND(a) < 0
        ensures modifies nothing
  
  high = proc(a: int_array returns (i: int)
    modifies nothing
    effects i = HBOUND(a)
  
  low = proc(a: int_array returns (i: int)
    modifies nothing
    effects i = LBOUND(a)
  
  store = proc(a: int_array, i: int, v: int) signals (bounds)
    modifies at most (a_obj)
    effects
      normally a_post = ASSIGN(a, i, v)
      except signals bounds when ~IS_DEFINED(a, i)
        ensures modifies nothing
  
  fetch = proc(a: int_array, i: int) returns (v: int) signals (bounds)
    modifies nothing
    effects
      normally v = FETCH(a, i)
      except signals bounds when ~IS_DEFINED(a, i)
  
  equal = proc(x: int_array, y: int_array) returns (b: bool)
    modifies nothing
    effects b = (x_obj = y_obj)
  
  similar = proc(x: int_array, y: int_array) returns (b: bool)
    modifies nothing
    effects b = (x = y)