Kihagyás

10. gyakorlat

1. feladat

Egy tömb páros elemeit növeljük meg 1-gyel

\(A = (x: \Z^n)\)

\(B = (x': \Z^n)\)

\(Q = (x=x')\)

\(R = \left(\forall i:[1\ldots n]: \overbrace{\begin{cases} (2|x'[k] \to x[k]=x'[k]+1) \; \land \\ (2\not|x'[k] \to x[k]=x'[k]) \end{cases}}^{Elem(k)} \right)\)

# Q
i = 1
# Q_1
while i <= n: # P, t
    if x[i] % 2 == 0:
        x[i], i = x[i]+1, i+1

    if x[i] % 2 != 0:
        i=i+1
# R

\(Q_1 = (Q \land i=1)\)

\(P=(i \in [1 \ldots n+1] \land (\forall k\in[1\ldots i-1]: Elem(k)) \land \underbrace{(\forall k\in[i\ldots n]: x[k]=x'[k])}_{x[i\ldots n]=x'[i\ldots n]})\)

\(t = n-i+1\)

Hogy állunk neki bizonyítani (levezetni)?

A specifikáció tétele miatt elég megmutatni azt, hogy \(Q \Rightarrow lf(S, R)\)

Szekvencia levezetési szabálya:

  1. \(Q \Rightarrow \text{lf}(i := 1, Q_1)=\)

    \(((x, i) \in D_{p(i:=1)} \land Q_1^{i \leftarrow 1}) = (\text{Igaz} \land Q \land 1=1)\)

  2. \(Q_1 \Rightarrow \text{lf}(LOOP, R)\)

    Ez egy ciklus, úgyhogy használjunk CLSz-t

Ciklus levezetési szabálya

  1. \(Q_1 \Rightarrow P\) \(= (i \in [1\ldots n+1] \land \forall k \in [i \ldots i-1]: \text{elem}(k) \land x[i\ldots n]=x'[i\ldots n])\)
  2. \(P \; \land \; i > n \Rightarrow R = \text{Igaz} \quad \{P: i \in [1\ldots n+1 \land \lnot lf \Rightarrow (i = n + 1 \;\; i = n +1 \land P \Rightarrow R)]\}\)
  3. \(P \Rightarrow (x, i) \in \overbrace{D_{i \le n}}^A=\text{Igaz}\)
  4. \(P \land i \leq n \Rightarrow n-i+1>0\)
  5. \(P \land i \leq n \land n-i+1=t_0 \Rightarrow \text{lf}(IF, P \land n-i+1 \leq t_0)\) Elágazás levezetési szabálya

Elágazás levezetési szabálya

  1. \(P \land i \leq n \land n-i+1=t_0 \Rightarrow (x, i) \in D_{2|x[i]} \land (x, i) \in D_{2\not|x[i]} = i \in [1\ldots n]\)
  2. \(P \land i \leq n \land n-i+1=t_0 \Rightarrow (2|x[i] \lor 2\not|x[i])\)
  3. \(P \land i \leq n \land n-i+1=t_0 \land (2\not|x[i]) \Rightarrow lf(i := i+1, P \land n-i+1<t_0) = ((x, i) \in \overbrace{D_{p(i:=i+1)}}^{A} \land (P\land n-i+1<t_0)^{i\leftarrow i+1} ) = (\text{Igaz} \land i+1 \in [1\ldots n+1] \land \overbrace{(\forall k\in[1\ldots i]: \text{Elem}(k))}^{P \land x[i] \bmod 2 = 1 \; \land\; \text{elem}(i)} \land x[i+1\ldots n]=x'[i+1\ldots n] \land \underbrace{n-(i+1)+1}_{n-i}<\underbrace{t_0}_{n-i+1})\)

Elágazás levezetési szabálya

  1. \(P \land i \leq n \land n-i+1=t_0 \land (2|x[i]) \Rightarrow \text{lf}((x[i], i := x[i]+1, i+1), P \land n-i+1 < t_0) = (i \in [1\ldots n] \land (P \land n-i+1<t_0)^{x[i] \leftarrow x[i]+1, i\leftarrow i+1}) = (\text{Igaz} \land i+1\in[i\ldots n+1] \land (\forall k \in [1\ldots i]: Elem(k))^{x[i]\leftarrow x[i]+1} \land x[i+1\ldots n]=x'[i+1\ldots n] \land n-(i+1)+1<t_0)\)

\(\text{Elem}(i)^{x[i]\leftarrow x[i]+1} = x'[i] \bmod 2 = 1 \rightarrow x[i]+1 = x'[i]\)

\(x'[i] \bmod 2 = 0 \rightarrow x[i]+1 = x'[i]+1\)