Kihagyás

12. gyakorlat

parbegin:
    #Q1
    random utasítás
    ||
    #Q2
    S1()
    ---- #Q21
    S2()
    #R2
parend

Atomi művelet

\(<S_1; S_2>\)

Struktogramban szaggatott vonal

Atomi művelet levezetési szabálya:

\(Q \Rightarrow \text{lf}(<S>, R)\)

ha

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

Várakozó utasítás

await guard then S ta

Struktogram jelölése: félkör ív

\(Q \Rightarrow \text{lf}(V, R)\)

ha:

  1. \(Q \Rightarrow \chi_{D_{\text{guard}}}\)
  2. \(Q \land \text{guard} \Rightarrow \text{lf}(S, R)\)

1. feladat

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

\(B = (o)\)

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

\(R = (x = 0)\)

parbegin:
    await x=0 then SKIP ta # ez legyen a V program
    ||
    x = 0
parend

Kód kép

(Megjegyzés: a kupolás jelölés az await)

pl: \(S = \{12 \to <12, 0>, \ldots\}\)

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

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

\(R_1 = (x=0)\)

\(R_2 = (x=0)\)

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

PLSz:

  1. \(Q \Rightarrow Q_1 \land Q_2\)
  2. \(R_1 \land R_2 \Rightarrow R\)
  3. I. ág helyessége: \(Q_1 \Rightarrow \text{lf}(V, R_1)\)
    • VLSz
  4. II. ág helyessége: \(Q_2 \Rightarrow \text{lf}(x:=0, R_2)=(x \in D_{p(x:=0)} \land R_2^{x \leftarrow 0})=(0=0)=\text{igaz}\)
  5. Interferencia mentesség:
    • I. ág \(\not\leadsto\) II. ág
      • Nincs kritikus utasítás az I. ágban
    • II. ág \(\leadsto\) I. ág
      • \(\{Q_2\} x := 0 \leadsto Q_1, R_1\)
        • \(Q_1 \land Q_2 \Rightarrow \text{lf}(x:=0, Q_1) = (\text{igaz} \land Q_1^{x \leftarrow 0})=\text{igaz0}\)
        • \(R_1 \land Q_2 \Rightarrow \text{lf}(x:=0, R_1) = (\text{igaz} \land R_1^{x \leftarrow 0}) = (0 = 0)\)

VLSz:

  1. \(Q_1 \Rightarrow x \in \overbrace{D_{x=0}}^{A}=\text{igaz}\)
  2. \(Q_1 \land (x=0) \Rightarrow \text{lf}(SKIP, R_1)=R_1=(x=0)\)

HP (holt pont vizsgálat) (nem Háry Péter):

  • ebben a speciális esetben:
  • holtpont = I. ág blokkolt \(\land\) II. ág vége
  • \(Q_1 \land \lnot \text{guard} \land R_2\)
  • \(text{igaz} \land x \ne 0 \land x=0\)
    • Ellentmondás, úgyhogy nincs holtpont

2. feladat

\(z=x^n\)

\(A = (x: \R, n: \N, z: \R)\)

\(B = (x': \R, n': \N)\)

\(Q = (x=x' \land n=n')\)

\(R = (z = x'^{n'})\)

# Q
z = 1
# \overline{Q}
parbegin:
    # Q_1
    while n != 0: # invariáns állítás: P. Termináló függvény: t
        await n%2 != 0 then
            z, n = z*x, n-1
        ta
    # R_1
    ||
    # Q_2
    while n != 0: # invariáns állítás: P. Termináló függvény: t
        await n%2 == 0 then
            x, n = x*x, n/2
        ta
    # R_2
parend

\(\overline{Q} = (Q \land z=1)\)

\(Q_1 = Q_2 = P = (z\cdot x^n=x'^{n'})\)

\(R_1 = R_2 = (R \land n=0)\)

\(\text{pre}(V_1)=P \land n \ne 0\)

\(\text{pre}(V_2)=P\)

Hogy csináljuk a pénteki zh-n?

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

SzLSz:

  1. \(Q \Rightarrow \text{lf}(z := 1, \overline Q)=(\text{igaz} \land \overline{Q}^{z \leftarrow 1})=(Q^{z \leftarrow 1} \land 1=1)=Q\)
  2. \(\overline Q \Rightarrow \text{lf}(\text{PAR}, R)\)

PLSz:

  1. be: \(\overline{Q} \Rightarrow Q_1 \land Q_2 = P\)
    • \(z=1 \land x=x' \land n=n' \Rightarrow (z \cdot x^n=x'^{n'})\)
    • \(1\cdot x^n=x^n\)
  2. ki: \(R_1 \land R_2 \Rightarrow R\)
  3. I. ág: \(Q_1 \Rightarrow \text{lf}(S_1, R_1)\)
  4. II. ág
  5. Interferencia mentesség

I. ág: CLSz

  1. \(P \land n \ne 0 \land n=t_0 \Rightarrow \text{lf}(V_1, P \land n < t_0)\)
    • VLSz 2. 3. 4. 5.

VLSz:

  1. \(P \land n \ne 0 \land n=t_0 \Rightarrow (x, n, z) \in D_{2 \nmid n} = \text{igaz}\)
  2. \(P \land n \ne 0 \land n=t_0 \land 2 \nmid n \Rightarrow \text{lf}(z, n := z\cdot x, n-1, P \land n < t_0)\)

II. ág: hasonló

IM (interferencia mentesség):

  • I. ág \(\leadsto\) II. ág
    • \(\{P \land n \ne 0\} V_1 \leadsto Q_2, R_2, P, t \leq t_0\)
    • \(Q_2 \land P \land n \ne 0 \Rightarrow \text{lf}(V_1, Q_2)\)
    • \(R_2 \land P \land n \ne 0 \Rightarrow \text{lf}(V_1, R_2)\)
      • \(R_2\) és \(n \ne 0\) ellentmondásra vezet
    • \(P \land t=t_0 \land P \land n \ne 0 \Rightarrow \text{lf}(V_1, P \land t \leq t_0)\) (ez kombinálja az utolsó kettőt)

Holtpontmentesség

Lehetséges holtpont:

  • mindkettő blokkolt vagy
    • \(P \land n \ne 0 \land 2 \nmid n \land P \land 2 \mid n = \text{hamis}\)
  • első blokkolt, második vége vagy
    • \(P \land n \ne 0 \land 2 \mid n \land R_2\)
  • első vége, második blokkolt
    • \(\underbrace{R_1}_{n=0} \land P \land 2 \nmid n = \text{hamis}\)