24.5. Definíció (Szuperpozíció).

Legyen az program az állapottér altere és az feltételes értékadás az állapottér felett definiálva oly módon, hogy az altér egyetlen változóját sem tartalmazza. Jelölje az és az utasítás szuperpozícióját (. def.). Legyen az az kiterjesztése -ra (. def.). Az a) ill. az b) , ahol alakú programokat az program és az utasítás szuperpozíciójának nevezzük.

24.6. Tétel.

(Szuperpozíció viselkedési relációja) Legyen az állapottéren adott program az alterén adott program és az . utasítás egy szuperpozíciója. Jelöljük az altéren adott logikai függvények -ra való kiterjesztését -vel. EkkorA tétel (1)-es, (2)-es, (3)-as, (4)-es pontja a UNITY szuperpozíció tételének relációs alakja [[???Cha Mis 89]].:

• ,

• ,

• ,

• ,

• ,

• ,

ahol a logikai függvény kiterjesztése és .

24.4. Megjegyzés.

Ha a szuperpozíció a) típusú, akkor a tétel (1),(2),(3) állítása a lokalitás tétel következménye.

24.6. Definíció (Feladat gyenge kiterjesztése).

az feladat kiterjesztésének gyengítése, ha az kiterjesztéséből, -ből, a típusú specifikációs feltételek elhagyásával kapjuk.

24.7. Tétel.

(Szuperpozíció levezetési szabálya) Legyen az állapottér altere és a paramétertér felett megadott feladat. Ha az program megoldja az feladatot, akkor az program és az utasítás bármely szuperpozíciója megoldja az feladat gyenge kiterjesztését.