Beteendeundertypning
I objektorienterad programmering är beteendesubtyping principen att underklasser ska tillfredsställa förväntningarna hos klienter som kommer åt subklassobjekt genom referenser av superklasstyp, inte bara när det gäller syntaktisk säkerhet (som frånvaron av "metod-ej-hittad"-fel) utan även när det gäller beteenderiktighet. Specifikt bör egenskaper som klienter kan bevisa med specifikationen av ett objekts förmodade typ hålla även om objektet faktiskt är medlem av en undertyp av den typen.
Tänk till exempel en typ Stack och en typ Queue, som båda har en put- metod för att lägga till ett element och en get- metod för att ta bort ett. Anta att dokumentationen som är associerad med dessa typer anger att typen Stacks metoder ska bete sig som förväntat för stackar (dvs. de ska uppvisa LIFO -beteende), och att typen Queues metoder ska bete sig som förväntat för köer (dvs. de ska uppvisa FIFO -beteende). Antag nu att den typen Stack deklarerades som en underklass av typen Queue. De flesta kompilatorer för programmeringsspråk ignorerar dokumentation och utför endast de kontroller som är nödvändiga för att bevara typsäkerheten . Eftersom, för varje metod av typen Queue, typ Stack tillhandahåller en metod med ett matchande namn och signatur, skulle denna kontroll lyckas. Men klienter som kommer åt ett Stack-objekt genom en referens av typen Queue skulle, baserat på Queues dokumentation, förvänta sig FIFO-beteende men observera LIFO-beteende, vilket ogiltigförklarar dessa klienters korrekthetsbevis och potentiellt leda till felaktigt beteende för programmet som helhet.
Det här exemplet bryter mot beteendeundertypning eftersom typen Stack inte är en beteendesubtyp av typen Queue: det är inte så att beteendet som beskrivs av dokumentationen av typen Stack (dvs. LIFO-beteende) överensstämmer med dokumentationen av typen Queue (som kräver FIFO-beteende) .
Däremot, ett program där både Stack och Queue är underklasser av en typ Bag, vars specifikation för get bara är att det tar bort något element, uppfyller beteendemässig subtyping och tillåter klienter att säkert resonera om korrekthet baserat på de förmodade typerna av objekten de interagera med. Alla objekt som uppfyller Stack- eller Queue-specifikationen uppfyller faktiskt också Bag-specifikationen.
Det är viktigt att betona att huruvida en typ S är en beteendesubtyp av en typ T bara beror på specifikationen ( dvs. dokumentationen ) av typ T; implementeringen av typ T, om den har någon, är helt irrelevant för denna fråga . Typ T behöver faktiskt inte ens ha en implementering; det kan vara en rent abstrakt klass. Som ett annat exempel är typen Stack ovan en beteendemässig undertyp av typen Bag även om typen Bags implementering uppvisar FIFO-beteende: det som spelar roll är att typen Bags specifikation inte anger vilket element som tas bort med metoden get . Detta betyder också att beteendesubtypning endast kan diskuteras med avseende på en viss (beteende)specifikation för varje inblandad typ och att om de inblandade typerna inte har någon väldefinierad beteendespecifikation kan beteendesubtypning inte diskuteras meningsfullt.
Verifiera beteendemässig subtyping
En typ S är en beteendesubtyp av en typ T om varje beteende som tillåts av specifikationen av S också tillåts av specifikationen av T. Detta kräver särskilt att för varje metod M av T är specifikationen av M i S starkare än den i T.
En metodspecifikation som ges av ett förutsättning P s och ett eftervillkor Q s är starkare än en som ges av ett förutsättning P t och ett eftervillkor Q t (formellt: (P s , Q s ) ⇒ (P t , Q t )) om P s är svagare än P t (dvs. P t antyder P s ) och Q s är starkare än Q t (dvs. Q s antyder Q t ). Det vill säga att stärka en metodspecifikation kan göras genom att stärka postbetingelsen och genom att försvaga förutsättningen. Faktum är att en metodspecifikation är starkare om den lägger mer specifika begränsningar på utdata för indata som redan stöddes, eller om den kräver att fler indata stöds.
Betrakta till exempel den (mycket svaga) specifikationen för en metod som beräknar det absoluta värdet av ett argument x , som specificerar ett förutsättningsvillkor 0 ≤ x och ett eftervillkor 0 ≤ resultat. Denna specifikation säger att metoden inte behöver stödja negativa värden för x , och den behöver bara säkerställa att resultatet också är icke-negativt. Två möjliga sätt att förstärka denna specifikation är genom att förstärka postvillkoret för att ange resultat = |x|, dvs resultatet är lika med det absoluta värdet av x, eller genom att försvaga förutsättningen till "true", dvs alla värden för x bör stödjas . Naturligtvis kan vi också kombinera båda, till en specifikation som säger att resultatet ska vara lika med det absoluta värdet av x , för vilket värde som helst av x .
Observera dock att det är möjligt att förstärka en specifikation ((P s , Q s ) ⇒ (P t , Q t )) utan att förstärka eftervillkoret (Q s ⇏ Q t ). Betrakta en specifikation för absolutvärdesmetoden som specificerar ett förutsättningsvillkor 0 ≤ x och ett eftervillkorsresultat = x. Specifikationen som specificerar ett förvillkor "true" och ett postcondition-resultat = |x| stärker denna specifikation, även om postcondition-resultatet = |x| stärker (eller försvagar) inte postcondition-resultatet = x. Det nödvändiga villkoret för att en specifikation med förutsättning P s och eftervillkor Qs ska vara starkare än en specifikation med förutsättning P t och eftervillkor Q t är att P s är svagare än P t och "Q s eller inte P s " är starkare än " Q t eller inte P t ". Faktum är att "resultat = |x| eller falskt" förstärker "resultat = x eller x < 0".
"Utbytbarhet"
I ett inflytelserik huvudtal om dataabstraktion och klasshierarkier vid OOPSLA 1987 programspråksforskningskonferens, sa Barbara Liskov följande: "Vad som önskas här är ungefär följande substitutionsegenskap: Om för varje objekt av typ S det finns ett objekt av typ T så att för alla program P definierade i termer av T, är beteendet hos P oförändrat när ersätts med , då är S en undertyp av T." Denna karakterisering har sedan dess varit allmänt känd som Liskov Substitution Principle (LSP) . Tyvärr har den dock flera problem. För det första, i sin ursprungliga formulering är den för stark: vi vill sällan att beteendet hos en underklass ska vara identiskt med dess superklass; att ersätta ett subklassobjekt med ett superklassobjekt görs ofta med avsikten att ändra programmets beteende, om än, om beteendemässig subtyping respekteras, på ett sätt som upprätthåller programmets önskvärda egenskaper. För det andra nämner det inget om specifikationer , så det uppmanar till en felaktig läsning där implementeringen av typ S jämförs med implementeringen av typ T. Detta är problematiskt av flera skäl, en är att det inte stöder det vanliga fallet där T är abstrakt och har ingen implementering. För det tredje, och mest subtilt, i sammanhanget med objektorienterad imperativ programmering är det svårt att exakt definiera vad det innebär att universellt eller existentiellt kvantifiera objekt av en given typ, eller att ersätta ett objekt med ett annat. I exemplet ovan ersätter vi inte ett Stack-objekt med ett Bag-objekt, vi använder helt enkelt ett Stack-objekt som ett Bag-objekt.
I en intervju 2016 förklarar Liskov själv att det hon presenterade i sitt huvudtal var en "informell regel", att Jeannette Wing senare föreslog att de "försöker ta reda på exakt vad detta betyder", vilket ledde till att de publicerade gemensamt om beteende. subtyping, och faktiskt att "tekniskt sett kallas det beteendemässig subtyping". Under intervjun använder hon inte substitutionsterminologi för att diskutera begreppen.
Anteckningar
- Parkinson, Matthew J.; Bierman, Gavin M. (januari 2008). "Separationslogik, abstraktion och arv". ACM SIGPLAN-meddelanden . 43 (1): 75–86. doi : 10.1145/1328897.1328451 .