Postvillkor - Postcondition

I datorprogrammering är en postvillkor ett villkor eller predikat som alltid måste vara sant strax efter utförandet av någon kodsektion eller efter en operation i en formell specifikation . Postvillkor testas ibland med påståenden i själva koden. Ofta ingår postvillkor helt enkelt i dokumentationen för det berörda kodavsnittet.

Till exempel: Resultatet av en faktoria är alltid ett heltal och större än eller lika med 1. Så ett program som beräknar faktorn för ett inmatningsnummer skulle ha efterförutsättningar att resultatet efter beräkningen är ett heltal och att det är större än eller lika med 1. Ett annat exempel: ett program som beräknar kvadratroten för ett inmatningsnummer kan ha efterförutsättningarna att resultatet är ett tal och att dess kvadrat är lika med ingången.

Postvillkor i objektorienterad programmering

I vissa tillvägagångssätt för programvarudesign är postvillkor, tillsammans med förutsättningar och klassinvarianter , komponenter i programvarukonstruktionsmetoden enligt kontrakt .

Efterförutsättningen för varje rutin är en deklaration av de fastigheter som garanteras när rutinen har genomförts. Eftersom det hänför sig till rutinkontraktet, erbjuder postvillkoren försäkran till potentiella uppringare att i de fall då rutinen anropas i ett tillstånd där dess förutsättning gäller, säkerställs de egenskaper som deklareras av postconditionen.

Eiffel exempel

Följande exempel skrivet i Eiffel ställer in värdet på ett klassattribut hourbaserat på ett uppringt argument a_hour. Postvillkoret följer nyckelordet ensure. I det här exemplet garanterar postvillkoret, i de fall då förutsättningen gäller (dvs. när det a_hourrepresenterar en giltig timme på dagen), att efter att körningen set_hourhar klassattributet hoursamma värde som a_hour. Taggen " hour_set:" beskriver denna postcondition-klausul och tjänar till att identifiera den i händelse av en runtime postcondition-kränkning. 

    set_hour (a_hour: INTEGER)
            -- Set `hour' to `a_hour'
        require
            valid_argument: 0 <= a_hour and a_hour <= 23
        do
            hour := a_hour
        ensure
            hour_set: hour = a_hour
        end

Postvillkor och arv

I närvaro av arv gör rutinerna som ärvda av efterkommande klasser (underklasser) det med sina kontrakt, det vill säga deras gällande förutsättningar och eftervillkor. Detta innebär att alla implementeringar eller omdefinitioner av ärvda rutiner också måste skrivas för att följa deras ärvda kontrakt. Postvillkor kan ändras i omdefinierade rutiner, men de kan bara förstärkas. Det vill säga den omdefinierade rutinen kan öka fördelarna som den ger klienten, men kanske inte minska dessa fördelar.

Se även

Referenser