11. gyakorlat

1. feladat

\(A = (z: \Z)\)

\(B = (z': \Z)\)

\(Q = (z=z' \land z=0)\)

\(R = (z = 3)\)

par: # Két programot futtat párhuzamosan
    # Q_1
    z = z+1 # egyik program
    # R_1
    ||      # A két programot elhatároló jelzés
    # Q_2
    z = z+2 # másik program
    # R_2

\(S = \{0 \to <0, 1, 3>, 0 \to <0, 2, 3>, \ldots\}\)

Specifikáció tétele (ST): \(Q \Rightarrow \text{lf}(S, R)\)

PLSz (Párhuzamos blokk levezetési szabálya):

\(Q_1=(z = 0 \lor z = 2)\)
\(Q_2=(z = 0 \lor z = 1)\)
\(R_1 = (z = 1 \lor z = 3)\)
\(R_2 = (z = 2 \lor z = 3)\)
Belépési kritérium:
- \(Q \Rightarrow Q_1 \land Q_2\)
- Ha a párhuzamos blokk el akar indulni, akkor el tud indulni minden ágából:
Kilépési kritérium:
- \(R_1 \land R_2 \Rightarrow R\)
- Ha mindegyik ág befejeződött, akkor a párhuzamos blokk is befejeződött
I. ág: \(Q_1 \Rightarrow \text{lf}(z:=z+1, R_1)\)
II. ág: \(Q_2 \Rightarrow \text{lf}(z:=z+2, R_2)\)
Interferencia mentesség (IM):
- "Megette a fene", ha az egyik ág sikerült, ha a két ág be tud egymásnak "kavarni". Ha kiválasztjuk bármelyik kettő ágát, akkor egyik ág se zavarja meg a másiknak a működését
- A kritikus utasítások nem fogját megsérteni a másik ág annotációs utasításait
- I. ág \(\leadsto\) II. ág:
  - \(\{Q_1\} z := z+1 \leadsto Q_2, R_2\)
  - a) \(Q_2 \land Q_1 \Rightarrow \text{lf}(z := z+1, Q_2)\)
  - b) \(R_2 \land Q_1 \Rightarrow \text{lf}(z:=z+1, R_2)\)
- II. ág \(\leadsto\) I. ág:
  - \(\{Q_2\} z := z+2 \leadsto Q_1, R_1\)
  - c) \(Q_1 \land Q_2 \Rightarrow \text{lf}(z = z + 2, Q_1)\)
  - d) \(R_1 \land Q_2 \Rightarrow \text{lf}(z:=z+2, R_1)\)

\(a \leadsto b\): \(a\) veszélyes lehet \(b\)-re

1. feladat bizonyítás

\(Q \Rightarrow Q_1 \land Q_2\)
\(R_1 \land R_2 \Rightarrow R\)
- \((z=1 \land z=2) \lor (z=1 \land z=3) \lor (z=3 \land z=2) \lor (z=3 \land z=3)\)
- Ez a szörnyűség azzal ekvivalens, hogy \(z = 3\)
\(Q_1 \Rightarrow \text{lf}(z:=z+1, R_1)=(\text{igaz} \land R_1^{z \leftarrow z+1}) = (z+1=1 \lor z+1=3)\)
\(Q_2 \Rightarrow \text{lf}(z:=z+2, R_2) = \ldots\)
IM
- \(\overbrace{Q_2 \land Q_1}^{z=0} \Rightarrow \text{lf}(z := z+1, Q_2)=(\text{igaz} \land Q_2^{z \leftarrow z+1})=(z+1=0 \lor z+1=1)\)

2. feladat

\(A = (x: \N)\)

\(B = (🤖)\)

\(Q = (\text{igaz})\)

\(R = (x = 0)\)

par:
    while x > 1:
        x = x-2
    ||
    if x mod 2 != 0:
        x = x-1

\(S = \{5 \to <5, 3, 1, 0>, 5 \to <5, 3, 2, 0>, 5 \to <5, 4, 2, 0>, \ldots\}\)

\(Q_1 = Q_2 = P = \text{Igaz}\)
\(R_1 = (x \leq 1)\)
\(R_2 = (2 \mid x)\)
\(t = x\)

ST: \(Q \Rightarrow \text{lf}(S, R)\)

PLSz:

Be: \(Q \Rightarrow Q_1 \land Q_2\)
- \(Igaz \Rightarrow Igaz \land Igaz\)
Ki: \(R_1 \land R_2 \Rightarrow R\)
- \(x \leq 1 \land 2\mid x \iff x=0\)
I. ág: \(Q_1 \Rightarrow \text{lf}(S_1, R_1)\)
- CLSz
II. ág: \(Q_2 \Rightarrow \text{lf}(S_2, R_2)\)
- ELSz.
IM.:

2. feladat: CLSz

\(Q_1 \Rightarrow P\)
- Triv.
\(P \Rightarrow x \in D_{x > 1}\)
- Triv.
\(P \land x \le 1 \Rightarrow R\)
- Triv.
\(P \land x > 1 \Rightarrow x>0\)
- Triv.
\(P \land x > 1 \land x=t_0 \Rightarrow \text{lf}(x:=x-2, P \land x < t_0)\)
- \(=(x \ge 2, (P \land x < t_0)^{x \leftarrow x-2})=(\underbrace{x \ge 2}_{\text{hiszen } x>1} \land x-2 < \underbrace{t_0}_{x})\)

2. feladat: ELSZ

\(Q_2 \Rightarrow x \in D_{2 \nmid x} \land x \in D_{2 \mid x}\)
\(Q_2 \Rightarrow 2 \nmid x \lor 2 \mid x\)
\(Q_2 \land 2 \nmid x \Rightarrow \text{lf}(x:=x-1, R_2)\)
\(Q_2 \land 2 \mid x \Rightarrow \text{lf}(\text{SKIP}, R_2)\)

2. feladat: IM

Bal oldal kritikus utasítása:

\(x := x-2\)
Feltétele: \(Q_2\) és a ciklus feltétel (\(x>1\))
\(I. \leadsto II.\)
- \(\{P \land x > 1\} x:= x-2 \leadsto Q_2, R_2\)
- \(Q_2 \land P \land x > 1 \Rightarrow \text{lf}(x:=x-2, Q_2)\)
- \(R_2 \land P \land x>1 \Rightarrow\text{lf}(x:=x-2, R_2)\)
\(II. \leadsto I.\)
- \(Q_1 \land Q_2 \land 2 \nmid x \Rightarrow \text{lf}(x := x-1, Q_1)\)
- \(R_1 \land Q_2 \land 2 \nmid x \Rightarrow \text{lf}(x := x-1, R_1)\)
- \(P \land Q_2 \land 2 \nmid x \Rightarrow \text{lf}(x := x-1, P)\)
- \(t=t_0 \land Q_2 \land 2 \nmid x \Rightarrow \text{lf}(x := x-1, t \le t_0)\)

3. feladat

\(A = (x : \Z)\)
\(B = (x': \Z)\)
\(Q = (x=x')\)
\(R = (x=0 \lor x=2)\)

par:
    x = x+1
    ||
    x=0

Legyen pl.

\(Q_1 = (x = x' \lor x = 0)\)
\(Q_2 = (\text{igaz})\)
\(R_1 = x = (x' + 2 \lor x = 2)\)
\(R_2 = (x=0)\)

IM.

\(R_2 \land Q_1 \Rightarrow \text{lf}(x:=x+2, R_2)=(\text{igaz} \land x+2=0)\) - nem belátható, hibás logikai függvényeket vettünk fel

vegyünk fel egy változót, ami jelzi, hogy a jobb oldal lefutott-e már

# Q
b = false
# Q'
par:
    x = x+2
    ||
    x,b = 0,true
# R

mint beszéltük már, segédváltozót bármikor hozzáadhatunk

\(Q' = (Q \land b=\text{hamis})\)
\(Q_1 = (\lnot b \Rightarrow x=x' \land b \Rightarrow x=0)\)
\(Q_2 = (\lnot b)\)
\(R_1 = (\lnot b \Rightarrow x=x'+2 \land b \Rightarrow x=2)\)
\(R_2 = (b \land x=0)\)

Ezekkel az IM is bizonyítható lesz

Következő röpzh-ra

Párhuzamos blokk levezetése (todo)