Szerkesztő:LUCI5T/Előfeltétel a programozásban

 

A számítógépes programozásban az előfeltétel egy olyan feltétel vagy predikátum, amelynek mindig igaznak kell lennie közvetlenül a kód valamely szakaszának végrehajtása előtt, vagy a formális specifikációban szereplő művelet előtt.

Ha egy előfeltétel sérül, a kódrészlet hatása meghatározatlanná válik, így előfordulhat, hogy nem végzi el a kívánt feladatát. Az előfeltételek, amelyek hiányoznak, nem elegendőek, nincsenek formálisan igazolva (vagy helytelen kísérlet történt az igazolásukra), vagy nincsenek statikusan vagy dinamikusan ellenőrizve, biztonsági problémákat okozhatnak, különösen olyan nem biztonságos nyelvek esetében, amelyek nem erősen típusosak.

Gyakran előfordul, hogy az előfeltételek egyszerűen szerepelnek az érintett kódszakasz dokumentációjában. Az előfeltételeket időnként a kódon belüli védőelemek vagy állítások segítségével tesztelik, és egyes nyelvek speciális szintaktikai konstrukciókkal rendelkeznek ehhez.

Példa

A faktoriális függvény csak akkor van definiálva, ha paramétere nullánál nagyobb vagy azzal egyenlő egész szám. Tehát a faktoriális függvény megvalósításának előfeltétele lenne, hogy paramétere egész szám legyen , és a paraméter nullánál nagyobb vagy egyenlő legyen. Alternatív megoldásként a nyelv típusrendszere is megadható, hogy a faktoriális függvény paramétere egy természetes szám (előjel nélküli egész), amely formálisan automatikusan ellenőrizhető a fordító típusellenőrzőjével.

Ezen kívül, ahol a numerikus típusoknak korlátozott a tartománya (mint a legtöbb programozási nyelvben), az előfeltételnek meg kell határoznia a paraméter maximális értékét is, hogy elkerüljük a túlcsordulást. Például, ha a faktoriálissal számoló implementáció az eredményt egy 64 bites előjelnélküli egész számként adja vissza, akkor a paraméternek kisebbnek kell lennie 21-nél, mert a faktoriális(21) nagyobb, mint a 64 biten tárolható maximális előjelnélküli egész szám. Ahol a nyelv tartomány-alapú altípusokat támogat (például Ada), ilyen korlátozásokat automatikusan ellenőrizhet a típus rendszer. Összetettebb korlátozások formális ellenőrzése interaktív módon történhet egy bizonyítási asszisztens segítségével.

Objektumorientált programozásban

Az objektum-orientált szoftverfejlesztés előfeltételei a szerződéses tervezés lényeges részét képezik. A szerződés szerinti tervezés magában foglalja az utófeltétel és az osztályinvariáns fogalmát is.

Bármely rutin előfeltétele meghatározza az objektum állapotára vonatkozó korlátozásokat, amelyek szükségesek a sikeres végrehajtáshoz. A programfejlesztő szempontjából ez képezi a rutin hívójának szerződésben vállalt részét. A hívónak kötelessége gondoskodni arról, hogy az előfeltétel teljesüljön a rutin meghívása előtt. A hívó erőfeszítésének jutalmát a meghívott rutin utófeltétele fejezi ki.

Eiffel példa

A következő példa az Eiffel nyelvben írt rutint mutat be, amely argumentumként egy olyan egész számot vesz át, amelynek egy nap órájának érvényes értékének kell lennie, azaz 0 és 23 között, beleértve a 0-t és a 23-at is. Az előfeltételt a require kulcsszó követi. Ez meghatározza, hogy az argumentumnak nagyobbnak vagy egyenlőnek kell lennie nullával, és kisebbnek vagy egyenlőnek kell lennie 23-mal. A "valid_argument:" címke leírja ezt az előfeltétel kitételt és azonosítja azt, ha futásidőben megsértik az előfeltételt.

    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

Előfeltételek és öröklődés

Öröklődés esetén az utódosztályok (származtatott osztályok) által örökölt rutinok az eredeti előfeltételekkel együtt öröklődnek. Ez azt jelenti, hogy az örökölt rutinok bármilyen implementációját vagy újradefiniálását úgy kell megírni, hogy megfeleljenek az örökölt szerződésnek. Az előfeltételek módosíthatók az újradefiniált rutinokban, de csak gyengíthetők. Vagyis az újradefiniált rutin csökkentheti az ügyfél kötelezettségeit, de nem növelheti azokat.

Lásd még

• Tervezés szerződés alapján
• Guard (számítástechnika)
• Utófeltétel
• Hoare logika
• Feltételek által fenntartott invariánsok
• Adatbázis trigger

Hivatkozások

[[Kategória:Programozási nyelvek]] [[Kategória:Számítástechnika]] [[Kategória:Logika]] [[Kategória:Lapok ellenőrizetlen fordításokkal]]