24.3.Szekvencia

24.3.Szekvencia
Előző	24. fejezet - Programkonstrukciók	Következő

24.7. Definíció (Szekvencia).
Legyen az állapottér altere felett, pedig az altér felett definiált program. Legyen egy logikai változó, amelyekhez tartozó állapottérkomponensek nem tartoznak sem az sem az altérhez. Jelöljük -gyel az altéren definiált programot, ahol ( . def.), ( . def.). Jelöljük -vel az állapottéren definiált programot, ahol . Legyen , Az programot az programok szekvenciájának nevezzzük, és -vel jelöljük.

A szekvenciát tehát feltételekkel kiegészített értékadások és unió segítségével definiáltuk.

Kimondunk néhány segédtételt:

24.8. Lemma (PSP).
Chandy-Misra Ha és , akkor . Biz.: strukturális indukcióval.

24.9. Lemma (Csoda kizárása és ).
Chandy-Misra Ha , akkor . Biz.: strukturális indukcióval.

24.10. Lemma.
Kozsik T. Ha , akkor . Hasonlóan: .

A feltételek gyengíthetőek. Elegendő, ha , így bármely , amelyet a kezdeti feltétel kezdetben igazzá tesz, -ből indulva is teljesül. Ha , akkor . A második állítás az első állításból és -ból következik.

24.11. Lemma.
Kozsik T. Tetszőleges programra, ha , akkor .

Az előző lemma és a PSP tétel (. lemma) felhasználásával: , azaz , így a csoda kizárásának elve (. lemma) miatt.

24.12. Tétel.
(Szekvencia viselkedési relációjáról) Legyen . Ekkor(9)-(12): Kozsik T.:

ha , akkor ,
ha , akkor ,
ha , akkor ,
ha , akkor ,
ha , akkor ,
ha , akkor ,
,
Ha akkor .
Ha , akkor és csak akkor ; valamint, ha , akkor és csak akkor .
Ha és , akkor és csak akkor .
Ha , akkor .
Ha és , akkor .

Biz.: (1), (2), (3): A ., ., ., . def. alapján könnyen belátható, hogy és . Az utóbbiból előállítása szerinti strukturális indukcióval: . A szekvencia definíciója (. def.) és . def. alapján ellenőrizhető, hogy: , és = , így alkalmazható a . tétel a , megfeleltetéssel.

(4),(5),(6): A szekvencia (. def.) és . def. alapján: . Alkalmazható a . tétel a megfeleltetéssel.

(7) Ha , akkor miatt nem lehet fixpont. Ha , akkor , ha , akkor változtat állapotot. Ezért . A másik irány a . definíció következménye.

(8) A (7)-es állítás következménye.

(9),(10) A szekvencia programjára vonatkozó leggyengébb előfeltételek kiszámításával bizonyítható.

(11)

struktúrája szerinti indukcióval. Alapesetben a . lemmát alkalmazzuk.

(12) Az első feltételből és (11)-ből: , így . Hasonlóan (6) felhasználásával: , így .

24.13. Tétel.
(Szekvencia levezetési szabálya) Legyen és az állapottér ill. altere és a paramétertér felett értelmezett determinisztikus feladat, az altéren definiált és az altéren adott szekvenciája. Tetszőleges -re jelöljük komponenseit , komponenseit indexszel. Ha megfelel a és a feltételnek a kezdeti feltétel mellett, megfelel és feltételeknek a feltétel mellett, és , akkor megfelel és feltételeknek a kezdeti feltétel mellettA tétel állítása Misra programszekvenciára vonatkozó - nem bizonyított - állításával rokon. Misra eredeti állítása a következőképpen fogalmazható meg a relációs modellben: ha , , és megfelel a specifikációs feltételnek a kezdeti feltétel mellett, akkor megfelel a specifikációs feltételnek ([[???UN 88-93]]/16-90). Misra a szekvencia fogalmát nem definiálja formálisan, így a tételt sem bizonyítja. Műveleti szemantikai megfontolásokra és a helyettesítési axiómára hivatkozva indokolja az állítás helyességét és példákon keresztül mutatja meg, hogy használata helyes következtetések levonásához vezet..

Biz.: A feltételekből a . tétel szerint . (. def.). a . tétel (3)-as pontja és a . tétel felhasználásával: . , így: .

felhasználásával .

Megjegyzés

22.11

. tétel és . def. szerint , azaz (. lemma).

Mivel , ezért a (. lemma) és a . def. (diszjunktivitás) alkalmazásával: .

Megjegyzés

21.32

. def. (tranzitivitás) alkalmazásával: .

A fentihez hasonló gondolatmenet alapján , amelyből a . tétel (6)-os pontja felhasználásával: . , így . A . def. (tranzitivitás) alkalmazásával: . . tétel (7)-es és (8)-as állításaival a tétel állítását kapjuk.

Előző	Fel	Következő
24.2.Szuperpozíció	Tartalom	25. fejezet - A modell tulajdonságai