Utófeltétel

A számítógépes programozásban az utófeltétel egy olyan feltétel vagy predikátum, amelynek mindig igaznak kell lennie közvetlenül egy kódrészlet végrehajtása után vagy egy művelet után a formális specifikációban. Az utófeltételeket néha állítások segítségével tesztelik magában a kódban. Gyakran az utófeltételeket egyszerűen az érintett kódrész dokumentációjában tüntetik fel.

Például: A faktoriális eredménye mindig egy egész szám és nagyobb vagy egyenlő 1-gyel. Tehát egy olyan programnak, amely egy bemeneti szám faktoriálisát számítja ki, utófeltételei lennének, hogy az eredmény a számítás után egy egész szám legyen, és nagyobb vagy egyenlő legyen 1-gyel. Egy másik példa: egy olyan program, amely egy bemeneti szám négyzetgyökét számítja ki, az utófeltételek szerint az eredmény egy szám legyen, és hogy a négyzete egyenlő legyen a bemeneti számmal.

Utófeltételek az objektumorientált programozásban

Egyes szoftvertervezési megközelítésekben az utófeltételek az előfeltételekkel és az osztályinvariánsokkal együtt a szoftverkonstrukciós módszer szerződés szerinti tervezésének összetevői.

Bármely rutin utófeltétele a végrehajtás befejezése után garantált tulajdonságok deklarációja. A rutin szerződéséhez kapcsolódóan az utófeltétel biztosítékot nyújt a potenciális hívók számára, hogy azokban az esetekben, amikor a rutint olyan állapotban hívják meg, amelyben az előfeltétel teljesül, az utófeltétel által deklarált tulajdonságok garantáltak.

Eiffel-példa

A következő, Eiffel nyelven írt példa egy osztályattribútum hour értékét állítja be a hívó által megadott a_hour argumentum alapján. Az utófeltétel a ensure kulcsszót követi. Ebben a példában az utófeltétel garantálja azokban az esetekben, amikor az előfeltétel teljesül (azaz amikor a_hour a nap egy érvényes óráját jelenti), hogy a set_hour végrehajtása után az hour osztály attribútum értéke megegyezik a_hour értékkel. A " hour_set: " címke leírja ezt az utólagos feltételt, és a futásidejű utófeltétel megsértése esetén annak azonosítására szolgál.

  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

Utófeltételek és öröklődés

Az öröklődés jelenlétében az utódosztályok (leszármazott osztályok) által örökölt rutinok az előfeltételeikkel és utófeltételeikkel együtt érvényesek. Ez azt jelenti, hogy az örökölt rutinok bármely implementációját vagy újradefiniálását úgy kell megírni, hogy azok megfeleljenek az örökölt szerződéseknek. Az utófeltételek módosíthatók az újradefiniált rutinokban, de csak erősíthetők. Ez azt jelenti, hogy az újradefiniált rutin növelheti az ügyfél számára nyújtott előnyöket, de nem csökkentheti azokat.

Fordítás

Ez a szócikk részben vagy egészben a Postcondition című angol Wikipédia-szócikk ezen változatának fordításán alapul. Az eredeti cikk szerkesztőit annak laptörténete sorolja fel. Ez a jelzés csupán a megfogalmazás eredetét és a szerzői jogokat jelzi, nem szolgál a cikkben szereplő információk forrásmegjelöléseként.

Kapcsolódó szócikkek

• Előfeltétel
• Szerződésalapú programozás]
• Trigger (adatbázisok)]