Fogalom gyűjtemény

Állapot

Info

Legyenek $\; A_1, \dots, A_n \;$ (ahol $n \in \N$) típusérték-halmazok és $\; v_1, \dots, v_n \;$ halmazokat azonosító egyedi címkék (változók).

Az ezekből képzett $\{v_1: a_1, v_2: a_2, \ldots, v_n: a_n\} \quad (\forall \; 1 \leq i \leq n : a_i \in A)$ halmazokat állapotnak nevezzük.

Állapottér

Info

Legyenek $A_1, \dots, A_n$ (ahol $n \in \N$) típusérték-halmazok és $v_1, \dots, v_n$ halmazokat azonosító egyedi címkék (változók).

Az ezekből képzett összes lehetséges $\{v_1:a_1, \dots, v_n:a_n\}$ állapot (ahol $\forall \; i \in [1..n]: \; a_i \in A_i$) halmazát állapottérnek nevezzük.

Jele: ($v_1: A_1, \dots, v_n: A_n$)

Feladat

Info

Legyen $A$ tetszőleges állapottér. Feladatnak nevezünk egy $F \subseteq A \times A$ relációt. (Homogén binár reláció.)

Program

Info

Adott $A$ alap-állapottér esetén, legyen $\overline{A}$ "azon véges komponensű állapotterek uniója, melyeknek altere az A alap-állapottér".

\[ \overline A = \bigcup_{A \; \leq \; B}B \]

Ebben az esetben, az $S \subseteq A \times (\overline A \cup \{fail\})^{**}$ reláció program, HA:

$\mathcal D_S=A$
A végrehajtás első állapota a kiinduló állapot
A $fail$ csak a végrehajtás végén lehet
A végrehajtás utolsó állapota $A$-beli, vagy $fail$

Program függvény

Info

Az adott $S$ program $p(S) \subseteq A \times A$ programfüggvénye megadja, hogy a program bizonyos bemenetek esetén milyen állapotban terminál.

A programfüggvény csak azon állapotokon értelmezett, amely nem vezet végtelen ciklusra, vagy $fail$ állapotra.

Megoldás

Info

Egy S program megoldja az F feladatot, ha:

$\mathcal D_F \subseteq \mathcal D_{p(S)}$
- A program legalább azon bemenetekre terminál, amelyekre a feladat megoldható
$\forall a \in \mathcal D_F: p(S)(a) \subseteq F(a)$
- A program adott bemenetre a feladatnak legalább egy megoldását megtalálja, és olyat nem, ami nem megoldása

Leggyengébb előfeltétel

Info

$lf(S, R): A \to \mathbb{L}$

Az $S$ programnak az $R$ feltételre vett leggyengébb előfeltétele

Azokra az állapotokra ad igazat, amelyre az $S$ program BIZTOSAN beleterminál az $R$ igazsághalmazába

$[lf(S, R)] = \{a \in D_{p(S)} \; | \; p(S)(a) \subseteq [R]\}$

Paramétertér

Info

Egy $B$ halmaz paramétertere az $F \subseteq A \times A$ feladatnak, ha van olyan $F_1 \subseteq A \times B$ és $F_2 \subseteq B \times A$ relációk, melyre $F = F_2 \circ F_1$.

"Ha egy feladatot fel tudunk bontani két ilyen részre, akkor a közbülső halmaz lesz a paraméter tér"

Elő- és utófeltétel

Info

Előfeltétel: $[Q_b]=F_1^{-1}(b)$

Utófeltétel: $[R_b]=F_2(b)$

Specifikáció tétele - Megoldás

Info

Ha $\forall b \in B$ esetén $Q_b \Rightarrow lf(S, R_b)$, akkor $S$ megoldja az $F$ feladatot.

Szekvencia

Info

Legyen $A$ közös alap-állapottere az $S_1$ és $S_2$ programoknak.

Az $(S_1; \; S_2)$ relációt az $S_1$ és $S_2$ programok szekvenciuájának nevezzük, ha

$(S_1; \; S_2)(a) =$

$\{\alpha \in \overline{A^{\infin}} \; | \; \alpha \in S_1(a)\} \; \cup$

$\{\alpha \in (\overline{A} \cup \{\text{fail}\})^* \; | \; \alpha \in S_1(a) \, \land \, \alpha_{|\alpha|} = \text{fail}\} \; \cup$

$\{\gamma \in (\overline{A} \cup \{\text{fail}\})^{**} \; | \; \gamma = \alpha \otimes \beta \, \land \, \alpha \in S_1(a) \, \land \, |\alpha| < \infin \, \land \, \alpha_{|\alpha|} \neq \text{fail} \, \land \, \beta \in S_2(\alpha_{|\alpha|})\}$

Valami magyarázat-féle:

2 programot egymás után végzünk el (nem kompozíció)
Az első program által generált végrehajtás egy lehetséges végrehajtása lesz a szekvenciának is
Ha az első program végrehajtása adott állapotból nem véges vagy hibásan terminál, akkor a második nem tudja folytatni a végrehajtást a végpontból
Csatlakozási pont: Az az állapot egy végrehajtási sorozatban, ahol az egyik progi terminál és a második progi elindul onnan

Elágazás

Info

Legyen $A$ közös alap-állapottere az $S_1, \dots, S_n$ programoknak.

Legyenek továbbá $\pi_1, \dots, \pi_n \in A \to \mathbb{L}$ logikai függvények.

Ekkor az $\text{IF} \subseteq A \times (\overline{A} \cup \{\text{fail}\})^{**}$ relációt az $S_i$ programból képzett $\pi_i$ feltételek által meghatározott elágazásnak nevezzük és $(\pi_1: S_1, \dots, \pi_n: S_n)$-nel jelöljük, ha

\[ \forall a \in A: \text{IF}(a) \; = \; \omega_0(a) \; \cup \; \bigcup\limits_{i=1}^{n} \omega_i (a) \]

\[ \omega_i(a) = \begin{cases} S_i(a) \quad \quad \quad \quad \; \text{ha} \quad a \in D_{\pi_i} \; \land \; \pi_i(a) \\ \empty \quad \quad \quad \quad \quad \quad \text{ha} \quad a \in D_{\pi_i} \; \land \; \neg \pi_i(a) \\ \{<a, \text{fail}>\} \quad \text{ha} \quad a \not \in D_{\pi_i} \end{cases} \]

\[ \omega_0(a) = \begin{cases} \{<a, \text{fail}>\} \quad \text{ha} \quad \forall i \in [1..n]: (a \in D_{\pi_i} \; \land \; \neg \pi_i(a)) \\ \; \empty \quad \quad \quad \quad \quad \; \; \; \text{különben} \end{cases} \]

Ciklus

Info

Legyen $\pi \in A \to \mathbb{L}$ feltétel és $S_0 \subseteq A \times (\overline{A} \cup \text{fail})^{**}$ program.

A $\text{DO} \subseteq A \times (\overline{A} \cup \text{fail})^{**}$ relációt az $S_0$ programból $\pi$ feltétellel képzett ciklusnak nevezzük és $(\pi, S_0)$-lal jelöljük,

ha $\forall a \in A$:

Ha $a \in D_{\pi} \; \land \; \pi(a)$, akkor $\text{DO}(a) = (S_0; \; \text{DO})(a)$
Ha $a \in D_{\pi} \; \land \; \neg \pi(a)$, akkor $\text{DO}(a) = \{<a>\}$
Ha $a \not \in D_{\pi}$, akkor $\text{DO}(a) = \{<a, \text{fail}>\}$

Szekvencia levezetési szabálya

Info

Legyen az $S_1$ és $S_2$ programok szekvenciája $S=(S_1; S_2)$.

Ezen kívül legyenek $Q$, $Q'$ és $R$ logikai függvények.

Ekkor, ha

$Q \Rightarrow \text{lf}(S_1, Q')$
$Q' \Rightarrow \text{lf}(S_2, R)$

akkor $\;\; Q \Rightarrow \text{lf}(S, R)$

Elágazás levezetési szabálya

Info

Legyen $\text{IF} = (\pi_1:S_1, \ldots, \pi_n:S_n)$ elágazás.

Legyenek továbbá $Q$ és $R$ logikai függvények.

HA!

$Q \Rightarrow \bigwedge \limits_{i=1}^n(\pi_i \lor \lnot \pi_i) \quad$ - Mindegyik feltétel eldönthető
$Q \Rightarrow \bigvee \limits_{i=1}^n \pi_i \quad$ - Legalább az egyik feltétel igaz
$\forall i\in[i_\ldots n]:Q \land \pi_i \Rightarrow \text{lf}(S_i, R) \quad$ - Bármelyik feltétel esetén a program $R$-ben terminál

Ekkor $\;\; Q \Rightarrow \text{lf}(\text{IF}, R)$

Ciklus levezetési szabálya

Info

Legyen $\text{DO}=(\pi, S_0)$ ciklus, ahol $\pi \in A \to \mathbb{L}$ és $S_0$ program.

Továbbá legyenek $P, Q, R$ logikai függvények, és $t: A \to \Z$.

HA

$Q \Rightarrow P$
$P \land \pi \Rightarrow \text{lf}(S_0, P)$
$P \land \lnot \pi \Rightarrow R$
$P \Rightarrow \pi \lor \lnot \pi$
$P \land \pi \Rightarrow t > 0$
$P \land \pi \land t = t_0 \Rightarrow \text{lf}(S_0, t < t_0)$

Ekkor $Q \Rightarrow \text{lf}(\text{DO}, R)$

Somewhat of an explanation:

$P$ a ciklus invariáns, tehát egy olyan logikai függvény, ami a ciklus teljes "élettartama" alatt igaz.

A $t$ a terminálófüggvény, jelzi, hogy mennyi "idő" van még hátra a ciklus befejezéséig.

A $P$ szabályai:

$Q \Rightarrow P$ - Az előfeltételből következik $P$, tehát a program elején $P$ biztos igaz.
$P \land \pi \Rightarrow \text{lf}(S_0, P)$ - Ha $\pi$ igaz, tehát folytatjuk a ciklust/belépünk a ciklusba, akkor a ciklusmag lefutása után is igaznak kell lennie $P$-nek. Ez a két szabály biztosítja, hogy $P$ az egész program alatt igaz lesz
$P \land \lnot \pi \Rightarrow R$ - Ha befejeződik a ciklus (a ciklusfeltétel már nem igaz), akkor $P$-t feltételezve (ami tudjuk, hogy normális esetben mindig igaz) $R$ is igaz. Ebből következik, hogy ha a program terminál, akkor olyan állapotban terminál, amiben $R$ igaz. Viszont, ez csak akkor igaz, ha sikerül terminálni.
$P \Rightarrow \pi \lor \lnot \pi$ - A $\pi$ feltétel a ciklus teljes élettartama során eldönthető.

A $t$ ahhoz szükséges, hogy ellenőrizzük, a program tényleg terminál-e:

$P \land \pi \Rightarrow t > 0$ - $t$ pozitív, amíg a ciklus fut
$P \land \pi \land t=t_0 \Rightarrow \text{lf}(S_0, t < t_0)$ - A ciklus futása alatt, a $t$ szigorú monoton szökken. Itt elég fura a notation, a nyíl bal oldalán lévő $t=t_0$ azt jelenti, vezessük be a $t_0$ változót, ami a program lefutása előtti "idő", az lf-ben lévő $t<t_0$ pedig valójában egy függvény, ami eldönti, hogy a program végállapotának ideje kisebb-e, mint az elmentett idő.

Mivel a ciklus futása alatt a $t$ szig.min.csök, ezért előbb-utóbb negatív lesz. Viszont, amiért a program futása alatt a $t$ pozitív, csak úgy lehet negatív, ha a program már nem fut. Ezzel biztosítja, hogy a program abbahagyja a futást.

Párhuzamos blokk

Info

Legyen $A$ közös alap-állapottere az $S_1 \dots S_n$ programoknak.

$\forall \; a \in A: \; (\text{parbegin} \;\; S_1 \; || \; \dots \; || \; S_i \; || \; \dots \; || \; S_n \;\; \text{parend})(a) \; = \; \bigcup \limits_{i=1}^{n} \; B_i(a)$

ahol

$$ B_i(a) = \begin{cases}

S_i; \; (\text{parbegin} \;\; S_1 \; || \; \dots \; || \; S_{i-1} \; || \; S_{i+1} \; || \; \dots \; || \; S_n \;\; \text{parend})(a) \ \quad\quad \text{ha } S_i \text{ nem megszakítható az } a \text{ állapotból indulva} \

\

u_i; \; (\text{parbegin} \;\; S_1 \; || \; \dots \; || \; S_{i-1} \; || \; T_i \; || \; S_{i+1} \; || \; \dots \; || \; S_n \;\; \text{parend})(a) \ \quad\quad \text{ha } S_i(a) = (u_i; T_i)(a) \text{ ahol } u_i \text{ nem megszakítható az } a \text{ állapotból kiindulva}

\end{cases} $$

Párhuzamos blokk levezetési szabálya

Info

Legyenek $\; Q, Q_1, \dots, Q_n \;$ és $\; R, R_1, \dots, R_n \;$ logikai függvények.

HA

$Q \; \Longrightarrow \; Q_1 \land \dots \land Q_n \;$ és
$R_1 \land \dots \land R_n \; \Longrightarrow \; R \;$ és
$\forall i \in [1..n]: Q_i \; \Longrightarrow \; \text{lf}(S_i, R_i) \;$ és
a $Q_1 \; \Longrightarrow \; \text{lf}(S_1, R_1), \; \dots \;, Q_n \; \Longrightarrow \; \text{lf}(S_n, R_n) \;$ teljes helyességi formulák interferenciamentesek és
a párhuzamos blokk holtpontmentes

akkor $\; Q \; \Longrightarrow \; \text{lf} \; (\text{parbegin} \;\; S_1 ||\; \dots \; || S_n \;\; \text{parend}) \;$

Magyarázat:

A párhuzamos blokk levezetési szabályának első három feltétele szemléletesen azt fejezi ki, hogy

ha $Q$ előfeltétel teljesül, akkor a párhuzamos blokk bármely $S_i$ komponensprogramjának végrehajtása elkezdhető, mert teljesül a $Q_i$ előfeltétele (ezt nevezhetjük "belépési feltételnek").
amikor a párhuzamos blokk terminál (az összes $S_i$ komponens befejeződött, elérte utófeltételét) akkor jó helyen terminált: ott ahol $R$ utófeltétel igaz (ezt nevezhetjük „kilépési feltételnek”).
minden $S_i$ komponens önmagában teljesen helyes a $Q_i$ előfeltételével és $R_i$ utófeltételével adott feladatra nézve.