Viselkedési altípus-meghatározás

Az objektumorientált programozásban a altípusosztály viselkedésének az elve azt jelenti, hogy a leszármazott osztályoknak meg kell felelniük azon elvárásoknak, amelyeket az osztály ősosztály típusú hivatkozásain keresztül történő elérésekor támasztanak rájuk a kliensek, nem csak a szintaktikai biztonság (például a "metódus-nem-található" hibák hiánya) szempontjából, hanem a viselkedésbeli helyesség szempontjából is. Kifejezetten azon tulajdonságoknak, amelyeket a kliensek az egy objektum feltételezett típusának specifikációja alapján bizonyíthatnak, meg kell felelniük, még akkor is, ha az objektum valójában annak a típusnak egy alfajába tartozik.

Vegyük példának a Stack és a Queue típusokat, amelyeknek mindkettőnek van put metódusa az elem hozzáadásához és get metódusa az elem eltávolításához. Tegyük fel, hogy a típusokhoz tartozó dokumentáció azt írja, hogy a Stack típus metódusai a várakozásoknak megfelelően viselkednek a veremekre vonatkozóan (azaz LIFO viselkedést mutatnak), és a Queue típus metódusai a várakozásoknak megfelelően viselkednek a sorokra vonatkozóan (azaz FIFO viselkedést mutatnak). Tegyük fel most, hogy a Stack típust a Queue típus leszármazottjaként deklarálták.

A legtöbb jelenlegi programozási nyelv fordítói figyelmen kívül hagyják a dokumentációt, és csak azokat az ellenőrzéseket végzik el, amelyek szükségesek a típusbiztonság megőrzéséhez. Mivel a Queue típus minden metódusához a Stack típus rendelkezik egy azonos nevű és szignatúrájú metódussal, ez az ellenőrzés sikeres lenne. Azonban a Queue típusra történő hivatkozással elérhető Stack objektumra támaszkodó kliensek a Queue dokumentációja alapján FIFO viselkedést várnának, de valójában LIFO viselkedést figyelnének meg, ezáltal érvényességi bizonyítványaik érvénytelenekké válnának, és a program teljes egészének helytelen viselkedéséhez vezethetne.

Ez a példa megszegi a Altípusosztály viselkedési szokásait, mert a Stack típus nem viselkedési alfajtája a Queue típusnak: nem igaz, hogy a Stack típus dokumentációjában leírt viselkedés (azaz a LIFO viselkedés) megfelel a Queue típus dokumentációjának (amely a FIFO viselkedést igényli).

Ellentétben az előző példával, egy olyan program, ahol mind a Stack, mind a Queue típusok a Bag típus leszármazottai, amelynek a get metódusának csak az a specifikációja, hogy eltávolít valamilyen elemet, teljesíti a, Altípusosztály viselkedési szokásait és lehetővé teszi a klienseknek, hogy biztonságosan következtessenek a helyességre azon objektumok feltételezett típusai alapján, amelyekkel interakcióba lépnek. Valójában bármely olyan objektum, amely megfelel a Stack vagy Queue specifikációnak, megfelel a Bag specifikációnak is.

Fontos hangsúlyozni, hogy az, hogy egy S típusú objektum viselkedési alfaj-e egy T típusú objektumnak, kizárólag a T típus specifikációján (azaz a dokumentációján) múlik; a T típus implementációja, ha van ilyen, teljesen lényegtelen ebben a kérdésben. Valójában a T típusnak nem is kell implementációja legyen; lehet tiszta absztrakt osztály is. Egy másik példa erre, hogy a Stack típus a Bag típus viselkedési alfaja, még akkor is, ha a Bag típus implementációja a FIFO viselkedést mutatja: az a fontos, hogy a Bag típus specifikációja nem határozza meg, hogy melyik elemet távolítja el a get metódus. Ez azt is jelenti, hogy a Altípusosztály viselkedési szokásai csak az egyes típusok konkrét (viselkedési) specifikációjával kapcsolatban kifejthető, és ha a résztvevő típusoknak nincsen jól meghatározott viselkedési specifikációja, akkor a Altípusosztály viselkedése nem kifejthető értelmesen.

Altípusosztály viselkedésének ellenőrzése

Egy típus S akkor tekinthető T egy viselkedés-al-típusának, ha S specifikációja engedélyezi minden olyan viselkedést, amelyet T specifikációja engedélyez. Ez azt jelenti, hogy T minden metódusára vonatkozóan S specifikációja erősebb, mint T specifikációja.

Egy metódus-specifikáció, amelyet egy előfeltétel P_s és egy utófeltétel Q_s határoz meg, erősebb, mint az egy előfeltétel P_t és egy utófeltétel Q_t által meghatározott metódus-specifikáció (formálisan: (P_s, Q_s) ⇒ (P_t, Q_t)) ha P_s gyengébb, mint P_t (azaz P_t implikálja Ps-t), és Q_s erősebb, mint Q_t (azaz Qs implikálja Q_t-t). Tehát a metódus-specifikáció megerősítése több szempontból is történhet, például azáltal, hogy szigorúbb követelményeket támaszt az eredményekre nézve az már támogatott bemenetek esetén, vagy hogy több bemenet lehetőségét támogatja.

Vegyük példának egy abszolút értéket számító metódust (nagyon gyenge specifikáció), x argumentumhoz . Ez a specifikáció egy előfeltételt határoz meg 0 ≤ x és egy utófeltételt 0 ≤ eredmény. Ez a specifikáció azt mondja, hogy a metódus nem köteles támogatni a negatív értékeket az x-ben, és csak arra kell ügyelni, hogy az eredmény is ugyan úgy ne negatív szám legyen . Két lehetséges módszer a specifikáció megerősítésére az eredményre vonatkozó utófeltétel megerősítése, ami azt állítja, hogy az eredmény megegyezik az x abszolút értékével |x|, vagy az előfeltétel gyengítése "true"-ra, vagyis minden x értéket támogatni kell. Természetesen mindkettőt kombinálhatjuk egy olyan specifikációban, amely azt mondja, hogy az eredmény minden x értékre megegyezik az x abszolút értékével.

Fontos megjegyezni, hogy lehetséges megerősíteni egy specifikációt ((Ps, Qs) ⇒ (Pt, Qt)) anélkül, hogy megerősítenénk az utófeltételt (Qs ⇏ Qt). Vegyünk például egy abszolút érték metódus specifikációját, amely előfeltételként 0 ≤ x-t, és utófeltételként result = x-t határoz meg. Az előfeltételként "true"-t és az utófeltételként result = |x|-et megadó specifikáció megerősíti ezt a specifikációt, még akkor is, ha az utófeltétel result = |x| nem erősíti meg (vagy gyengíti) az utófeltételt result = x. Az előfeltétel Ps és az utófeltétel Qs által meghatározott specifikáció akkor tekinthető erősebbnek egy Pt előfeltétel és egy Qt utófeltétel által meghatározott specifikációnál, ha Ps gyengébb, mint Pt, és "Qs vagy nem Ps" erősebb, mint "Qt vagy nem Pt". Valójában "result = |x| vagy hamis" megerősíti "result = x vagy x < 0".

"Helyettesíthetőség"

Az adatabsztrakció és az osztályhierarchiák témájában tartott jelentős hatású előadásában az 1987-es OOPSLA programozási nyelvi kutatási konferencián Barbara Liskov a következőket mondta: "Amire itt szükség van, az valami olyasmi, mint az alábbi helyettesítési tulajdonság: Ha minden S típusú o1 objektumhoz létezik egy T típusú o2 objektum úgy, hogy minden T-ben meghatározott P programra igaz, hogy a P viselkedése nem változik, ha o1 helyettesíti o2-t, akkor S T alfaja." Ez a jellemzés azóta a Liskov Helyettesítési Elv (Liskov Substitution Principle, LSP) néven ismert. Sajnos azonban több problémája van.

Először is, eredeti megfogalmazásában túl erős: ritkán szeretnénk, hogy az egyik alosztály viselkedése teljesen azonos legyen az őstípusával; egy alosztály objektumát gyakran úgy helyettesítjük az őstípus objektumával, hogy a program viselkedését megváltoztatjuk meg, bár a viselkedés-al-típus elvét tiszteletben tartva olyan módon, hogy megőrizzük a program kívánatos tulajdonságait. Másodszor, nem tesz említést a specifikációkról, ezért félreértelmezést kér, ahol a S típus implementációját összehasonlítják a T típus implementációjával. Ez több okból problémás, például nem támogatja a gyakori esetet, amikor T absztrakt és nincs implementációja. Harmadszor, és legpontosabb, pontként a tárgyilagos, imperatív objektumorientált programozás kontextusában nehéz pontosan meghatározni, mit jelent egy adott típusú objektumokra univerzálisan vagy egzisztenciálisan kvantifikálni, vagy helyettesíteni az egyik objektumot a másikkal. Az előző példában nem egy Stack objektumot helyettesítünk egy Bag objektummal, egyszerűen csak egy Stack objektumot használunk Bag objektumként. Egy 2016-os interjúban Liskov maga is elmagyarázza, hogy amit előadásában bemutatott, az egy "informális szabály" volt, majd Jeannette Wing azt javasolta, hogy próbálják meg "pontosan kitalálni, mit jelent mindez", ami vezetett közös publikációjukhoz a viselkedési al-típusozásról, és valójában "technikailag viselkedési al-típusozásnak nevezik". Az interjú során nem használ helyettesítési terminológiát a koncepciók megvitatásához.

Források

• Parkinson Matthew J.; Bierman, Gavin M (2008. január) "Separation logic, abstraction and inheritance ACM SIGPLAN Notices 43(1) 75-86.