I programmering , speciellt objektorienterad programmering , är en klassinvariant (eller typinvariant ) en invariant som används för att begränsa objekt i en klass. Klassmetoder måste bevara det invarianta.
Under skapandet av klasser etableras deras invarianter, som ständigt upprätthålls mellan anrop till offentliga metoder. Tillfällig överträdelse av klassinvarians mellan privata metodanrop är möjlig, även om det inte är önskvärt.
En objektinvariant är en programmeringskonstruktion som består av en uppsättning invarianta egenskaper. Detta säkerställer att objektet alltid kommer att matcha de fördefinierade villkoren, och därför kan metoder alltid referera till objektet utan risk för att göra oprecisa antaganden. Att definiera klassinvarianter kan hjälpa programmerare och testare att hitta fler buggar när de testar programvara.
Den användbara effekten av klassinvarianter i objektorienterad programmering förstärks av närvaron av arv. Klassinvarianter ärvs, det vill säga invarianterna för alla föräldrar i en klass gäller själva klassen. [ett]
Arv tillåter underordnade klasser att ändra implementeringsdata för överordnade klasser, så en understigande klass kan ändra instansernas tillstånd på ett sätt som gör dem ogiltiga ur den överordnade klassens synvinkel. Att hänvisa till denna ogiltiga underordnade typ är en av anledningarna till att objektorienterade mjukvaruutvecklare föredrar inkapsling framför arv. [2]
Men eftersom klassinvarianter ärvs, består klassinvarianten för en viss klass av alla invarianta uttalanden som kodas direkt i den klassen, kombinerat med alla invarianta satser som ärvts från den klassens föräldrar. Detta innebär att medan underliggande klasser kan komma åt sina överordnade implementeringsdata, kan en klassinvariant förhindra dem från att manipulera denna data på något sätt som skapar en ogiltig instans vid körning.
Programmeringsspråk som C++ och Java stöder standardpåståenden , som kan användas för att definiera klassinvarianter . Ett vanligt exempel på implementering av invarianter i klasser är att klasskonstruktorn kastar ett undantag om invarianten inte uppfylls. Eftersom metoder bevarar invarianter, kan de acceptera giltigheten av en invariant och behöver inte explicit leta efter den.
Klassen invariant är en viktig komponent i kontraktsprogrammering . Således kommer programmeringsspråk som ger fullt stöd för kontraktsprogrammering, som Eiffel , Ada och D , också ge fullt stöd för klassinvarianter.
Java har ett kraftfullare verktyg som kallas Java Modeling Language som ger ett mer robust sätt att definiera klassinvarianter.
Programmeringsspråket D har inbyggt stöd för klassinvarianter, såväl som andra kontraktsprogrammeringstekniker. Här är ett exempel från den officiella dokumentationen.
klass Datum { int dag ; int timme ; invariant () { hävda ( 1 <= dag && dag <= 31 ); hävda ( 0 <= timme && timme < 24 ); } } EiffelI Eiffel deklareras en klassinvariant i slutet av klassen efter nyckelordet.
klass DATUM skapa fabrikat funktion { INGEN } -- Initiering make ( a_day : INTEGER ; a_hour : INTEGER ) -- Initiera `Current' med `a_day' och `a_hour'. kräver valid_day : 1 <= a_day and a_day <= 31 valid_hour : 0 <= a_hour and a_hour <= 23 do day := a_day hour := a_hour se day_set : day = a_day hour_set : hour = a_hour end funktion -- Åtkomst dag : INTEGER -- Dag i månaden för `Current' timme : INTEGER -- Timme på dygnet för `Current' funktion -- Elementändring set_day ( a_day : INTEGER ) -- Sätt 'day' till 'a_day' kräver valid_argument : 1 <= a_day och a_day <= 31 do day := a_day säkerställ day_set : day = a_day end set_hour ( a_hour : INTEGER ) -- Ställ in `hour' till `a_hour' kräver valid_argument : 0 <= a_hour och a_hour <= 23 do hour := a_hour säkerställ timme_set : timme = a_hour end invariant valid_day : 1 <= dag och dag <= 31 valid_hour : 0 <= timme och timme <= 23 slutDetta är ett exempel på en klassinvariant i programmeringsspråket Java med Java Modeling Language. Invarianten måste vara sann efter att konstruktören har slutfört och vid inträde och utträde av alla medlemmar av den offentliga funktionen, som måste definiera ett förutsättningsvillkor och ett eftervillkor för att genomdriva klassens invariant.
offentlig klass Datum { int /*@spec_public@*/ day ; int /*@spec_public@*/ timme ; /*@invariant 1 <= dag && dag <= 31; @*/ //klass invariant /*@invariant 0 <= timme && timme < 24; @*/ //klass invariant /*@ @ kräver 1 <= d && d <= 31; @kräver 0 <= h && h < 24; @*/ public Date ( int d , int h ) { // konstruktordag = d ; timme = h ; } /*@ @ kräver 1 <= d && d <= 31; @försäkrar dag == d; @*/ public void setDay ( int d ) { day = d ; } /*@ @ kräver 0 <= h && h < 24; @säkrar timme == h; @*/ public void setHour ( int h ) { timme = h ; } }