Gondolatok
a típus-specifikációk
kompatibilitásának
vizsgálatáról

Eszmefuttatásom célja egy módszert vázolni, amely perspektivikus lehet annak vizsgálatában, hogy a típusok, típusosztályok algebrai, valamint a „hagyományosabb” külső felület szerinti specifikációjának^[1] egymáshoz illeszkedése nem sérül-e. A módszer egyik sarkalatos pontja a Prolog nyelv felhasználása, amely –elképzeléseim szerint– képes támogatni eme vizsgálatot. Elvárásom, hogy egy alkalmasan felépített Prolog nyelvű programmal igazolható, a típus két leírásának kompatibilitása: logikai egymáshoz illeszkedősége.

Egy ilyen módszer kidolgozásának elsősorban gyakorlati jelentősége van. Ismert [KV2001] ugyanis, hogy algebrai specifikációból formálisan is előállíthatók az érintett operációk elő- és utófeltételes specifikációi, tehát a típusosztály P/P-specifikációja. A programfejlesztés során a programozó nem az említett tétel alkalmazásával (még ha tud is róla), hanem inkább „józanésszel” jut el a típusosztály-megvalósításhoz közelebb álló (azaz egyéb operációktól függetlenül megfogalmazott) másik specifikációjához. Ekkor nagyobb „űr” tátong a kétféle specifikáció között, ami fölveti a kompatibilitás meglétének kérdését.

Egy ilyen módszer más szempontból is hasznos lehet. Ha ugyanis valóban „mechanikussá” sikerül tenni a kompatibilitás vizsgálatát, jó eséllyel akár programmal is elvégezhetővé válik az ellenőrzés.

A negyedik részben számos példával egészítjük ki az eddig leírtakat.

IV. rész
Példatár

Vázlat:

1. „Klasszikus példák”. 3

1.1. A kupac. 3

1.1.1. Algebrai specifikáció. 3

1.1.2. Exportmodul 3

1.2. A statikus gráf 3

1.2.1. Algebrai specifikáció. 3

1.2.2. Exportmodul 3

1.3. A rekurzió. 3

1.3.1. Algebrai specifikáció. 3

1.3.2. Exportmodul 3

2. Példák a „nagyvilágból”. 4

2.1. „Egervár ostroma”. 4

2.1.0. A feladat megfogalmazása. 4

2.1.1. Algebrai specifikáció. 4

2.1.2. Exportmodul 4

1. „Klasszikus példák”

1.1. A kupac

1.1.1. Algebrai specifikáció

… a prioritási sor specifikációjával megegyezik …

1.1.2. Exportmodul

… itt kell figyelembe venni a folytonos ábrázolást + a kupactulajdonság meghatározta indexelést …

1.2. A statikus gráf

1.2.1. Algebrai specifikáció

…

1.2.2. Exportmodul

…

1.3. A rekurzió

1.3.1. Algebrai specifikáció

…

1.3.2. Exportmodul

…

2. Példák a „nagyvilágból”

2.1. „Egervár ostroma”

2.1.0. A feladat megfogalmazása

2.1.1. Algebrai specifikáció

2.1.2. Exportmodul

---

^[1] Szokás az irodalomban ezt P/P-specifikációnak is nevezni, mivel az pre- és postcondition, vagyis az elő- és az utófeltétel megadását jelenti.