9. gyakorlat

1. feladat

\(z = x^n\)

Feladat:

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

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

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

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

Program:

z = 1
# LOOP:
while (n != 0):
    if (n mod 2 != 0):
        z, n = z * x, n - 1
    if (n mod 2 == 0):
        x, n = x * x, n / 2

Specifikáció tétele miatt, elég belátni azt, hogy \(Q \Rightarrow \text{lf}(S, R)\)

1. SzLSz:

Legyen \(Q_1 = (Q \land z=1)\)

\(Q \Rightarrow \text{lf}(z := 1, Q_1) = \underbrace{(x, n, z) \in \overbrace{D_{p(z := 1)}}^{A}}_{triv} \land Q_1^{z \leftarrow 1}=(Q \land 1=1)\)

\(Q_1 \Rightarrow \text{lf}(\text{LOOP}, R)\) - Ezt nem igen fogjuk csak úgy bizonyítani 2. CLSz:

Legyen $P=(z \cdot x^n=x'^{n'})$ és $t = n$

1. $Q_1 \Rightarrow P$ [Ehhez kell: $x^n=x'^{n'}$]
2. $P \Rightarrow (x, n, z) \in D_{n \neq 0} = \text{igaz}$ // értelmes-e a ciklus feltétel?
3. $P \land n = 0 \Rightarrow R$

    $[P \land n = 0 \Rightarrow z \cdot x^0 = {x'}^{\, n'} \Rightarrow z = {x'}^{\, n'}]$
4. $P \land n \neq 0 \Rightarrow n > 0$
5. $P \land n \neq 0 \land n = t_0 \Rightarrow \text{lf}(\text{IF}, P \land n < t_0)$
    - Szintén nem tudjuk natúr bizonyítani

1. ELSz:

   1. \(P \land n \neq 0 \land n = t_0 \Rightarrow (x, n, z) \in \overbrace{D_{n \bmod 2 == 0}}^{A} \land (x, n, z) \in \overbrace{D_{n \bmod 2 \neq 0}}^{A}=\text{Igaz}\)

   2. \(P \land n \neq 0 \land n = t_0 \Rightarrow n \bmod 2 = 0 \lor n \bmod 2 \neq 0 = \text{igaz}\)

   3. \(P \land n \neq 0 \land n = t_0 \land n \bmod 2 \neq 0 \Rightarrow \text{lf}((z_n, n) := (z\cdot x, n-1), p \land n < t_0) = n \neq 0 \land (P \land n < t_0)^{z, n \leftarrow z \cdot x, n - 1} = (\underbrace{n \neq 0}_{\mathclap{\text{ciklusfeltétel}}} \land \underbrace{z\cdot x \cdot x^{n_1}}_{z\cdot x^n}=x'^{n'} \land \underbrace{n-1}_{n=t_0} < t_0) = \text{igaz} \land \text{igaz} \land \text{igaz} = \text{igaz}\)

   4. \(P \land n \neq 0 \land n = t_0 \land n \bmod 2 = 0 \Rightarrow \text{lf}((x, n) := (x \cdot x, \frac{n}{2}), p \land n < t_0) = P \land n \neq 0 \land n = t_0 \land n \bmod 2 = 0 \Rightarrow \text{lf} (x, n = x \cdot x, \frac{n}{2}, \; P \land n < t_0) = (\text{igaz} \land (P\land n < t_0)^{x, n \leftarrow x \cdot x, \frac{n}{2}})=(z \cdot (x \cdot x)^{\frac{n}{2}} = x'^{n'} \land \frac{n}{2} < t_0)=\text{Igaz}\)

2. feladat

Döntsük el egy természetes számról, hogy prím-e

\(A = (n:\N, l: \mathbb{L})\)

\(B = (n': \N)\)

\(Q = (n=n' \land n' \neq 1)\)

\(R = (Q \land l=(\forall k \in [2 \ldots n-1]:n \bmod k \neq 0))\)

i, l = 2, True # i: \N
while l and i < n:
    l, i = n % i != 0, i+1

Legyen:

\(P = (Q \land i \in [2 \ldots n] \land l = (\forall k \in [2 \ldots i-1]: n \bmod k \neq 0))\)

\(t = n-i\)

\(Q_1 = (Q \land l = \text{igaz} \land i = 2)\)

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

SzLSz:

1. \(Q \Rightarrow \text{lf}(l, i := \text{igaz}, 2, Q_1) = (\text{igaz}, Q_1^{l, i \leftarrow \text{igaz}, 2}) = (Q \land \text{igaz} = \text{igaz} \land 2 = 2)=Q\)
2. \(Q_1 \Rightarrow \text{lf}(\text{LOOP}, R)\)

CLSz:

1. \(Q_1 \Rightarrow P\)
2. \(P \Rightarrow (n, l, i) \in D_{l \land i < n}\)
3. \(P \land \lnot (l \land i < n) \Rightarrow R\)

\(\lnot (l \land i < n) = \lnot l \lor i \geq n\)

Esetszétválasztással érdemes megoldani

\(\begin{cases} P \land \lnot l \Rightarrow \exists k \in [2\ldots i-1]:n \bmod k = 0 \Rightarrow \text{n nem prím} \\ P \land l \land i \geq n \Rightarrow l = \forall k\in[2\ldots n-1]: n \bmod k \neq 0 \end{cases}\)

1. \(P \land l \land i < n \Rightarrow n-1 > 0\)
2. \(P \land l \land i < n \land n-1=t_0 \Rightarrow \text{lf}((l, i := n \bmod i \neq 0, i+1), P \land n-i<t_0) = (\underbrace{i \neq 0}_{\mathclap{D_{l := n \bmod i \neq 0}}} \land (P \land n-1 < t_0)^{l, i \leftarrow (n \bmod i \neq 0), i+1}) = (i \neq 0 \land Q \land i+1 \in [2 \ldots n] \land (n \bmod i \neq 0) = (\forall k \in [2 \ldots i+1-1]:i \bmod k \neq 0)) \land n - (i + 1) < t_0\)