Kihagyás

8. gyakorlat

Levezetési szabályok

1. feladat

Cseréljük ki két változó értékét

\(A = (x:\Z, \, y: \Z)\)

\(B = (x':\Z, \, y': \Z)\)

\(Q = (x=x' \; \land \; y = y')\)

\(R = (x = y' \; \land \; y = x')\)

  1. \(x,y := y,x\)

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

    \((x,y) \in D_{P(x,y:=y,x)} \land \underbrace{R^{x,y \; \leftarrow \; y, x}}_{y=y' \; \land \; x=x'}\)

  2.
    \(x := x - y\)
    Közbülső állítás: \(Q_1\)
    \(y := x + y\)
    Közbülső állítás: \(Q_2\)
    \(x := y - x\)

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

    A szekvencia levezetési szabálya (SZLSZ) miatt: Tudunk mondani olyan \(Q_1\) és \(Q_2\) közbülső állításokat, hogy

    1. \(Q \Rightarrow \text{lf}\,(x:=x-y, \;Q_1)\)
    2. \(Q_1 \Rightarrow \text{lf}\,(y:=x+y, Q_2)\)
    3. \(Q_2 \Rightarrow \text{lf}\,(x := y - x,R)\)

    Gregó tipp a megoldáshoz (levezetési szabályok)

    • Az lf alapján erre akarunk jutni
    • Egyszerű-e a feladat?
    • Megoldjuk

    Gregó szótár: ami "y"-nak néz ki, az valójában "lf"

    Legyen \(Q_1=(x=x'-y' \land y=y')\) és \(Q_2=(x=x'-y' \land y=x')\)

    1. \(Q \Rightarrow \text{lf}\,(x:=x-y, \; Q_1)=(\text{igaz}\;\land\;Q_1^{x \; \leftarrow \; x-y})=(x-y=x'-y' \land y = y')\) Trivi (a \(Q\) miatt)
    2. \(Q_1 \Rightarrow \text{lf}\,(x := x + y, \; Q_2) = (\text{igaz} \land Q_2^{y \; \leftarrow \; x + y})=(x=x'-y'\land x+y=x')\)
    3. \(Q_2 \Rightarrow \text{lf}\,(x := y -x, \; R) = (\text{igaz} \; \land \; R^{x \; \leftarrow \; y-x} ) = (y - x = y' \; \land \; y = x')\)

  3. \(A'=(x:\Z, y\Z, z: \Z)\)
    \(z := x\)
    \(x := y\)
    \(y := z\)

    Legyen:

    • \(Q_1=(x=x' \; \land \; y=y' \; \land \; z=x')\)
    • \(Q_2 = (x = y' \; \land \; y = y' \; \land \; z = x')\)

    (Házi feladat a zh utánra)

    Nem érvényes rá a specifikáció tétele, mert ez nem ugyan az az állapottér, mint az eredeti feladat

    Kibővíthetjük az állapotteret egy segédváltozóval, úgyhogy ez mégsem probléma

2. feladat

MAX

\(A=(x:\Z, y:\Z, z:\z)\)

\(B=(x':\Z, y': \Z)\)

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

\(R=(z=\max(x', y'))\)

  1. \(z:=\max(x,y)\)

    """Trivi""" - HF 2. \(z:=x+y-|x-y|\)

    "Bizonyítani nem olyan bonyolult"

    You guessed it: HF 3. (Ez itt elágazás táblázattal szemléltetve, mert még mindig nem találtam ki jobb módszert rá)

    \(x \geq y\) \(x \leq y\)
    \(z:=x\) \(z:=y\)

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

    Elágazás levezetési szabálya (ELSz): "Egy elágazás akkor vezet el minket, a \(Q\)-ból az \(R\)-be, ha külön-külön az elágazások ágai (feltéve az ághoz tartozó feltételt) elvezetnek az \(R\)-be"

    Be kell bizonyítani: - mindegyik feltétel értelmes - valamelyik feltétel biztos teljesül - minden ághoz 1-1 bizonyítás

    1. \(Q \Rightarrow (x,y,z) \in D_{x \geq y} \land (x,y,z) \in D_{x \leq y}\)

      \(\iff Q \Rightarrow (x \geq y \; \lor \; x < y) \; \land \; (x \leq \lor x > y)\) 2. \(Q \Rightarrow x \geq y \; \lor \; x \leq y\) 3. \(Q \land x \geq y \Rightarrow \text{lf}\,(z:=x,R)=(\text{igaz} \; \land \; R^{z \; \leftarrow \; x})=(x=\max(x', y'))\) 4. \(Q \land x \leq y \Rightarrow \text{lf}\,(z:=y,R)=(\text{igaz} \; \land \; R^{z \; \leftarrow \; y})=(y=\max(x', y'))\)

3. feladat

Számítsuk ki egy egész szám szignumát!

\(A = (x: \Z, s: \Z)\)

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

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

\(R=(s := \text{sgn}(x'))\)

\(x > 0\) \(x = 0\) \(x < 0\)
\(s := 1\) \(s := 0\) \(s := -1\)

You guessed it HF

4. feladat

Keressük meg két egész szám legnagyobb közös osztóját!

\(A = (a: \N, b: \N)\) // \(a\)-ba kerüljön az eredmény

\(B = (a': \N, b': \N)\)

\(Q = (a = a' \; \land \; b = b' \; \land \; (a' > 0 \land b' > 0) )\)

\(R = (a=\text{lnko}(a',b'))\)

while b != 0:
    a, b:=b, a%b

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

Ciklus Levezetési Szabálya (CLSz):

  • Feltételezve, hogy a ciklus megáll, meg kell mutatni, hogy jó helyen áll meg
    • ciklus invariáns állítása (olyan állítás, ami a ciklusban mindig igaz): \(P\)
    • \(Q \Rightarrow P\) - Az előfeltételek szerint \(P\) teljesül
    • \(P \land \pi \; \Rightarrow \; \text{lf}\,(S_0, P)\) - tehát, ha \(P\) teljesül, akkor a ciklusmag lefutása után is teljesül \(P\)
    • \(P \land \lnot \pi \Rightarrow R\) - ha a ciklusfeltétel már nem teljesül, de P igen akkor az az utófeltételt jelenti
    • \(P \Rightarrow \chi_{D_\pi}\) - I don't know honestly
    • \(P \land \pi \Rightarrow t > 0 \quad\) \(t\): hány lépés van hátra
    • \(P \land \pi \land t = t' \Rightarrow \text{lf}(S_0 \land t < t_0)\) - A hátralévő lépések száma csökken a ciklusmag lefutására

A két \(\text{lf}\)-es cuccot össze lehet vonni

\(P\): Az invariáns állítás jele

\(t\): hátralévő lépések száma

Ennek a gyakorlati használata:

\(P = (\text{lnko}(a,b) = \text{lnko}(a', b') \; \land \; (a > 0 \; \land \; b > 0))\)

\(t=b\)

Lépések:

  • \(Q \Rightarrow P\)
  • \(P \land \pi \Rightarrow R\)
  • \(P \Rightarrow \chi_{D_\pi}\)
    • Mivel a ciklusfeltétel bármilyen állapotra értelmezett, ezért ez triviálisan igaz
  • \(P \land \pi \Rightarrow t > 0\)
    • \(\pi = (b \neq 0)\), és \(b \in \N\), viszont \(t := b\), ezért beláttuk, hogy \(t>0\), hiszen \(b>0\)
  • \(P \land b \neq 0 \land b = t_0 \Rightarrow \text{lf}\,(a, b := b,a \bmod b, P \land b < t_0) = (b \neq 0 \land (P \land b < t_0)^{a,b \; \leftarrow \; b, a \bmod b})=(b \neq 0 \; \land \; \text{lnko}(b, a \bmod b)=\text{lnko}(a', b') \land (b > 0 \lor a \bmod b > 0) \land a \bmod b < t_0)\)

"Tekeredik a ciklus, megoldás akar lenni." (Doboz)

Előadás jegyzet: 𓅂𓃭𓅱𓄿𓂧𓄿𓋴 𓆓𓅂𓎼𓇌𓊃𓅂𓏏 :nod:

ZH-ban a \(Q_1\)-et, \(Q_2\)-t, \(P\)-t megkapjuk