5. gyakorlat
Emlékeztető
1. emlékeztető
\(v = \frac{s}{t}\)
\(A = (s:\R, t: \R, v: \R)\)
\(F = \{a \to c \; | \; s(a) \geq 0 \; \land \; t(a) \geq 0 \; \land \; v(c)=\frac{s(a)}{t(a)}\}\)
\((x, y, *) \to (*, *, \frac{x}{y})\) \(\quad \forall x, y \in \R, \quad x \geq 0, \; y \geq\)
Nézzük meg a következő felírást:
\(\{(x, y, *)\} \to (x, y)\to \{*, *, \frac{x}{y}\}\)
Így az input is része a felírásnak, hasonlóan a "matematikai" felíráshoz.
Fogalmazzuk meg logikai állításokkal is.
\(Q_{(x, y)}, R_{(x, y)}:A \to \mathbb{L}\)
\(Q_{(x, y)}(a)=(s(a)=x \; \land \; t(a)=y \; \land \; s(a) \geq 0 \; \land \; t(a)\geq 0) \quad \mathrel{\leadsto} \quad\) \(Q_{(x,y)} = (s = x \land t = y \land x > 0 \land y > 0)\)
\(R_{(x, y)}(a)=\left(v(a)=\frac{x}{y}\right) \quad \mathrel{\leadsto} \quad\)
\(R_{(x, y)}=\left(v = \frac{x}{y}\right)\)
\(Q\) - Basically előfeltétel
\(R\) - Basically utófeltétel
(Újabb kísérlet, hogy megszeressük és megértsük a specifikációkat.)
B: paraméter tér
\(B = \left(s': \R, \, t': \R \right)\)
\(b\in B: \; s'(b)=x \quad t'(b)=y\)
\(Q_b(a) = \left(s(a)=s'(b) \land t(a)=t'(b) \land s'(b) \geq 0 \land t'(b) \geq 0\right)\)
\(R_b(a) = \left(v(a) = \frac{s'(b)}{t'(b)} \right)\)
\(Q = \left(s = s' \; \land \; t = t' \; \land \; s' \geq 0 \; \land \; t' \geq 0 \right)\)
\(R = \left(v = \frac{s'}{t'}\right)\)
A specifikáció tétele
(Megjegyzés: Ez egy nagy tétel, de plusz-mínuszban csak részenként lesz kérdezve.)
1.) Mi a paraméterttér
\(F \subseteq A \times A \; \mathrel{\leadsto} \; F=F_2 \circ F_1\)
\(F_1 \subseteq A \times B\)
\(F_2 \subseteq B \times A\)
Ha egy feladatot fel tudunk bontani két ilyen részre, akkor a közbülső halmaz lesz a paraméter tér.
Fel lehet bontani a feladatot két lépésre.
2.) MI az adott paramétertérre vett elő- és utófeltétel
Hogyan állítjuk elő egy feladat adott paramétertérre vett elő- és utófeltételét
\(Q_b, R_b: A \to \mathbb{L} \quad \forall b \in B\)
\([Q_b]=F_1^{-1}(b)\)
\([R_b] = F_2(b)\)
\(A \stackrel{F}{\to} A\)
\([Q_b] \stackrel{F_1}{\to} b \stackrel{F_2}{\to} [R_b]\)
3.) Ennek volt neve?
\(\forall b \in B\)-re be tudjuk bizonyítani azt, hogy a \(Q_b \Rightarrow lf(S, R_b)\), akkor \(S\) megoldja \(F\) feladatot.
(Ez visszafele nem mindig igaz)
Feladatok
1. feladat
\(A = (x: \Z, y: \Z, z: \Z)\)
\(B = (x': \Z, y': \Z)\)
\(Q = (x = x' \land y = y') \quad \iff\)
Ez utóbbi kiírva teljesen:
\(Q_{\{x: e, \; y': f\}}(a) = (x(a) = e \; \land \; y(a) = f)\)
\(R = ((z = x' \lor z = y')\land z \geq x' \land z \geq y')\)
a. \(F(6,5,1) = \{(* ,* ,6)\}\)
b. \(F(2, -5, 0) = \{(*, *, 2)\}\)
c. \(F(0,0,0) = \{(*, *, 0)\}\)
d. \(F^{-1}(6,5,6) = \{(a, b, *) \; | \; \max\{a, b\}=6\}\)
- \(F^{-1}(6,5,6) = \{(6,5,*), \; (5,6,*), \; \ldots\}\)
Most már van elő- és utófeltételünk, pont úgy, mint a speciben
A \(Q\) az előfeltétel, az \(R\) az utófeltétel.
Alapból egy feladat/program csak állapotokon dolgozik. Viszont könnyebb lenne, ha tudnánk inkább bemenetekkel és kimenetekkel dolgozni. Ezt csinálja a Q és az R, ha jól értem. A Q "előkészíti" a bemeneti paramétereket az állapotból, az R pedig a paraméterekből csinál egy kimeneti állapotot.
e/1. \(Q_{(6,5)}: A \to \mathbb{L} \quad [Q_{(6,5)}]=\{(6, 5, *)\}\)
e/2. \(Q_{(6,5)}: A \to \mathbb{L} \quad [Q_{(e, f)}] = \{(e, f, *)\}\)
f/1. \(R_{(6,5)}: A \to \mathbb{L} \quad [R_{(6, 5)}] = \{(*, *, 6)\}\)
f/2. \(R_{(6,5)}: A \to \mathbb{L} \quad [R_{(e, f)}] = \{(*, *, \max(e, f))\}\)
g. \(F = \{a \to c \; | \; (z(c) = x \; \lor \; z(c)=y(a)) \land z(c) \geq x(a) \land z(c) \geq y(a) \; \}\)
Mi itt a feladat szövegesen?
Két szám maximumának kiválasztása.
2. feladat
\(F = \begin{cases}A = (x: \Z, y: \Z, z: \Z) \\ B = (x': \Z, y': \Z) \\ Q = (x=x' \land y = y' \land x' > 5) \\ R = (x' > y' \to z=x')\end{cases}\)
\(F(6,2,7) = \{(*, *, 6)\}\)
\(F(4,2,1) = \empty\) (nincs értelmezve, mert nem teljesül az előfeltétel)
\(F(6,9,4) = \{(*, *, *)\} \text{ vagy } A\)
Ha az első paraméter nagyobb, mint a második és az első nagyobb, mint 5, akkor az első paramétert adja vissza.
\([Q_{(6,2)}] = \{(6, 2, *)\}\)
\([Q_{(4,2)}] = \empty\)
\([Q_{(6,9)}] = \{(6, 9, *)\}\)
\([R_{(6,2)}] = \{(*, *, 6)\}\)
\([R_{(4,2)}] = \empty\)
\([R_{(6,9)}] = \{(*, *, *)\}\)
asdasdasd NYEEEE
3. feladat
Cseréljük ki két változó tartalmát
\(A = (x: \Z, y: \Z)\)
\(B = (x': \Z, y': \Z)\)
\(Q = (x=x' \land y=y')\)
\(R = (x=y' \land y=x')\)
Bizonyítsuk, hogy az alábbi program megoldja a feladatot:
Elég úgy vizsgálni, hogy
\(Q \Rightarrow lf(\text{x, y := y, x} \; , R) = ((x, y) \in D_{p(x, y := y, x)} \land R^{x, y \leftarrow y, x})\)
\(R^{x, y \leftarrow y, x} = (y=y' \land x=x')\)
Elméleti kérdések plusz-mínuszra
- Mi a paraméter tér?
- Mi az elő- és utófeltétele egy paraméter térnek?
- Specifikáció tétele?