BEVEZETÉS A PROGRAMOZÁSHOZ (Kivonat)

ELSŐ RÉSZ

A jegyzet elsősorban E.W. Dijkstra alapvető munkáira támaszkodik, az általa kimondott elveket igyekszik követni. Célja egy tudományos igényű programozói szemlélet kialakítása. 1

FELHASZNÁLT MATEMATIKAI FOGALMAK

1. Sorozatok

Jelölések N a természetes számok halmaza. N_{0} a természetes számokból és a nullából álló halmaz. Z az egész számok halmaza. L =^{def} {hamis, igaz}, a logikai értékek halmaza. Véges sorozat: α = (α_{1}, …, α_{n}). Végtelen sorozat: α = (α_{1}, . . . . . .). A^{∗} : A elemeiből képzett véges sorozatok halmaza. A^{∞} : A elemeiből képzett végtelen sorozatok halmaza.

A^{∗∗} =^{def} A^{∗} ∪ A^{∞}.

Definíciók 1.) kon (α, β) az α ∈ A^{∗} és a β ∈ A^{∗∗} sorozatok konkatenáltja, ha

kon (α, β) =^{def} (α_{1}, …, α_{n}, β_{1} . . . . . .).

2.) Az α ∈ A^{∗∗} redukáltjának nevezzük, és red (α)-val jelöljük azt a sorozatot, amit úgy kapunk, hogy az α minden azonos elemekből álló véges részsorozatát a részsorozat egyetlen elemével helyettesítjük.

3.) Legyen α^{1}, α^{2}, …, α^{n−1} ∈ A^{∗}; α^{n} ∈ A^{∗∗}.

χ_{n} (α^{1}, α^{2}, …, α^{n}) =^{def} red(kon(α^{1}, α^{2}, …, α^{n})).

χ_{∞} : végtelen sok véges sorozat konkatenáltjának redukáltja. 4.) Legyen α = (α_{1}, …, α_{n}) ∈ A^{∗}. τ : A^{∗} → A olyan függvény, amelyre τ(α) =^{def}

α_{n}.

2. Direktszorzat

Definíciók

1.) Legyen I = {i_{1}, i_{2}, …, i_{n}}.  ×_{i_{j}∈I} A_{i_{j}} =^{def} {(a_{i_{1}}, a_{i_{2}}, …, a_{i_{n}}) | a_{i_{j}} ∈ A_{i_{j}} }.

2.) Azt mondjuk, hogy a B halmaz az A halmaz altere, ha A = ×_{i_{j}∈I} A_{i_{j}} ; B =

×_{j_{k}∈J} A_{j_{k}} ,

ahol I = {i_{1}, i_{2}, …, i_{n}} , J = {j_{1}, j_{2}, …, j_{m}} , m ≤n és J ⊆ I ⊆ N. 3.) pr_{B} (a) az a ∈ A-nak a B-re vett projekciója, ha B altere A-nak és

pr_{B} (a) =^{def} (a_{j_{1}}, a_{j_{2}}, …, a_{j_{m}}) (a 2. pont jelöléseivel ).

3. Relációk

Definíciók 1.) Az R ⊆ A × B-t bináris relációnak nevezzük.

2.) Legyen R ⊆ A × B. R(a) =^{def} { b | (a, b) ∈ R }.

3.) Legyen R ⊆ A × B. Az R reláció értelmezési tartománya:

D_{R} =^{def} { a ∈ A | ∃b ∈ B : (a, b) ∈ R}.

4.) Legyen R ⊆ A × B. Az R reláció értékkészlete: R_{R} =^{def} ∪_{a∈A} R(a). 5.) Az R ⊆ A × B reláció determinisztikus reláció (vagy parciális függvény), ha

∀ a ∈ A : | R(a) | ≤ 1. 6.) Az R ⊆ A × B reláció függvény, ha ∀ a ∈ A : | R(a) | = 1. 7.) R^{(−1)} =^{def} { (b, a) | (a, b) ∈ R } az R ⊆ A × B reláció inverze. 8.) R̃ =^{def} { (a, b) | (a, b) ∉ R ∧ (a, b) ∈ A × B} az R ⊆ A × B reláció komplemense.

9.) R_{2} ∘ R_{1} =^{def} { (a, c) | ∃ b ∈ B : (a, b) ∈ R_{1} ∧ (b, c) ∈ R_{2} } az R_{1} ⊆ A × B és

az R_{2} ⊆ B × C relációk kompozicíója. 10.) R^{n} =^{def} R ∘ R^{n−1} (n ∈ N) az R ⊆ A × A reláció n. hatványa.

11.) Legyen R ⊆ A × A. R^{0} =^{def} { (a, a) | a ∈ A }.

12.) R_{2} ⊙ R_{1} =^{def} { (a, c) | R_{1} (a) ⊆ D_{R_{2}} ∧ ∃ b ∈ B : (a, b) ∈ R_{1} ∧ (b, c) ∈ R_{2} }

az R_{1} ⊆ A × B és az R_{2} ⊆ B × C relációk szigorú kompozíciója.

13.) R^{(−1)} (H) =^{def} { a ∈ A | ∃ h ∈ H : (a, h) ∈ R } a H ⊆ B halmaznak az

R ⊆ A × B relációra vonatkozó inverz képe. 14.) R^{−1} (H) =^{def} { a ∈ A | R (a) ⊆ H ∧ R (a) ≠ ∅ } a H ⊆ B halmaznak az

R ⊆ A × B relációra vonatkozó ősképe. 15.) L_{R}(a_{0}, …, a_{q}) az R ⊆ A × A reláció q hosszúságú pontlánca, ha ∀i ∈ [1, q] : a_{i} ∈

R(a_{i−1}). a_{q} a sorozat végpontja, ha a_{q} ∉ D_{R}. 16.) L_{R}(a_{0}, . . . . . .) az R ⊆ A × A reláció végtelen pontlánca, ha ∀i ∈ N : a_{i} ∈ R(a_{i−1}).

17.) \overline{R} az R ⊆ A × A reláció lezártja, ha D \overline{R} =^{def} \{a ∈ A| ∄L_{R}(a_{0}, . . . . . .) : a_{0} = a\},

\overline{R}(a) =^{def} \{a′ ∈ A|∃L_{R}(a_{0}, …, a_{q}) : a = a_{0} ∧ a′ = a_{q} ∧ a_{q} ∉ D_{R}\}.

18.) \overline{\overline{R}} az R ⊆ A × A reláció korlátos lezártja, ha

D\overline{\overline{R}} =^{def} \{a ∈ A| ∄L_{R}(a_{0}, …) : a_{0} = a ∧

∃n ∈ N : ∀L_{R}(a_{0}, …, a_{q}) : (a = a_{0}) → q≤n},

\overline{\overline{R}}(a) =^{def} \{a′ ∈ A|∃L_{R}(a_{0}, …, a_{q}) : a = a_{0} ∧ a′ = a_{q} : a_{q} ∉ D_{R}\}.

19.) Az f ⊆ A × L relációt logikai függvénynek (vagy állításnak) nevezzük. 20.) [f] =^{def} {a ∈ A|f(a) = {igaz}} az f logikai függvény igazsághalmaza. 21.) [R] =^{def} R^{−1}({igaz}) az R ⊆ A × L reláció igazsághalmaza. 22.) Legyen R ⊆ A × B , H ⊆ A.

R|_{H} =^{def} (R ∩ (H × B)) reláció az R megszorítása a H halmazra. 23.) Legyen R ⊆ A × A és π egy állítás A-n.

R|_{π} =^{def} (R ∩ ([π] × A)) ∪ {(a, a) | [π] \ D_{R}} (feltételre vonatkozó reláció). Megj.: R|_{π} ≠ R|_{[π]}.

24.) \overline{R|_{π}} az R reláció π feltételre vonatkozó lezártja, \overline{\overline{R|_{π}}} az R reláció π feltételre

vonatkozó korlátos lezártja. Tételek 1.) [f] = f^{−1}({i}). 2.) ∀n ∈ N : |A| > n ⇒ ∃R : R ⊆ A × A : \overline{R} ≠ \overline{\overline{R}}.

ALAPVETŐ DEFINÍCIÓK ÉS TÉTELEK

Definíciók 1.) Legyen I ⊂ N , ∀i_{j} ∈ I : A_{i_{j}} megszámlálható halmaz.

Az A =^{def} ×_{i_{j}∈I} A_{i_{j}} halmazt állapottérnek, az A_{i_{j}} halmazokat típusértékhalmazoknak nevezzük. 2

2.) Az állapottér elemeit, az a = (a_{i_{1}}, …, a_{i_{n}}) ∈ A pontokat állapotoknak nevezzük. 3.) Az a_{i_{j}} : A → A_{i_{j}} projekciókat változóknak nevezzük. 3 4.) Az F ⊆ A × A relációt feladatnak nevezzük. 4 5.) Az S ⊆ A × A^{∗∗} relációt programnak nevezzük, ha 5

a.) ∀a ∈ A : ∀α ∈ S(a) : α_{1} = a, b.) D_{S} = A, c.) ∀α ∈ R_{S} : α = red(α).

6.) A p(S) ⊆ A × A reláció az S ⊆ A × A^{∗∗} program programfüggvénye, ha 6 a.) D_{p(S)} = {a ∈ A|S(a) ⊆ A^{∗}}, b.)p(S)(a) = {b ∈ A|∃α ∈ S(a) : τ(α) = b}.

7.) Az S ⊆ A × A^{∗∗} program megoldja az F ⊆ A × A feladatot, ha 7 a.) D_{F} ⊆ D_{p(S)}, b.) ∀a ∈ D_{F} : p(S)(a) ⊆ F (a).

8.) Legyenek S_{1}, S_{2} ⊆ A × A^{∗∗} programok. S_{1} ekvivalens S_{2}-vel, ha p(S_{1}) = p(S_{2}). 9.) Legyen B altere az A állapottérnek. Az F′ ⊆ A × A feladat az F ⊆ B × B feladat

kiterjesztése az A térre, ha F′ = {(a_{1}, a_{2}) | (pr_{B}(a_{1}), pr_{B}(a_{2})) ∈ F }. 10.) Legyen B altere A-nak, J ⊆ I és A = ×_{i∈I} A_{i} , B = ×_{j∈J} A_{j}. B′ a B altér kiegészítő

altere az A-ra, ha B′ = ×_{k∈(I\J)}A_{k} . 11.) Legyen B altere A-nak, B′ a B altér kiegészítő altere az A-ra. S′ az S ⊆ B × B^{∗∗}

program kiterjesztése A-ra, ha

S′ = {(a, α) | (pr_{B}(a), pr_{B}(α)) ∈ S ∧
α ∈ A^{∗} → ∀i ∈ [1..|α|] : pr_{B′}(α)_{i} = pr_{B′}(a) ∧
α ∈ A^{∞} → ∀i ∈ N : pr_{B′}(α)_{i} = pr_{B′}(a)}

12.) Legyen B közös altere A_{1}-nek és A_{2}-nek, S_{1} program A_{1}-en, S_{2} program A_{2}-

n. S_{1} ekvivalens S_{2}-vel a B altéren, ha pr_{B}(p(S_{1})) = pr_{B}(p(S_{2})). 13.) Legyen B altere A-nak, G ⊆ A × A feladat. A G feladat vetítéstartó a B altér

felett,ha ∀ a_{1}, a_{2} ∈ D_{G} : (pr_{B}(a_{1}) = pr_{B}(a_{2}) ⇒ pr_{B}(G(a_{1})) = pr_{B}(G(a_{2}))).

14.) Legyen B′ altere A-nak, G ⊆ A × A feladat. A G feladat bővített identitás a B′ altér felett, ha ∀ (a_{1}, a_{3}) ∈ G : ∃(a_{1}, a_{4}) ∈ G : (pr_{B′}(a_{4}) = pr_{B′}(a_{1}) ∧ pr_{B}(a_{3}) = pr_{B}(a_{4})).

Tételek Legyen B altere A-nak, B′ a B kiegészítő altere A-ra, S program B-n, F ⊆ B × B feladat, S′ illetve F′ S-nek, illetve F -nek kiterjesztése A-ra, S_{1} program A-n, G ⊆ A × A feladat, G_{1} = pr_{B×B}(G), és legyen S_{1} és S ekvivalens B-n. 8 1.) Ha S′ megoldja G-t ⇒ S megoldja G_{1}-t. 2.) Ha S_{1} megoldja F′-t ⇒ S megoldja F -t. 3.) Ha S′ megoldja F′-t ⇔ S megoldja F -t. 4.) Ha S megoldja G_{1}-t, G vetítéstartó B felett, és bővített identitás B′ felett ⇒

S′ megoldja G-t.

TÍPUS

Definíciók 1.) A T_{S} = (T, I_{S}, F) rendszert típusspecifikációnak nevezzük.

T : alaphalmaz ; I_{S} : specifikációs invariáns ; T_{S} ( = [I_{S}]) : típusértékhalmaz ; F = {F_{1}, F_{2}, …, F_{n}} : ∀k ∈ [1, …, n] : F_{k} ⊆ A_{k} × A_{k} ;

A_{k} = ×_{l∈L_{k}} A_{k}_{l} ∧ ∃l ∈ L_{k} : A_{k}_{l} = T_{S}.

2.) T = (ϱ, S, I) rendszert típusnak nevezzük.

E : elemi típusértékek halmaza ; ϱ : reprezentációs függvény ; ϱ ⊆ E^{∗} × T′ ; S : programok halmaza ; S = {S_{1}, S_{2}, …, S_{m}} : ∀i ∈ [1, …, m] : S_{i} ⊆ B_{i} × B_{i};

B_{i} = ×_{j∈J_{i}} B_{i}_{j} ∧ ∃j ∈ J_{i} : B_{i}_{j} = E^{∗}.

I : típusinvariáns, állítás az E^{∗} halmazon. 3.) A T = (ϱ, S, I) típus megfelel a T_{S} = (T, I_{S}, F) típusspecifikációnak, ha

a.) T ⊆ T′ ∧ ϱ([I]) = T_{S},

b.) ∀F_{k} ∈ F : (∃S_{i} ∈ S : S_{i} megoldja^{∗} F_{k}-t).

4.) S_{i} ⊆ B_{i} × B_{i} megoldja^{∗} F_{k} ⊆ A_{k} × A_{k}-t, ha

a.) B_{i} = ×_{j∈J_{i}} B_{i}_{j} ∧ A_{k} = ×_{l∈L_{k}} A_{k}_{l} ∧ L_{k} ⊆ J_{i} ⊂ N ∧

(∀l ∈ L_{k} : B_{i}_{l} = A_{k}_{l} ∨ (B_{i}_{l} = E^{∗} ∧ A_{k}_{l} = T_{S})), b.) ∀a ∈ D_{F_{k}} : γ_{k} ⊙ p(S) ⊙ γ_{k}^{(−1)} (a) ≠ ∅, c.) ∀a ∈ D_{F_{k}} : γ_{k} ⊙ p(S) ⊙ γ_{k}^{(−1)} (a) ⊆ F (a),

ahol γ_{k} = (γ_{k}_{l_{1}} … γ_{k}_{l_{|L|}}),

γ_{k} ⊆ ( ×_{l∈L_{k}} B_{i}_{l}) × ( ×_{l∈L_{k}} A_{k}_{l}, ) ∧ ∀b_{i} ∈ ( ×_{l∈L_{k}} B_{i}_{l}) : γ_{k}(b_{i}) = ×_{l∈L_{k}} γ_{k}_{l}(b_{i})

γ_{k}_{l}(b_{i}) =^{def} \{ \begin{matrix}ϱ|_{[I]}(b_{i}_{l}) & ,ha A_{k}_{l} = T_{S} \\ \{b_{i}_{l}\} & ,ha A_{k}_{l} = B_{i}_{l} \end{matrix}

SPECIFIKÁCIÓ

Definíciók 1.) Az R utófeltétel S programra vonatkozó leggyengébb előfeltételének nevezzük azt

az lf(S, R) állítást, amelyre 9

[lf(S, R)] = {a ∈ D_{p(S)} | p(S)(a) ⊆ [R]}. 2.) F^{−1} : 2^{A} → 2^{A}, F^{−1}(H) = {a ∈ A | F (a) = H}. 3.) B az F ⊆ A × A feladat paramétertere, ha

∃ F_{1}, F_{2} : F_{1} ⊆ A × B , F_{2} ⊆ B × A és F = F_{2} ∘ F_{1}. Tételek 1.)

a.) [lf(S, R)] = p(S)^{−1}([R]).
b.) lf(S, R)(a) = a ∈ [R ∘ p(S)].

2.) A leggyengébb előfeltétel tulajdonságai 10 a.) lf(S, hamis) = hamis (A csoda kizárásának elve).

b.) lf(S, P ∧ Q) = lf(S, P) ∧ lf(S, Q).
c.) lf(S, P ∨ Q) ⇐ lf(S, P) ∨ lf(S, Q).
d.) Q → R ⇒ lf(S, Q) → lf(S, R) (Monotonitás).

3.) A tulajdonságok duálisai a.) D_{p(S)} = ∅ ⇔ lf(S, R) = hamis.

b.) S_{1} ⊆ S_{2} ⇒ [lf(S_{2}, R)] ⊆ [lf(S_{1}, R)].

c.) Ha S_{1} ∩ S_{2} program, akkor [lf(S_{1}, R)] ∩ lf(S_{2}, R)] ⊆ [lf(S_{1} ∩ S_{2}, R)].

d.) [lf(S_{1} ∪ S_{2}, R)] ⊆ [lf(S_{1}, R)] ∪ [lf(S_{2}, R)].

4.) A leggyengébb előfeltétel és a megoldás kapcsolata 11 a.) S megoldja F -t ⇔ ∀ a ∈ D_{F} : a ∈ [lf(S, P (F (a)))].

b.) S megoldja F -t ⇔ ∀ H ⊆ D_{F^{−1}} : F^{−1}(H) ⊆ [lf(S, P (H))].

5.) (Specifikáció tétele) 12 Legyen F ⊆ A × A, B az F egy paramétertere. Legyen b ∈ B és [Q_{b}] = F_{1}^{(−1)}(b) és [R_{b}] = F_{2}(b). Ha ∀ b ∈ B-re : Q_{b} ⇒ lf(S, R_{b}), akkor S megoldja F -et.

6.) A specifikáció tétele nem megfordítható, azaz 13 ∃F ⊆ A × A feladat, S program, ∃F_{1}, F_{2}, hogy F = F_{2} ∘ F_{1} és Q_{b}, R_{b} adottak a

specifikáció tétele szerint, és S megoldja F -t, és ¬∀b ∈ B : Q_{b} ⇒ lf(S, R_{b}).

ELEMI PROGRAMOK

Definíciók 1.) Eleminek nevezünk egy A állapottéren egy S programot, ha

∀a ∈ A : S(a) ⊆ {(a), (aaa …), (a, b) | b ∈ A ∧ b ≠ a}. 2.) Üresnek nevezzük, és SKIP-pel jelöljük azt a programot, amire

∀a ∈ A : SKIP (a) = {(a)}. 3.) Törlődésnek nevezzük, és ABORT-tal jelöljük azt a programot, amire

∀a ∈ A : ABORT (a) = {(aaa …)} . 4.) Legyen A = A_{1} × … × A_{n}, F = (F_{1}, …, F_{n}), ahol F_{i} ⊆ A × A_{i}. Az S program

általános értékadás, ha 14

S = {(a, red(a, b)) | a, b ∈ A ∧ a ∈ ∩_{i∈[1,n]}D_{F_{i}} ∧ b ∈ F (a)} ∪

{(a, (aaa …)) | a ∈ A ∧ a ∉ ∩_{i∈[1,n]}D_{F_{i}}}

Megjegyzés:

D_{F} = ∩_{i∈[1,n]}D_{F_{i}}

F (a) = F_{1}(a) × F_{2}(a) × … × F_{n}(a)

a) Ha D_{F} = A, akkor az S programot értékkiválasztásnak nevezzük és a :∈ F (a) -val jelöljük.

b) Ha az F reláció függvény akkor az S programot értékadásnak nevezzük és a := F (a)-val jelöljük.

c) Ha D_{F} ⊂ A, akkor parciális értékkiválasztásról beszélünk.

d) Ha D_{F} ⊂ A és F determinisztikus, akkor S parciális értékadás .

e) Ha ∀i, j ∈ [1..n] : i ≠ j ∧ F_{i}(a_{1}, .., a_{i}, .., a_{n}) ≠ a_{i} ⇒ F_{j}(a_{1}, .., a_{j}, .., a_{n}) = a_{j}, akkor S egyszerű (általános) értékadás ( egyébként szimultán értékadás ).

Tételek 1.) lf(SKIP, R) = R. 2.) lf(ABORT, R) = hamis. 3.) Ha S az F reláció által meghatározott értékadás, akkor lf(S, R) = F^{−1}([R]).

PROGRAMKONSTRUKCIÓK

Definíciók 1.) Legyenek S_{1},S_{2} ⊆ A × A^{∗∗} programok. Az S ⊆ A × A^{∗∗} relációt az S_{1} és S_{2}

szekvenciájának nevezzük, és (S_{1}; S_{2})-vel jelöljük, ha 15

\begin{aligned}∀a ∈ A : S(a) = & \{α | α ∈ S_{1}(a) ∩ A^{∞}\}∪ \\ & ∪ \{χ_{2}(α, β) | α ∈ S_{1}(a) ∩ A^{∗} ∧ β ∈ S_{2}(τ(α))\}. \end{aligned}

2.) Legyenek π_{1}, …, π_{n} feltételek, S_{1}, …, S_{n} programok A-n. Az IF ⊆ A × A^{∗∗} relációt az S_{i}-kből képzett elágazásnak nevezzük és (π_{1} : S_{1}, …, π_{n} : S_{n})-nel jelöljük, ha 16

∀a ∈ A : IF (a) = ({∪ \atop i ∈ [1, n]}w_{i}(a)) ∪ w(a),

ahol

w_{i}(a) = \{ \begin{matrix}S_{i}(a) , & ha a ∈ [π_{i}] \\ ∅ , & különben \end{matrix}
w(a) = \{ \begin{matrix}\{(a, a, …)\} , & ha a ∉ ∪_{i∈[1,n]}[π_{i}] \\ ∅ , & különben \end{matrix}

3.) Legyen π feltétel és S_{0} program A-n. A DO ⊆ A × A^{∗∗} relációt az S_{0}-ból és π-

ből képezett ciklusnak nevezzük, és (π, S_{0})-lal jelöljük, ha 17 ∀a ∈ [¬π] : DO(a) = {(a)},

∀a ∈ [π] : DO(a) = {α | α ∈ A^{∗∗} ∧ ∃α_{1}, …, α_{n} ∈ A^{∗∗} :

(α = χ_{n}(α_{1}, …, α_{n}) ∧ α_{1} ∈ S_{0}(a) ∧ ∀i ∈ [1, n − 1] : α_{i} ∈ A^{∗} ∧ α_{i+1} ∈

S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π]) ∧ ((α_{n} ∈ A^{∗} ∧ τ(α_{n}) ∉ [π]) ∨ (α_{n} ∈ A^{∞}))} ∪

{α | α ∈ A^{∞} ∧ ∃α_{1}, …, α_{k}, .. ∈ A^{∗} : (α = χ_{∞}(α_{1}, …, α_{k}, ..) ∧ α_{1} ∈ S_{0}(a) ∧

∀i ∈ N : α_{i} ∈ A^{∗} ∧ α_{i+1} ∈ S_{0}(τ(α_{i})) ∧ τ(α_{i}) ∈ [π])}.

Tételek 1.) A szekvencia, az elágazás és a ciklus program. 18 2.) Legyen S = (S_{1}; S_{2}) szekvencia, IF = (π_{1} : S_{1}, …, π_{n} : S_{n}) elágazás és DO =

(π, S_{0}) ciklus. Ekkor 19 a.) p((S_{1}; S_{2})) = p(S_{2}) ⊙ p(S_{1}).

b.) D_{p(IF)} = {a ∈ A | a ∈ ∪_{i∈[1,n]}[π_{i}] ∧ ∀i ∈ [1, n] : a ∈ [π_{i}] ⇒ a ∈ D_{p(S_{i})}}

∀a ∈ D_{p(IF)} : p(IF)(a) = ∪_{i∈[1,n]}pw_{i}(a) , ahol

pw_{i}(a) = \{ \begin{matrix}p(S_{i})(a), & ha a ∈ [π_{i}] \\ ∅, & különben \end{matrix}

c.) p(DO(π, S_{0})) = \overline{p(S_{0})|_{π}}.

3.) A szekvencia, az elágazás és a ciklus leggyengébb előfeltétele rendelkezik a következő tulajdonságokkal :

a) Legyen S = (S_{1}; S_{2}), és Q, R olyan állítások A-n, amelyekre Q ⇒ lf(S, R). Ekkor létezik olyan Q′ állítás, amire Q ⇒ lf(S_{1}, Q′) ∧ Q′ ⇒ lf(S_{2}, R).

b) Legyen IF = (π_{1} : S_{1}, …, π_{n} : S_{n}), és Q, R olyan állítások A-n, amelyekre

Q ∧ ( ∨_{i∈[1,n]}π_{i}) ⇒ lf(IF, R). Ekkor ∀i ∈ [1, n] : Q ∧ π_{i} ⇒ lf(S_{i}, R).

c) Legyen DO = (π, S_{0}), és Q, R olyan állítások A-n, amelyekre Q ⇒ lf(DO, R), és tegyük fel, hogy ∀a ∈ D_{p(S_{0})} ∩ [π] : ∃k ∈ N : p(S_{0})^{k}(a) = ∅. Ekkor létezik P állítás és t : A → Z függvény, amelyekre

1. Q ⇒ P,

2. P ∧ ¬π ⇒ R,

3. P ∧ π ⇒ t > 0,

4. P ∧ π ∧ t = t′ ⇒ lf(S_{0}, P ∧ (t≤t′ − 1)).

LEVEZETÉSI SZABÁLYOK

Tételek 1.) A szekvencia levezetési szabálya. 20

Legyen S = (S_{1}; S_{2}), és adott Q, R és Q′ állítás A-n. Ha

1. Q ⇒ lf(S_{1}, Q′) és

2. Q′ ⇒ lf(S_{2}, R), akkor Q ⇒ lf(S, R). 2.) Az elágazás levezetési szabálya. 21

Legyen IF = (π_{1} : S_{1}, …, π_{n} : S_{n}), és adott Q, R állítás A-n. Ha

∀i ∈ [1, n] : Q ∧ π_{i} ⇒ lf(S, R), akkor Q ∧ ( ∨_{i∈[1,n]}π_{i}) ⇒ lf(IF, R).

3.) A ciklus levezetési szabálya. 22 Legyen adott P, Q, R állítás A-n, t : A → Z függvény és legyen DO = (π, S_{0}). Ha

1. Q ⇒ P,

2. P ∧ ¬π ⇒ R,

3. P ∧ π ⇒ t > 0,

4. P ∧ π ∧ t = t′ ⇒ lf(S_{0}, P ∧ (t≤t′ − 1)) akkor Q ⇒ lf(DO, R). A t függvényt variáns függvénynek, a P állítást invariáns tulajdonságnak nevezzük.

TÍPUSKONSTRUKCIÓK

Legyenek a T_{0}, T_{1}, …, T_{n}, E_{1}, …, E_{n} nem üres, véges vagy megszámlálható halmazok, E = ∪_{i=1,n}E_{i}, ϱ_{i} ⊂ E^{∗} × T_{i} reprezentációs függvények, T_{i} = (ϱ_{i}, I_{i}, S_{i}) (i = 0, …, n) típusok.

Definíciók 1.) Direktszorzat

ϱ = ψ_{D} ∘ φ_{D}, ahol ψ_{D} ⊂ B × T, B = T_{1} × … × T_{n}, φ_{D} = {(ε, b) ∈ E^{∗} × B | ∃ε_{1}, …, ε_{n} ∈ E^{∗} : ∀i ∈ [1, n] : (ε_{i}, b_{i}) ∈ ϱ_{i} ∧ ε = kon(ε_{1}, …, ε_{n})}. Jelölés: T = (T_{1}, …, T_{n}). Ha ψ_{D} kölcsönösen egyértelmű, akkor T rekord típus. 23

2.) Unió ϱ = ψ_{U} ∘ φ_{U}, ahol ψ_{U} ⊂ B × T, B = T_{1} ∪ … ∪ T_{n}, φ_{U} = {(ε, b) ∈ E^{∗} × B | ∃i ∈ [1, n] : (ε, b) ∈ ϱ_{i}} . Jelölés: T = (T_{1}; …; T_{n}). Ha ψ_{U} kölcsönösen egyértelmű, akkor T egyesítés.

3.) Iterált ϱ = ψ_{I} ∘ φ_{I}, ahol ψ_{I} ⊂ T_{0}^{∗} × T, φ_{I} = {(ε, β) ∈ E^{∗} × T_{0}^{∗} | ∃α ∈ (E^{∗})^{∗} :| α |=| β | ∧∀i ∈ [1, | α |] : (α_{i}, β_{i}) ∈ ϱ_{0} ∧ ε = kon(α_{1}, …, α_{|α|}}. Jelölés: T = it(T_{0}). Ha ψ_{I} kölcsönösen egyértelmű, akkor T sorozat típus.

Jelölés: T = seq(T_{0}). Ha D_{ψ_{I}} = T_{0}^{∗} és (α, t), (β, t) ∈ ψ_{I} ≡ α ∈ perm(β), akkor T kombináció típus.

Jelölés: T = com(T_{0}). Ha D_{ψ_{I}} = T_{0}^{∗} és (α, t), (β, t) ∈ ψ_{I} ≡ ∪{α_{i}} = ∪{β_{i}}, akkor T halmaz típus.

Jelölés: T = set(T_{0}).

1. Specifikációs függvények

Definíciók

1. Szelekciós függvények

a) Legyen T = (T_{1}, ..., T_{n}) rekord típus. s_{1}, ..., s_{n} a rekord szelektorfüggvényei, ha s_{i} : T → T_{i} , és ∀t ∈ T -re λ_{D} ∘ (s_{1}, ..., s_{n})(t) = t. A szelektorokkal ellátott rekord jelölése: T = (s_{1} : T_{1}, ..., s_{n} : T_{n}).

b) Legyen T = (T_{1}; ...; T_{n}) egyesítés típus. s_{1}, ..., s_{n} az egyesítés szelektorfüggvényei, ha s_{i} : T → L és ∀t ∈ T -re s_{i}(t) ≡ t ∈ λ_{U}(T_{i}). A szelektorokkal ellátott egyesítés jelölése: T = (s_{1} : T_{1}; ...; s_{n} : T_{n}).

c) Legyen T = it(T_{0}) iterált típus, t_{0} ∈ T_{0}, t ∈ T. A t_{0} ∈ t relációt úgy értelmezzük, hogy t_{0} ∈ t ≡ ∃(α, t) ∈ λ_{I}, i ∈ N : α_{i} = t_{0}.

d) T = seq(T_{0}). kiv : T × N → T_{0} a sorozatra értelmezett szelekciós függvény, ha

kiv(t, i) =^{def} \{ \begin{matrix}α & ,ha 1 ≤ i ≤ dom(t) ∧ (α, t) ∈ λ \\ nem definiált & , egyébként. \end{matrix}

A sorozatra vonatkozó kiválasztásfüggvényt indexeléssel jelöljük: t_{j}.

2. A T = it(T_{0}) iterált típushoz definiáljuk a dom : T → N_{0} függvényt.

Legyen (α, t) ∈ λ_{I}, ekkor

dom(t) =^{def} \{ \begin{matrix}| α | & ha T sorozat, vagy kombináció \\ | ∪_{i=1,|α|}\{α_{i}\} | & ha T halmaz \\ definiálatlan & egyébként \end{matrix}

3. Sorozatra értelmezett függvények Legyen T = seq(T_{0}) ∧ (α, t) ∈ λ_{I}.

a) low : T → T_{0}. low(t) =^{def} α_{1}, ha dom(t) ≠ 0.

b) hiw : T → T_{0}. hiw(t) =^{def} α_{|α|}, ha dom(t) ≠ 0.

b) ext : T × T → T. Ha (α_{1}, t_{1}), (α_{2}, t_{2}) ∈ λ_{I}, akkor

ext(t_{1}, t_{2}) =^{def} λ_{I}(kon(α_{1}, α_{2})).

ext(t_{1}, ..., t_{k}) =^{def} ext(ext(t_{1}, ..., t_{k−1}), t_{k}).

c) rem : T × T → T.

rem(t_{1}, t_{2}) =^{def} \{ \begin{matrix}ext(t′, t′′) & , ha ∃t′, t′′ : t_{1} = ext(t′, t_{2}, t′′) \\ t_{1} & , egyébként \end{matrix}

d) loext : T × T_{0} → T. loext(t, t_{0}) =^{def} ext(λ_{I}(t_{0}), t).

e) hiext : T × T_{0} → T. hiext(t, t_{0}) =^{def} ext(t, λ_{I}(t_{0})).

f) hirem : T → T. hiext(hirem(t), hiw(t)) = t, ha dom(t) ≠ 0.

g) lorem : T → T. loext(lorem(t), low(t)) = t, ha dom(t) ≠ 0.

4. A kombinációra értelmezett függvények Legyen T = com(T_{0}).

a) ism : T × T_{0} → N_{0}. Ha α ∈ λ_{I}^{−1}(t) és t_{0} ∈ T_{0}, akkor

ism(t, t_{0}) =^{def} ∑_{i=1}^{|α|} χ(α_{i} = t_{0})

ahol χ : L → {0, 1} ún. karakterisztikus függvény: χ(↑) = 1, χ(↓) = 0.

5. A függvény típus Legyen H tetszőleges rendezett halmaz, amelyen értelmezve vannak a pred, succ és ord függvények, ord(succ(x)) − ord(x) = 1. Legyen T = seq(T_{0}). Az F = (H, T) rekord típust függvény típusnak nevezzük. Jele: F = fun(H, T_{0}).

6. Függvény típuson értelmezett függvények Legyen F = fun(H, T_{0}) függvény típus, továbbá ((m, t), f) ∈ λ_{D} tetszőleges rögzített elem. Ekkor

a) dom : F → N_{0}, dom(f) =^{def} dom(t).

b) lob : F → H, lob(f) =^{def} m.

c) hib : F → H, ord(hib(f)) − ord(lob(f)) = dom(f) − 1.

d) kiv : F × H → T_{0}.

e) kiv(f, i) =^{def} t_{ord(i)−ord(lob(f))+1}, ha lob(f) ≤ i ≤ hib(f).

f) low : F → T_{0}, low(f) =^{def} t_{1}, ha dom(f) ≠ 0.

g) hiw : F → T_{0}, hiw(f) =^{def} t_{dom(t)}, ha dom(f) ≠ 0.

h) hiext : F × T_{0} → F hiext(f, t_{0}) =^{def} λ_{D}(m, ext(t, t_{0})).

i) loext : F × T_{0} → F loext(f, t_{0}) =^{def} λ_{D}(m − 1, ext(t_{0}, t)).

k) hirem : F → F, hirem(f) =^{def} λ_{D}(m, hirem(t)), ha dom(f) ≠ 0.

l) hirem : F → F, lorem(f) =^{def} λ_{D}(m + 1, lorem(t)), ha dom(f) ≠ 0.

2. Nevezetes típusok és típusosztályok

A továbbiakban R jelöljön tetszőleges utófeltételt.

1. Rekord típusok műveletei: t_{i} := t.s_{i} , t.s_{i} := t_{i}.

Legyen A = T × T_{1} × ... × T_{n} és t : T, t_{i} : T_{i}(i ∈ [1..n]) és T = (s_{1} : T_{1}, ..., s_{n} : T_{n}).

a) t_{i} := t.s_{i}, ahol i ∈ [1, ..., n]). lf(t_{i} := t.s_{i}, R) = R^{t_{i}←t_{i}.s}.

b) t.s_{i} := t_{i}, ahol i ∈ [1, ..., n]). lf(t.s_{i} := t_{i}, R) = R^{t←t′}, ahol t′ ∈ T és s_{j}(t′) = t.s_{j}, ha i ≠ j, s_{i}(t′) = t_{i}.

2. Egyesítés típusok műveletei: t.s_{i} logikai függvények.

Legyen T = (s_{1} : T_{1}; ...; s_{n} : T_{n}).

a) i ∈ [1, ..., n]). t.s_{i} ≡ t ∈ λ_{U}(T_{i}).

3. Halmaz típusok műveletei: t_{0} ∈ t, t_{0} : mem(t), t := t ˜−{t_{0}}, t := t˜∪{t_{0}}. Legyen T = set(T_{0}).

a) t_{0} : mem(t). lf(t_{0} : mem(t), R) = dom(t) ≠ ∅ ∧ foralle ∈ t : R^{t_{0}←e}.

b) t := t ˜−{t_{0}}. lf(t := t ˜−t_{0}, R) = t_{0} ∈ t ∧ R^{t←t−{t_{0}}}.

c) t := t˜∪{t_{0}} lf(t := t˜∪t_{0}, R) = t_{0} ∈ t ∧ R^{t←t∪{t_{0}}}.

d) t_{0} ∈ t logikai függvény.

4. Kombináció típusok műveletei: t_{0} ∈ t, t_{0} : mem(t), t := t ˜−t_{0}, t := t˜∪t_{0}, m : ism(t, t_{0}).

Legyen T = com(T_{0}). a)-d) t_{0} ∈ t, t_{0} : mem(t), t := t ˜−t_{0}, t := t˜∪t_{0}, m : ism(t, t_{0}).

(A műveletek specifikációja megegyezik a halmaz típus megfelelő műveleteinek specifikációjával.)

e) lf(m : ism(t, t_{0}), R) = R^{m←ism(t_{0},t)}.

5. Sorozat típusok műveletei: dom, low, hiw, hiext, loext, lorem, hirem, t_{0} := t_{i}, t_{i} := t_{0}, lopop, hipop. Legyen T = seq(T_{0}), A = T × T_{0}, t_{0} : T_{0}, t : T, m : N_{0}.

a) lf(m := t.dom, R) = R^{m←dom(t)}.

b) lf(t_{0} := t.low, R) = dom(t) ≠ 0 ∧ R^{t_{0}←low(t)}.

c) lf(t_{0} := t.hiw, R) = dom(t) ≠ 0 ∧ R^{t_{0}←hiw(t)}.

d) lf(t : hiext(t_{0}), R) = R^{t←hiext(t,t_{0})}.

e) lf(t : loext(t_{0}), R) = R^{t←loext(t,t_{0})}. Legyen A = T és t : T.

f) lf(t : lorem, R) = dom(t) ≠ 0 ∧ R^{t←lorem(t)}.

g) lf(t : hirem, R) = dom(t) ≠ 0 ∧ R^{t←hirem(t)}. Legyen A = T × T_{0} × N és t_{0} : T_{0}, t : T, i : N.

h) lf(t_{0} := t_{i}, R) = 1 ≤ i ≤ dom(t) ∧ R^{t_{0}←t_{i}}.

i) lf(t_{i} := t_{0}, R) = 1 ≤ i ≤ dom(t) ∧ R^{t←t′},

ahol t′ ∈ T, t′_{j} = t_{j} ha i ≠ j és t′_{i} = t_{0}. Legyen A = T × T_{0} és t_{0} : T_{0}, t : T.

j) lf(t_{0}, t : lopop, R) = dom(t) ≠ 0 ∧ R^{t_{0},t←low(t),lorem(t)}, t_{0}, t : lopop ≡ t_{0}, t := t.low, t : lorem.

k) lf(t_{0}, t : hipop, R) = dom(t) ≠ 0 ∧ R^{t_{0},t←hiw(t),hirem(t)}, t_{0}, t : hipop ≡ t_{0}, t := t.low, t : hirem.

6) A  függvény  típusok  műveletei:

dom, lob, hib, hiw, low, t_{0} := f_{k}, f_{k} := t_{0}, hiext, loext, hirem, lorem, hipop, lopop. Legyen F = fun(H, T_{0}).

a) lf(k := f.dom, R) = R^{k←dom(f)}.

b) lf(k := f.lob, R) = R^{k←lob(f)}.

c) lf(k := f.hib, R) = R^{k←hib(f)}.

d) lf(t_{0} := f.low, R) = dom(f) ≠ 0 ∧ R^{t_{0}←low(f)}.

e) lf(t_{0} := f.hiw, R) = dom(f) ≠ 0 ∧ R^{t_{0}←hiw(f)}.

f) lf(t_{0} := f_{k}, R) = lob(f) ≤ k ≤ hib(f) ∧ R^{t_{0}←f_{k}}.

g) lf(f_{k} := t_{0}, R) = lob(f) ≤ k ≤ hib(f) ∧ R^{f←f′}, ahol f′ ∈ F és f′_{i} = f_{i}, ha i ≠ k és f′_{k} = t_{0}.

h) lf(f : hiext(t_{0}), R) = R^{f←hiext(f,t_{0})}.

i) lf(f : loext(t_{0}), R) = R^{f←loext(f,t_{0})}.

j) lf(f : hirem, R) = dom(f) ≠ 0 ∧ R^{f←hirem(f)}.

k) lf(f : lorem, R) = dom(f) ≠ 0 ∧ R^{f←lorem(f)}. l) lf(t_{0}, f : hipop, R) = dom(f) ≠ 0 ∧ R^{t_{0},f←hiw(f),hirem(f)}.

m) lf(t_{0}, f : lopop, R) = dom(f) ≠ 0 ∧ R^{t_{0},f←low(f),lorem(f)}.

7. Szekvenciális input file A SeqInp(T_{0}) = (seq(T_{0}); reset, st, dt, t : read) típust szekvenciális input file-nak nevezzük, ahol lf(st, dt, t : read, R) = dom(t) ≠ 0 ⇒ R^{st,dt,t←norm,low(t),lorem(t)}∧ dom(t) = 0 ⇒ R^{st←abnorm}.

8. Szekvenciális output file A SeqOut(T_{0}) = (seq(T_{0}); create, t : write(t_{0})) típust szekvenciális output filenak nevezzük, ahol

t : write(t_{0}) =^{def} t : hiext(t_{0}).

9. A verem típus A V erem(T_{0}) = (seq(T_{0}); create, pop, push, top, empty) típust verem típusnak nevezzük. Legyen v : V erem, t_{0} : T_{0}.

a) pop(v) =^{def} v : hirem.

b) push(v, t_{0}) =^{def} v : hiext(t_{0}).

c) top(v, t_{0}) =^{def} t_{0} := v.hiw, empty(v) ≡ v.dom = 0.

10. A sor típus A Sor(T_{0}) = (seq(T_{0}); create, pop, push, top, empty) típust sor típusnak nevezzük. Legyen s : Sor, t_{0} : T_{0}.

a) pop(s) =^{def} s : lorem.

b) push(s, t_{0}) =^{def} s : hiext(t_{0}).

c) top(s, t_{0}) =^{def} t_{0} := s.low.

d) empty(s) ≡ s.dom = 0.

11. A vektor típus A T = (fun(H, T_{0}); dom, lob, hib, low, hiw, t_{0} := t_{k}, t_{k} := t_{0}) típust vektor típusnak nevezzük. A vektor típus jele: V ektor(H, T_{0}).

PROGRAMOZÁSI TÉTELEK

1. Lineáris keresés A feladat az, hogy az egész számok egy zárt intervallumán keressük meg a legkisebb adott tulajdonságú egész számot. 24

A = Z × Z × Z, m, n, i : Z. B = Z × Z, m′, n′ : Z. Q_{m′,n′} = (m = m′ ∧ n = n′ ∧ [m, n] ∩ [β] ≠ ∅), R_{m′,n′} = (Q_{m′,n′} ∧ i ∈ [m, n] ∧ β(i) ∧ ∀j ∈ [m, i) : ¬β(j)).

i.) P_{m′,n′} = (Q_{m′,n′} ∧ i ∈ [m, n] ∧ ∀j ∈ [m, i) : ¬β(j)).

i := m ; ¬β(i) ; \overline{i := i + 1}

ii.) P′_{m′,n′} = (Q_{m′,n′} ∧ i ∈ [m − 1, n] ∧ (∀j ∈ [m, i) : ¬β(j)) ∧ ¬l = ∀j ∈ [m, i] : ¬β(j)).

i, l := m − 1, ↓ ; ¬l ; \overline{\frac{l := β(i + 1)}{i := i + 1}}

iii.) Tegyük fel, hogy β = γ ∨ δ és [δ] ∩ [m, n] ≠ ∅. Keressük meg a legkisebb i ∈ [m, n] ∩ [β] elemet, és mondjuk meg azt is, hogy γ(i) igaz-e !

A = Z × Z × Z × L, m, n, i : Z, u : L. B = Z × Z, m′, n′ : Z. Q_{m′,n′} = (m = m′ ∧ n = n′ ∧ [m, n] ∩ [δ] ≠ ∅), R_{m′,n′} = (Q_{m′,n′} ∧ u = (∃j ∈ [m, n] : γ(j) ∧ ∀k ∈ [m, j − 1] : ¬δ(k))∧

u ⇒ (i ∈ [m, n] ∧ γ(i) ∧ ∀j ∈ [m, i − 1] : ¬γ(j)). P_{m′,n′} = (Q_{m′,n′} ∧ i ≤ n ∧ ¬u = ∀j ∈ [m, i] : ¬γ(j)∧

¬v = ∀j ∈ [m, i] : ¬δ(j) ∧ ∀j ∈ [m, i) : ¬β(j)).

i, u, v := m − 1, ↓, ↓ ; ¬u ∧ ¬v ; \overline{\frac{u, v := γ(i + 1), δ(i + 1)}{i := i + 1}}

2. Logaritmikus keresés Legyen H egy olyan halmaz, amin értelmezve van egy rendezési reláció. Legyen

f : Z → H monoton növekedő függvény. A feladat az, hogy eldöntsük egy adott h ∈ H értékről, hogy felveszi-e azt az f függvény egy adott [m, n] ⊂ Z intervallumon, és ha igen, akkor adjuk meg egy olyan pontját, ahol a függvényérték h. 25

A = Z × Z × Z × H × L, m, n, i : Z, h : H, l : L.

B = Z × Z × H, m′, n′ : Z, h′ : H.

Q_{m′,n′,h′} = (m = m′ ∧ n = n′ ∧ h = h′ ∧ ∀k, j ∈ [m, n] : k ≤ j ⇒ f(k) ≤ f(j)), R_{m′,n′,h′} = (Q_{m′,n′,h′} ∧ l = (∃j ∈ [m, n] : f(j) = h)

∧ l ⇒ (i ∈ [m, n] ∧ f(i) = h)).

P_{m′,n′,h′} = (Q_{m′,n′,h′} ∧ [u, v] ⊆ [m, n] ∧ ∀j ∈ [m, n] \ [u, v] : f(j) ≠ h ∧ l = (i ∈ [u, v] ∧ f(i) = h)).

u, v, i, l := m, n, m − 1, ↓ ; ¬l ∧ (u ≤ v) ; \overline{i := [(u + v)/2] ; \ f(i) < h \ f(i) > h \ f(i) = h ; u := i + 1  v := i − 1  l :=↑}

3. Maximumkeresés Legyen H egy tetszőleges rendezett halmaz és f : Z → H egy függvény. Felada-

tunk az, hogy egy adott [u, v] ⊂ Z intervallumban keressük meg az f függvény maximumát és egy olyan helyét, ahol ezt a maximumértéket felveszi. 26

A = H × Z × Z × Z, m : H, u, v, i : Z.

B = Z × Z, u′, v′ : Z.

Q_{u′,v′} = (u = u′ ∧ v = v′ ∧ u ≤ v),

R_{u′,v′} = (Q_{u′,v′} ∧ i ∈ [u, v] ∧ m = f(i) ∧ ∀j ∈ [u, v] : f(j) ≤ f(i)).

P_{u′,v′} = (Q_{u′,v′} ∧ k ∈ [u, v] ∧ i ∈ [u, k] ∧ m = f(i) ∧ ∀j ∈ [u, k] : f(j) ≤ f(i)).

i, k, m := u, u, f(u) ; k ≠ v ; \overline{\  m < f(k + 1)  / ; \begin{aligned}i, m := k + 1, f(k + 1) \\ & SKIP \end{aligned} ; k := k + 1}

4. Feltételes maximumkeresés Legyen H egy tetszőleges rendezett halmaz és f : [m, n] ⊂ Z → H egy függvény.

Legyen β egy az egész számokon értelmezett logikai függvény. Határozzuk meg a [β] ∩ [m, n] halmaz felett az f függvény maximumát és a halmaz azon elemét, amelyen f a maximumértékét felveszi.

A = Z × Z × Z × H × L, m, n, i : Z, h : H l : L. B = Z × Z, m′, n′ : Z. Q_{m′,n′} = (m = m′ ∧ n = n′ ∧ m ≤ n + 1), R_{m′,n′} = (Q_{m′,n′} ∧ l = (∃i ∈ [m, n] : ε(m, n, i)) ∧ l ⇒ ε(m, n, i) ∧ h = f(i))). P_{m′,n′} = (Q_{m′,n′} ∧ u ∈ [m, n]∧

l = (∃i ∈ [m, k] : ε(m, k, i)) ∧ l ⇒ ε(m, k, i) ∧ h = f(i))),

ahol ε(m, k, i) = i ∈ [m, k] ∧ β(i) ∧ ∀j ∈ [m, k] : β(j) ⇒ f(i) ≥ f(j).

k, l := m − 1, ↓ ; k ≠ n ; \overline{\¬β(k + 1)\  β(k + 1) ∧ l  \  β(k + 1) ∧ ¬l ; SKIP \frac{\  h < f(k + 1)  /}{\begin{aligned}i, h := k + 1, f(k + 1) \\ & SKIP \end{aligned}}l, i, h :=↑, k + 1, f(k + 1) ; k := k + 1}

5. Adott tulajdonsággal rendelkező elemek megszámolása Legyen β egy az egész számokon értelmezett logikai függvény. A feladat az, hogy

számoljuk meg, hány helyen igaz β az [m, n] ⊂ Z intervallumban. 27

A = Z × Z × N_{0}, m, n : Z, s : N_{0}. B = Z × Z, m′, n′ : Z. Q_{m′,n′} = (m = m′ ∧ n = n′ ∧ m ≤ n + 1),

R_{m′,n′} = (Q_{m′,n′} ∧ s = ∑_{i=m}^{n} χ(β(i))),

ahol χ : L → N_{0}, χ(↑) = 1, χ(↓) = 0.

P_{m′,n′} = (Q_{m′,n′} ∧ k ≤ n ∧ s = ∑_{i=m}^{k} χ(β(i))).

k, s := m − 1, 0 ; k ≠ n ; \overline{\  β(k + 1)  / ; \begin{aligned}s := s + 1 \\ & SKIP \end{aligned} ; k := k + 1}

6. Összegzés Legyen H egy tetszőleges halmaz, amelyen értelmezett az összeadás művelete.

Tegyük fel, hogy létezik neutrális eleme a H-nak az összeadásra nézve, valamint adott az f : Z → H függvény. Feladatunk az, hogy egy adott [m, n] ⊂ Z intervallumban összegezzük az f függvény értékeit.

A = Z × Z × H, m, n : Z, s : H. B = Z × Z, m′, n′ : Z. Q_{m′,n′} = (m = m′ ∧ n = n′ ∧ m ≤ n + 1),

R_{m′,n′} = (Q_{m′,n′} ∧ s = ∑_{i=m}^{n} f(i)).

P_{m′,n′} = (Q_{m′,n′} ∧ k ≤ n ∧ s = ∑_{i=m}^{k} f(i)).

k, s := m − 1, 0 ; k ≠ n ; \overline{\frac{s := s + f(i + 1)}{k := k + 1}}

7. Rendezés Legyen T tetszőleges rendezett típus és X = seq(T), legyen továbbá x : X. Ren-

dezzük át az x sorozatot úgy, hogy az elemei növekedő sorrendben legyenek. 28

A = X, x : X.
B = X, x′ : X.
Q_{x′} = (x = x′),
R_{x′} = (x ∈ perm(x′) ∧ ϱ(x, 0, x.dom)),
ahol ϱ(x, i, j) = (∀k, l(i < k < l ≤ j) : x_{k} ≤ x_{l}),
μ(x, i, j) = (∀k, l(1 ≤ k ≤ i < l ≤ j) : x_{k} ≤ x_{l}).
P_{x′} = (x ∈ perm(x′) ∧ 0 ≤ k ≤ x.dom ∧ ϱ(x, k, x.dom) ∧ μ(x, k, x.dom)).

k := x.dom ; k ≠ 0 ; \overline{\frac{UJSZELET}{k := m}}

P′ = (ϱ(x, m, l) ∧ μ(x, m, l) ∧ m < l ∧ 1 ≤ l ≤ k ∧ P_{x′}).

UJSZELET m, l := 0, 1 ; l ≠ k ; \overline{\  x_{l+1} < x_{l}  / ; \begin{aligned}m, x_{l}, x_{l+1} := l, x_{l+1}, x_{l} \\ & SKIP \end{aligned} ; l := l + 1}

8. Speciális formában adott függvény értékének kiszámítása adott helyen

8.1. Függvénykompozícióval definiált függvény

Legyen H_{1}, H_{2}, H_{3} tetszőleges halmaz, továbbá f : H_{1} → H_{3}, g : H_{1} → H_{2}, h : H_{2} → H_{3}, olyan függvények, hogy f = h ∘ g. Feladatunk az, hogy meghatározzuk f függvény i ∈ H_{1} helyen felvett értékét.

A = H_{1} × H_{3}, i : H_{1}, z : H_{3}.
B = H_{1}, i′ : H_{1}.
Q_{i′} = (i = i′),
R_{i′} = (Q_{i′} ∧ z = f(i)).
Q′_{i′} = (Q_{i′} ∧ z = g(i)).

\frac{z := g(i)}{z := h(z)}

8.2. Kapcsoszárójellel definiált függvény

Legyen H egy tetszőleges halmaz, továbbá f, h_{1}, ..., h_{k} : Z → H, olyan függvények, hogy

f(i) = \{ \begin{matrix}h_{1}(i), & ha π_{1}(i) \\ ... \\ h_{k}(i), & ha π_{k}(i) \end{matrix}

Feladatunk az, hogy meghatározzuk f függvény i helyen felvett értékét.

A = Z × H, i : Z, z : H.
B = Z, i′ : Z.
Q_{i′} = (i = i′) ∧ i ∈ ∪_{j=1}^{k}[π_{j}]),
R_{i′} = (Q_{i′} ∧ z = f(i)).

\frac{\  π_{1}(i)  \  …  \  π_{k}(i)}{z := h_{1}(i)  …  z := h_{k}(i)}

8.3. Rekurzív függvény

Legyen H egy tetszőleges halmaz, k > 0 egy egész szám, továbbá f : Z → H, h : Z × H^{k} → T olyan függvények, hogy f(0) = t_{0}, f(−1) = t_{−1}, .., f(−k + 1) = t_{−k+1} és ∀i > 0 : f(i + 1) = h(i + 1, f(i), ..., f(i − k + 1)). Feladatunk az, hogy meghatározzuk az f függvény n > 0 helyen felvett értékét.

A = Z × H, n : Z, z : H. B = Z, n′ : Z. Q_{n′} = (n = n′ ∧ n > 0), R_{n′} = (Q_{n′} ∧ z = f(n)). P_{n′} = (Q_{n′} ∧ 0 ≤ i ≤ n ∧ z = f(i), z_{−1} = f(i − 1), .., z_{−k+1} = f(i − k + 1)).

i, z, z_{−1}, .., z_{−k+1} := 0, t_{0}, t_{−1}, .., t_{−k+1} ; i ≠ n ; \overline{\frac{z, z_{−1}, .., z_{−k+1} := h(i + 1, f(i), ..., f(i − k + 1)), z, .., z_{−k+2}}{i := i + 1}}

8.4. Elemenkénti feldolgozás Jelölések: Legyen H tetszőleges halmaz.

X =^{def} X_{1} × ... × X_{n}, X_{i} ⊆ 2^{H}(i = 1, ..., n),

Y =^{def} Y_{1} × ... × Y_{m}, Y_{i} ⊆ 2^{H}(i = 1, ..., m).

x, \overline{x}, \overline{\overline{x}} ∈ X.

1. Def.: (Teljesen diszjunkt felbontás) Azt mondjuk, hogy \overline{x}, \overline{\overline{x}} teljesen diszjunkt felbontása x -nek, ha ∀i ∈ [1, n] : x_{i} = \overline{x}_{i} ∪ \overline{\overline{x}}_{i} és ∀i, j ∈ [1, n] : \overline{x}_{i} ∩ \overline{\overline{x}}_{j} = ∅ .

2. Def.: (Elemenként feldolgozható függvény) Legyen f : X → Y. Ha minden x ∈ X

minden \overline{x}, \overline{\overline{x}} teljesen diszjunkt felbontására i) f(\overline{x}) ∪ f(\overline{\overline{x}}) = f(x), ii) f(\overline{x}) ∩ f(\overline{\overline{x}}) = ∅, akkor f -et elemenként feldolgozhatónak nevezzük.

i.) Első változat Legyen f : X → Y, X, Y ⊆ 2^{H} függvény. 29

A = A_{1} × A_{2},

A_{1} = set(H_{1}), A_{2} = set(H_{2}), H_{1} ⊆ H, H_{2} ⊆ H, x : A_{1}, z : A_{2}.
B = A_{1}, x′ : A_{1}.
Q_{x′} = (x = x′),
R_{x′} = (z = f(x′)).
P_{x′} = (z ∪ f(x) = f(x′) ∧ z ∩ f(x) = ∅).

z := ∅ ; f(x) ≠ ∅ ; \overline{e : mem(x) ; z := z˜∪f(\{e\}) ; x := x ˜−\{e\}}

ii.) Második változat Legyen az f kétváltozós függvény. 30

A = A_{1} × A_{2} × A_{3}, A_{i} = set(H_{i}), H_{i} ⊆ H(i = 1, 2, 3), x : A_{1}, y : A_{2}, z : A_{3}. B = A_{2} × A_{3}, x′ : A_{1}, y′ : A_{2}. Q_{x′,y′} = (x = x′ ∧ y = y′), R_{x′,y′} = (z = f(x′, y′)). P_{x′,y′} = (z ∪ f(x, y) = f(x′, y′) ∧ f(x, y) ∩ z = ∅

∧ (x′ \ x) ∩ y = ∅ ∧ (y′ \ y) ∩ x = ∅).

z := ∅ ; f(x, y) ≠ ∅ ; \overline{e : mem(x ∪ y) ; \ e ∈ x ∧ e ∉ y \ e ∉ x ∧ e ∈ y \ e ∈ x ∧ e ∈ y ; {z := z˜∪f(\{e\}, ∅) \atop x := x ˜−\{e\}} {z := z˜∪f(∅, \{e\}) \atop y := y ˜−\{e\}} z := z˜∪f(\{e\}, \{e\}) ; x := x ˜−\{e\} ; y := y ˜−\{e\}}

iii.) Harmadik változat Az f függvényről feltesszük, hogy (f_{1}, f_{2}) alakú. 31

A = A_{1} × A_{2} × A_{3}, A_{i} = set(H_{i} ⊆ H)(i = 1, 2, 3), x : A_{1}, y : A_{2}, z : A_{3}. B = A_{1}, x′ : A_{1}. Q_{x′} = (x = x′), R_{x′} = (y = f_{1}(x′) ∧ z = f_{2}(x′)). P_{x′} = (y ∪ f_{1}(x) = f_{1}(x′) ∧ y ∩ f_{1}(x) = ∅ ∧ z ∪ f_{2}(x) = f_{2}(x′) ∧ z ∩ f_{2}(x) = ∅).

y, z := ∅, ∅ ; f_{1}(x) ≠ ∅ ∨ f_{2}(x) ≠ ∅ ; \overline{e : mem(x) ; y, z := y˜∪f_{1}(\{e\}), z˜∪f_{2}(\{e\}) ; x := x ˜−\{e\}}

iv.) Általános változat Rögzített m -re, n -re: z_{i} = f_{i}(x_{1}, ..., x_{n})(i = 1, ..., m). 32

\begin{matrix}P_{x′_{1},...,x′_{n}} = (∀i ∈ [1, m] : (z_{i} ∪ f_{i}(x_{1}, ..., x_{n}) = f_{i}(x′_{1}, ..., x′_{n}) \\ ∧ z_{i} ∩ f_{i}(x_{1}, ..., x_{n}) = ∅) ∧ (∀i, j ∈ [1, n] : (x′_{i} \ x_{i}) ∩ x_{j} = ∅)). \end{matrix}

y_{1}, ..., y_{m} := ∅, ..., ∅ ; ∪_{i=1}^{m}f_{i}(x_{1}, ..., x_{n}) ≠ ∅ ; \overline{e : mem(∪_{i=1}^{n}x_{i}) ; \… \  e ∈ x_{i_{1}} ∧ … e ∈ x_{i_{k}} ∧ e ∉ x_{i_{k+1}} ∧ e ∉ x_{i_{n}}  \…; …  {y_{j} := y_{j} ˜∪f_{j}(sl(\{i_{1} … i_{k}\}, e)_{j})(j ∈ \{i_{1}, ..., i_{k}\}) \atop x_{i_{1}}, …, x_{i_{k}} := x_{i_{1}} ˜−\{e\}, …, x_{i_{k}} ˜−\{e\}}  …}

ahol i_{1}, ..., i_{n} az 1, ..., n permutációja, sl : 2^{{1,...,n}} × H → Y,

sl(\{i_{1}, .., i_{k}\}, e)_{i} = \{ \begin{matrix}\{e\}, & ha i ∈ \{i_{1}, ..., i_{k}\} \\ ∅, & ha i ∉ \{i_{1}, ..., i_{k}\} \end{matrix}

az elágazás ”ágainak” száma 2^{n} − 1,

MÁSODIK RÉSZ

PROGRAMTRANSZFORMÁCIÓK

Definíciók Legyen A = A_{1} × ... × A_{n}, a_{i} : A_{i}, S ⊆ A × A^{∗∗}.

1. Azt mondjuk, hogy az S program p(S) programfüggvénye független az A_{i} állapottérkomponenstől, ha ∀a, b ∈ D_{p(S)} : (∀k ∈ ([1, i − 1] ∪ [i + 1, n]) : a_{k} = b_{k}) → p(S)(a) = p(S)(b).

2. Azt mondjuk, hogy az a_{i} : A_{i} változó konstans függvény az S programban, ha ∀a ∈ A : ∀α ∈ S(a) : (∀α_{k} ∈ α : α_{k}_{i} = a_{i}).

3. Azt mondjuk, hogy az S program végrehajtása nem változtatja meg az a_{i} : A_{i} változót, ha ∀a ∈ D_{p(S)} : p(S)(a)_{i} = a_{i}).

Tételek

1. Nem megengedett elágazásfeltételek kitranszformálása Legyen S ⊆ A × A^{∗∗}, ahol S = IF (π_{1} : S_{1}, ..., π_{n} : S_{n}), A = A_{1} × ... × A_{m}. Legyen

S_{IF} ⊆ A′ × A′^{∗∗}, ahol A′ = A_{1} × ... × A_{m} × L_{1} × ... × L_{n}, a_{i} : A_{i}, l_{j} : L_{j}.

S′ ⊆ A′ × A′^{∗∗} l_{1} := π_{1}(a_{1}, ..., a_{m}) ; ... ; l_{n} := π_{n}(a_{1}, ..., a_{m})

Ekkor az S_{IF} =^{def} (S′; IF (l_{1} : S_{1}, ..., l_{n} : S_{n}) program ekvivalens A-n az S programmal.

2. Nem megengedett ciklusfeltétel kitranszformálása Legyen S ⊆ A × A^{∗∗}, ahol S = DO(π, S_{0}), A = A_{1} × ... × A_{m}. Legyen S_{DO} ⊆

A′ × A′^{∗∗}, ahol A′ = A_{1} × ... × A_{m} × L, a_{i} : A_{i}, l : L.

S_{DO} ⊆ A′ × A′^{∗∗} l := π(a_{1}, ..., a_{m}) ; l ; \overline{\frac{S_{0}}{l := π(a_{1}, ..., a_{m})}}

Ekkor az S_{DO} program ekvivalens A-n az S programmal.

3. Szimultán értékadás kitranszformálása S ⊆ A × A^{∗∗}, ahol A = A_{1} × ... × A_{m} S′ ⊆ A′ × A′^{∗∗}, ahol A′ = A_{11} × ... × A_{m1} × A_{12} × ... × A_{m2}, a_{i1} : A_{i1}, a_{i2} : A_{i2}.

S =^{def} a_{11}, ..., a_{m1} := f_{1}(a_{11}, ..., a_{m1}), ..., f_{m}(a_{11}, ..., a_{m1}).

S′ ⊆ A′ × A′^{∗∗} \frac{a_{12}, ..., a_{m2} := f_{1}(a_{11}, ..., a_{m1}), ..., f_{m}(a_{11}, ..., a_{m1})}{a_{11}, ..., a_{m1} := a_{12}, ..., a_{m2}}

Ekkor az S′ program ekvivalens A-n az S programmal. Megj.: Speciális esetek, amikor f_{i} nem függ az A minden komponensétől.

4. Szekvencia két tagjának felcserélése Ha S_{12} = (S_{1}; S_{2}), S_{21} = (S_{2}; S_{1}) és minden olyan állapottérkomponenst, amelytől

S_{1} nem függelen, az S_{2} végrehajtása nem változtat meg és viszont, akkor S_{12} ekvivalens S_{21}-gyel az A-n.

5. Ciklusmagban levő szekvencia két tagjának felcserélése: Ha S = DO(π, S_{0}), S_{0} = (i := i + 1; S_{01}), S′ = (S_{01}^{i←i+1}; i := i + 1) és i konstans

függvény S_{01}-ben, akkor S ekvivalens S′-vel az A-n.

6. Függvény helyettesítése változóval Legyen f az állapottér A_{i_{1}} × ... × A_{i_{k}} alterén értelmezett függvény, mely-

nek értékkészlete a H halmaz (f ∘ (a_{1}, ..., a_{n}) az A-n értelmezett függvény). Ha Sben az a_{i_{1}}, ..., a_{i_{k}} változók konstans függvények, akkor S ekvivalens az

S′ = (z := f(a_{i_{1}}, ..., a_{i_{k}}); S^{f(a_{i_{1}} ,...,a_{i_{k}})←z}) programmal az A-n, ahol S′ ⊆ A′ × A′^{∗∗} és A′ = A_{1} × ... × A_{n} × H, a_{i} : A_{i}, z : H.

7. Rekurzív függvény kitranszformálása Legyen H egy tetszőleges halmaz, k > 0 egy egész szám, továbbá f : Z → H,

h : Z ×H^{k} → T olyan függvények, hogy f(0) = t_{0}, f(−1) = t_{−1} ,..., f(−k +1) = t_{−k+1} és ∀i > 0 : f(i + 1) = h(i + 1, f(i), ..., f(i − k + 1)).

S i := 0 ; S_{1} ; π ; \overline{\frac{S_{0}}{i := i + 1}}

ahol i konstans függvény úgy S_{1}-ben, mint S_{0}-ban, valamint S_{0}-ban hivatkozás történik f(i + 1)-re. Ekkor S ekvivalens a következő programmal az A-n:

i, z, z_{−1}, .., z_{−k+1} := 0, t_{0}, t_{−1}, .., t_{−k+1} ; S_{1} ; π ; \overline{\begin{matrix}z, z_{−1}, .., z_{−k+1} := h(i + 1, f(i), ..., f(i − k + 1)), z, .., z_{−k+2} \\ S_{0} & f(i+1)←z \\ i := i + 1 \end{matrix}}

8. Programinverzió ...

9. Kiemelési szabályok a.) IF (π_{1} : (S; S_{1}), π_{2} : (S; S_{2})) ekvivalens A-n az S; IF (π_{1} : S_{1}, π_{2} : S_{2} program-

mal, ha a π_{1} és π_{2} függvényekre és az S programra alkalmazható a függvény helyettesítése változóval transzformáció.

b.) IF (π : a :=↑, ¬π : a :=↓) ≡ a := π. ...

TÍPUSTRANSZFORMÁCIÓK PROGRAMOZÁSI TÉTELEKRE

1. Sorozatról file-ra előreolvasási technikával Legyen T egy tetszőleges típus és legyen a : seq(T; low, lorem, dom). Legyen

továbbá x : seq(T; lopop) egy olyan file, amelynek végét egy extremális elem jelzi.

a.low ; a : lorem ; a.dom ≠ 0  dx, x : lopop ; dx ; dx, x : lopop ; dx ≠ EXT R

2. Halmazról sorozatra elemenkénti feldolgozással

Legyen T tetszőleges típus és legyen x, y, z : set(T). Legyenek továbbá a, b : seq(T; dom, low, lorem) szigorúan monoton növekvő sorozatok, és c : seq(T; hiext) egy tetszőleges sorozat.

z := ∅ ; x ≠ ∅ ∨ y ≠ ∅ ; e : mem(x ∪ y) ; z˜∪ ; x ˜− ; e ∈ x , e ∉ x  c := () ; a.dom ≠ 0 ∨ b.dom ≠ 0 ; e := min(a.low, b.low) ; c : hiext ; a : lorem ; e = a.low , e < a.low !!

3. Intervallumon értelmezett függvényről sorozatra Legyenek m és n tetszőleges egész számok (m ≤ n), legyen T tetszőleges típus és

legyen f : fun([m, n], T). Legyen továbbá x : seq(T; dom, low, lorem egy sorozat.

i = n ; f(i + 1) ; i := i + 1 ; f(m)  x.dom = 0 ; x.low ; x : lorem ; x.low

4. Sorozatról vektorra (vagy függvény típusra) Legyen T tetszőleges típus és legyen a : seq(T; dom, low, lorem, hiext). Legyen

továbbá v : V ektor(Z, T) egy vektor (i, j ∈ [v.lob, v.hib], i ≤ j).

a.dom = 0 ; a.low ; a : lorem ; a : hiext(e)  i = j ; v(i) ; i := i + 1 ; v(j + 1), j := e, j + 1

ÁLLAPOTTÉRTRANSZFORMÁCIÓ

...

ADATABSZTRAKCIÓ

...

FÜGGVÉNYABSZTRAKCIÓ

...

VISSZALÉPÉSES KERESÉS

1. A feladat megfogalmazása Legyenek U_{1}, …, U_{n} véges halmazok, ahol az egyes halmazok számosságát jelölje

σ_{i}, azaz σ_{i} =^{def} |U_{i}| (∀i ∈ [1, n]) és tegyük fel, hogy σ_{1} ≠ 0. Jelölje U az U_{i} halmazok direktszorzatát: U =^{def} ×_{i=1}^{n}U_{i}. Legyen ϱ : U → L egy olyan tulajdonság (logikai függvény), amelyhez megadható egy ϱ_{i} (i ∈ [0, n]) tulajdonságsorozat, amelyre:

i) ϱ_{0} =^{def} igaz,

ii) ϱ_{i+1}(u) ⇒ ϱ_{i}(u) (∀i ∈ [0, n − 1]), iii) ∀j ∈ [1, i] : u_{j} = v_{l} ⇒ ϱ_{i}(u) = ϱ_{i}(v),

azaz ϱ_{i} csak az U első i komponensétől függ, iv) ϱ_{n} = ϱ.

A feladat: döntsük el, hogy van-e olyan u ∈ U, amelyre ϱ(u) igaz, s ha van, adjunk is meg egy ϱ tulajdonságú elemet!

2. A feladat specifikációja

Legyen N = ×_{i=1}^{n}V_{i}, ahol V_{i} = [0, σ_{i} − 1] ⊂ N_{0} (∀i ∈ [1, n]). Ekkor |N| = |U|. Sorszámozzuk meg az U_{i}-beli elemeket 0-tól σ_{i} − 1 -ig (∀i ∈ [1, n]), s jelölje u_{i_{j}} ∈ U_{i} a megfelelő elemeket. Ekkor kölcsönösen egyértelműen megfeleltethetjük egymásnak N és U elemeit — jelölje ezt a leképezést ϕ. Így ϕ : N → U, s ha ν ∈ N, akkor ϕ(ν) = (u_{1_{ν1}}, …, u_{n_{νn}}). Az N elemei tekinthetők vegyes számrendszerbeli számoknak. Ezzel definiálunk ui. egy rendezést N -en, így van értelme egy elem ”rákövetkezőjéről” beszélni.

Jelöljük f(ν) -vel a ν ∈ N vegyes számrendszerbeli szám értékét, azaz legyen

f(ν) =^{def} ∑_{i=1}^{n} (ν_{i} ∏_{j=i+1}^{n} σ_{j}).

Ha ν′, ν′′ ∈ N, akkor ν′ < ν′′ ⇔ f(ν′) < f(ν′′). Jelölje továbbá

ε_{0} az N −beli zéruselemet : ε_{0} =^{def} (0, 0, …, 0),

ε_{n} az N −beli egységelemet : ε_{n} =^{def} (0, 0, …, 1),

ε_{i} =^{def} (0, 0, …, i, …, 1) azt az N −beli értéket, amelyre f(ε_{i}) =^{def} ∏_{j=i+1}^{n} σ_{j}.

A fentiek figyelembevételével megfogalmazhatjuk a feladat specifikációját:

A = N × L, ν : N, l : L.
Q = (igaz),
R = (l = (∃ν′ ∈ N : ϱ(ϕ(ν′))) ∧ l ⇒ ϱ(ϕ(ν)).

3. A megoldás előállítása

A fenti feladat — ha nem használjuk ki a ϱ speciális jellemzőit — visszavezethető a lineáris keresés tételének harmadik változatára a következő megfeleltetésekkel:

[m, n] ⟶ [f^{−1}(0), f^{−1}(|N| − 1)]
u ⟶ l
γ ⟶ ϱ
δ ⟶ f(ν) = |N| − 1

A kapott program:

l, v, ν := ϱ(ϕ(ε_{0})), (f(ε_{0}) = |N| − 1), ε_{0} ; ¬l ∧ ¬v ; \overline{ν := ν ⊕ ε_{n} ; l := ϱ(ϕ(ν)) ; v := (f(ν) = |N| − 1)}

Lényegesen növelhetjük az algoritmus hatékonyságát, ha kihasználjuk a ϱ speciális tulajdonságát, azaz azt, hogy ha ϱ_{i}(ϕ(ν)) igaz és ϱ_{i+1}(ϕ(ν)) hamis, akkor minden olyan ν′-re, amely az első i + 1 komponensében megegyezik ν-vel, ϱ_{i+1}(ϕ(ν′)) hamis lesz, a ϱ iii) tulajdonsága miatt. Ekkor tehát a ν-vel együtt elvethetjük az összes ilyen ν′- t is!

Így célszerűbb ν ⊕ ε_{n} helyett ν ⊕ ε_{i+1} -et venni, ami tulajdonképpen a ν vegyes számrendszerbeli szám inkrementálása az (i + 1). pozíción. Az inkrementálást könnyebben kezelhetjük a programban, ha ν-t kiegészítjük egy túlcsordulást jelző bittel — jelölje ezt c. Ekkor, ha c értéke 1 -re változik, ez azt jelenti, hogy nincs több lehetőségünk értelmes ν választására.

A fentiekből következik, hogy az l := ϱ(ϕ(ν)) értékadást érdemes kiegészíteni annak vizsgálatával, hogy melyik az a legkisebb index, amelyre már ϱ_{i}(ϕ(ν)) hamis.

Alkalmazzuk a levezetési szabályokat! A ciklus invariánsának válasszuk a következőt:

\begin{matrix}P : (∀ν′, (0 ≤ f(ν′) < f(ν) + c|N| : ¬ϱ(ϕ(ν′)))∧ \\ l = ϱ(ϕ(ν)) ∧ ¬l ⇒ (ϱ_{m−1}(ϕ(ν)) ∧ ¬ϱ(ϕ(ν)) ∧ (∀i ∈ [m + 1, n] : ν_{i} = 0)). \end{matrix}

Ha ciklusfeltételnek π = ¬l ∧ (c = 0) -t választjuk, akkor P ∧ ¬π ⇒ R valóban teljesül. A terminátor függvény legyen t = |N| − f(ν) − c|N|. Amíg P ∧ π igaz, addig a t > 0 nyilván teljesül. A t csökkentéséről a ν inkrementálásával gondoskodunk.

ν, c, m := ε_{0}, 0, 1 ; KER(ν, m, l) ; ¬l ∧ (c = 0) ; \overline{\frac{SUM(ν, m, c)}{KER(ν, m, l)}}

A KER(ν, m, l) programnak biztosítania kell a ciklus Q ⇒ P feltételének teljesülését is.

A_{KER} = N × N_{0} × L, ν : N, m : N_{0}, l : L.
B_{KER} = N × N_{0}, ν′ : N, m′ : N_{0}.
Q_{KER} = (ν = ν′ ∧ m = m′ ∧ ϱ_{m′−1}(ϕ(ν))),
R_{KER} = (ν = ν′ ∧ ϱ_{m′−1}(ϕ(ν)) ∧ l = (∀i ∈ [m′, n] : ϱ_{i}(ϕ(ν)))
∧ ¬l ⇒ (¬ϱ_{m}(ϕ(ν)) ∧ ∀i ∈ [m′, m − 1] : ϱ_{i}(ϕ(ν)))).

Ez a feladat visszavezethető a lineáris keresés harmadik változatára, azzal a megfontolással, hogy az az állítás, hogy egy tulajdonság egy intervallum minden elemére igaz, ekvivalens azzal az állítással, hogy nem létezik az intervallumnak olyan eleme, amelyre a tulajdonság nem igaz.

u ⟶ ¬l
i ⟶ m
γ ⟶ ϱ(m)
δ ⟶ (m = n)

KER(ν, m, l) l, m :=↑, m − 1 ; l ∧ (m ≠ n) ; \overline{\frac{l := ϱ_{m+1}(ϕ(ν))}{m := m + 1}}

A főprogramban így Q′ = (R_{KER} ∧ (ν = ε_{0}) ∧ (c = 0)) lesz, s ebből Q′ ⇒ P belátható.

A SUM(ν, m, c) program legyen a következő:

A_{SUM} = N × N_{0} × E, ν : N, m : N_{0}, c : E.

B_{SUM} = N × N_{0}, ν′ : N, m′ : N_{0}.

Q_{SUM} = (ν = ν′ ∧ m = m′),

R_{SUM} = ((f(ν) + c|N| = f(ν′) + ∏_{i=m′+1}^{n} σ_{i}) ∧ m ∈ [0, m′] ∧

(∀i ∈ [m + 1, m′] : ν_{i} = 0) ∧ (c = 0 ⇒ ν_{m} ≠ 0)).

Invariáns tulajdonságnak a következőt vehetjük:

\begin{matrix}P_{SUM} : ((f(ν) + c ∏_{i=m+1}^{n} σ_{i} = f(ν′) + ∏_{i=m′+1}^{n} σ_{i}) ∧ m ∈ [0, m′]∧ \\ (∀i ∈ [m + 1, m′] : ν_{i} = 0) ∧ (c = 0 ⇒ ν_{m} ≠ 0)). \end{matrix}

A ciklusfeltétel legyen π_{SUM} = (m ≠ 0) ∧ (c ≠ 0), s ekkor belátható, hogy P_{SUM} ∧ ¬π_{SUM} ⇒ R_{SUM}. A terminátorfüggvény legyen t_{SUM} = m + c. Amíg P_{SUM} ∧ π_{SUM} igaz, addig t_{SUM} > 0 is nyilván teljesül. A t_{SUM} értéke akkor csökken, ha vagy met, vagy c-t csökkentjük.

SUM(ν, m, c) c := 1 ; m ≠ 0 ∧ c ≠ 0 ; \overline{\frac{\  ν^{m} = σ^{m} − 1  /}{\begin{aligned}ν_{m}, m := 0, m − 1 \\ & c, ν_{m} := 0, ν_{m} + 1 \end{aligned}}}

Legyen Q′_{SUM} = (ν = ν′ ∧ m = m′ ∧ c = 1), ekkor Q′_{SUM} ⇒ P_{SUM} teljesül. P_{SUM} ∧ π ⇒ lf(S_{0_{SUM}} , P_{SUM}) belátásához igazolnunk kell, hogy

\begin{matrix}i) P_{SUM} ∧ π ∧ ν_{m} = σ_{m} − 1 ⇒ lf(ν_{m} := 0; m := m − 1, P_{SUM}) \\ ii) P_{SUM} ∧ π ∧ ν_{m} = σ_{m} − 1 ⇒ lf(c := 0; ν_{m} := ν_{m} + 1, P_{SUM}) \end{matrix}

teljesül. Ezek beláthatók f(ν) definíciójának segítségével.

A SUM program levezetése után a főprogram helyességéhez már csak a P ∧ π ⇒ lf(SUM; KER, P) teljesülése szükséges, s ez a fentiekből következik.

IDŐSZERŰSÍTÉS

1. Az időszerűsítés definíciója

Tegyük fel, hogy van egy adatállományunk, ami azonos típusú rekordok sorozata. Nevezzük ezt törzsfile-nak:

\begin{matrix}T = it(E), \\ to : T. \end{matrix}

Továbbá adott transzformációk egy sorozata, nevezzük ezt módosítófile-nak:

\begin{matrix}M = it(F), F = \{ f | f : T → T reláció\}, \\ m : M. \end{matrix}

A feladat a törzsfile aktualizálása a módosítófile alapján, azaz a módosítófile-beli transzformációsorozat végrehajtásával kapott új törzsfile meghatározása. Jelölje ezt a transzformációt:

t = id(to, m), másképpen t = ( m_{|m|} ∘ … ∘ m_{1})(to).

Ez a megfogalmazás még túl általános, a függvény tényleges kiszámíthatóságához néhány további tulajdonságát is meg kell adnunk. i.) Legyenek to és m kulcsos szekvenciális file-ok.

\begin{matrix}T = seq(E), E = (K, D) \\ M = seq(F), F = (K, V) \end{matrix}

ahol K tetszőleges rendezett halmaz, a rekord kulcsrésze, D az adatrész típusa, és V adja a végrehajtandó transzformációt. ii.) Legyen to kulcs szerint egyértelmű file, azaz egy kulcs csak egyszer forduljon elő benne.

to : T, ∀ i, j ∈ [1, to.dom] : t_{i}.K = t_{j}.K ⇔ i = j.

iii.) Végül leszűkítjük a lehetséges transzformációkat is:

V = (W 1; W 2; W 2), W 1 = {törlés}, W 2 = ({beszúrás}, D), W 3 = ({javitás}, M′),

M′ = seq(G), ahol G − be a D → D alakú leképezések tartoznak.

Definiáljuk ezen módosító transzformációk hatását a törzsfile-ra! (A definíciókat halmazokra írjuk fel, ami to kulcs szerinti egyértelműsége miatt megengedhető.) Legyen m_{i} : M. Az m_{i}.W 1, azaz a törlés transzformáció hatása

{m_{i}(t)} = {t_{j}|t_{j} ∈ t ∧ t_{j}.K ≠ m_{i}.K}.

Az m_{i}.W 2, azaz a beszúrás transzformáció hatása

\{m_{i}(t)\} = \{t\} ∪ \{ \begin{matrix}∅ & , ha ∃k ∈ [1, t.dom] : t_{k}.K = m_{i}.K \\ \{(m_{i}.K, m_{i}.D)\} & , ha ∃k ∈ [1, t.dom] : t_{k}.K = m_{i}.K \end{matrix}

Az m_{i}.W 3, azaz a módositás transzformáció hatása

\begin{matrix}\{m_{i}(t)\} = \{t_{j}|t_{j} ∈ t ∧ t_{j}.K ≠ m_{i}.K\}∪ \\ ∪ \{ \begin{matrix}∅ & , ha ∃k ∈ [1, t.dom] : t_{k}.K = m_{i}.K \\ \{(m_{i}.K, m_{i}.M′(t_{k}.D)) \\ |t_{k} ∈ t ∧ m_{i}.K = t_{k}.K\} & , ha ∃k ∈ [1, t.dom] : t_{k}.K = m_{i}.K \end{matrix} \end{matrix}

Def.: (Közönséges időszerűsítés) Az időszerűsítést közönségesnek nevezzük, ha az i.), ii.) és iii.) megkötések teljesülnek rá.

Def.: (Egyszerű időszerűsítés) A közönséges időszerűsítést egyszerűnek nevezzük, ha G egyértelmű és konstans transzformáció. Ekkor egy javítás egyetlen konstans transzformáció, vagyis valójában csere.

2. Egyértelmű módosítófile esete

A következőkben egyértelmű módosító file esetén három különböző mélységű absztrakción alapuló megközelítéssel állítunk elő egy-egy megoldást.

Tegyük fel tehát, hogy a módosítófile egyértelmű kulcs szerint, s adjuk meg a feladat specifikációját:

A = T × T × M, t : T, to : T, m : M. B = T × M, to′ : T, m′ : M. Q = (to = to′ ∧ m = m′ ∧ az időszerűsités egyszerű és m′ egyértelmű), R = (t = id(to′, m′)).

2.1. Visszavezetés halmazok uniójára

Milyen kulcsok lesznek az új törzsfile-ban, t-ben? Biztos, hogy csak olyanok, amelyek vagy to′-ben, vagy m′-ben, vagy mindkettőben szerepeltek. Próbáljuk meg visszavezetni a feladatot két halmaz uniójára!

Jelölje K(to) a to-beli, K(m) az m-beli kulcsok halmazát, valamint k(to) azt a tobeli, és k(m) azt az m-beli elemet, aminek a kulcsa k.

Bővítsük az adatok halmazát: D′ = (D ∪ {üres}). Az egyes transzformációk értelmezési tartománya és értékkészlete felírható D′

segítségével:

W 1 : D → {üres} − − a törlés
W 2 : {üres} → D − − a beszúrás
W 3 : D → D − − a módositás

Ha egy elem adatrésze üres, akkor ez az elem nem létezik, nem írhatjuk ki az új törzsfile-ba.

Emlékeztetőül a z = x ∪ y program:

z := ∅ ; x ≠ ∅ ∨ y ≠ ∅ ; \overline{e : mem(x ∪ y) ; \ e ∈ x ∧ e ∉ y \ e ∉ x ∧ e ∈ y \ e ∈ x ∧ e ∈ y ; {z := z˜∪\{e\} \atop x := x ˜−\{e\}}  {z := z˜∪\{e\} \atop y := y ˜−\{e\}}  z := z˜∪\{e\} ; x := x ˜−\{e\} ; y := y ˜−\{e\}}

Mi felel meg ennek az időszerűsítési feladatban?

x  ⟶  to

y  ⟶  m
z  ⟶  t
x ≠ ∅ ∨ y ≠ ∅  ⟶  to ≠ ∅ ∨ m ≠ ∅
e : mem(x ∪ y)  ⟶  k : mem(K(to) ∪ K(m))
e ∈ x  ⟶  k ∈ K(to)
e ∈ y  ⟶  k ∈ K(m)

A megfelelő program:

t := ∅ ; to ≠ ∅ ∨ m ≠ ∅ ; \overline{k : mem(K(to) ∪ K(m)) ; \k ∈ K(to) ∧ k ∉ K(m) \k ∉ K(to) ∧ k ∈ K(m) \k ∈ K(to) ∧ k ∈ K(m) ; S1  S2  S3}

Vizsgáljuk az elágazás egyes ágainak megfelelő programokat! Első eset. Ha a k kulcs csak to-ban szerepelt, m-ben nem, az azt jelenti, hogy nincs erre az elemre vonatkozó módosítás m-ben. Ekkor hozzá kell venni az új törzsfilehoz, és el kell hagyni to-ból.

S1 {t := t ∪ \{k(to)\} \atop to := to − \{k(to)\}}

Második eset. Ha a k kulcs csak m-ben szerepelt, to-ban nem, akkor csak a beszúrás transzformáció hajtható végre helyesen, s az m-ből kell elhagyni a k kulcsú transzformációt.

S2 \ k(m).W 1 \  k(m).W 2  \ k(m).W 3 ; hiba(1)  t := t ∪ {(k, k(m).D)}  hiba(2) ; m := m − {k(m)}

Harmadik eset. Ha a k kulcs to-ban is és m-ben is szerepelt, akkor a törlés és a javitás transzformációk hajthatók végre, s mindkét file-ból el kell hagyni a k kulcsú elemet:

S3 \ k(m).W 1 \ k(m).W 2 \  k(m).W 3 ; SKIP  {hiba(3) \atop t := t ∪ \{k(to)\}} t := t ∪ \{(k, k(m).G(k(to).D))\} ; to := to − \{k(to)\} ; m := m − \{k(m)\}

Ha a program hibajelzéseket is ad, azokat a jelzett ágakon kell megvalósítani. Térjünk vissza az eredeti feladathoz, amikor a törzsfile-t és a módosítófile-t nem

halmazként, hanem szekvenciális file-ként kezeljük. Tegyük fel, hogy mindkét file elemei kulcs szerint rendezettek, s a file végét egy extremális (minden más kulcsnál nagyobb kulcsú) elem jelöli. A megoldó program ekkor:

t := ∅ ; dto, to : lopop ; dm, m : lopop ; dto.K ≠ EXT R ∨ dm.K ≠ EXT R ; \overline{k : mem(K(to) ∪ K(m)) ; \ dto.K < dm.K \ dm.K < dto.K  \ dm.K = dto.K ; {t : hiext(dto) \atop dto, to : lopop}  S2  S3} ; t : hiext(EXT R)

S2 \ dm.W 1 \  dm.W 2  \ dm.W 3 ; hiba(1) t : hiext(dm.K, dm.D) hiba(2) ; dm, m : lopop

S3 \ dm.W 1 \ dm.W 2  \  dm.W 3 ; SKIP {hiba(3) \atop t : hiext(dto)}  t : hiext(dto.K, dm.D) ; dto, to : lopop ; dm, m : lopop

2.2. Megoldás az elemenkénti feldolgozás fogalmának segítségével

A halmazműveletek — mint a fenti unió — általánosításával, az absztrakzió szintjét növelve, eljuthatunk az elemenkénti feldolgozás fogalmához, s így megfogalmazhatjuk, mi az, ami ezekben a feladatokban közös, ami miatt az elemenként feldolgozható függvények helyettesítési értékét kiszámító program mindig ugyanaz.

Az előbbi feladat megoldását kétféleképpen is visszavezethetjük az elemenkénti feldolgozásra.

2.2.1. Visszavezetés egyváltozós elemenkénti feldolgozásra

Az időszerűsítési feladat állapotterét elképzelhetjük úgy is, hogy ha vesszük a törzsfile-beli és a módosítófile-beli kulcsok halmazának unióját, lesznek olyanok, amelyekhez csak egy törzsfile-beli adatrész tartozik, lesznek olyanok, amelyek a törzsfileban nem szerepelnek, s végül, lesznek olyanok, amelyek mindkettőben. Így gondolatban a törzsfile-ból és a módosítófile-ból létrehozhatunk egy olyan állományt, amelyek elemei három komponensből állnak: egy kulcsból (vagy to-ból, vagy m-ből), egy to-beli adatrészből (aminek értéke esetleg üres), és egy m-beli transzformációrészből (ami esetleg üres, s ez az identikus leképezést jelzi). A két utóbbi mező természetesen nem lehet egyszerre üres. Formálisan leírva:

X = seq(DX),
DX = (K, D′, V′),
D′ = D ∪ {üres},
V′ = V ∪ {üres}.

Legyen x : X. Ekkor K(x) = K(to) ∪ K(m). Jelölje dx az x egy tetszőleges elemét. Ekkor az előbbiek alapján

dx.D′ = \{ \begin{matrix}üres & , ha dx.K ∉ K(to) \\ dx.K(to).D & , ha dx.K ∈ K(to) \end{matrix}

dx.V′ = \{ \begin{matrix}üres & , ha dx.K ∉ K(m) \\ dx.K(m).V & , ha dx.K ∈ K(m) \end{matrix}

Állapottértranszformációt alkalmazunk, így a feladat ezen az állapottéren felfogható egyváltozós elemenkénti feldolgozásnak, a következő f függvénnyel: f({e}) = (e.K, e.V′(e.D)), azaz a transzformációs részt alkalmazzuk az adatrészre

e.V′.üres(e.D′) = e.D′
e.V.W 1(e.D′) = üres, ha e.D′ = üres
e.V.W 2(üres) = e.V.W 2.D
e.V.W 3(e.D′) = e.V.W 3.D, ha e.D′ = üres

A specifikáció ezen az állapottéren:

A = X × T, x : X, t : T.
B = X, x′ : X.
Q = (x = x′ ∧ az időszerűsités egyszerű),
R = (t = f(x′)).

A program:

t := ∅ ; x ≠ ∅ ; \overline{e : mem(x) ; d := f(\{e\}) ; t := ∪\{d\} ; x := x − \{e\}}

A d := f({e}) program megvalósítása:

d := f(\{e\}) \frac{\e.D′ ≠ üres ∧ e.V′ = üres\e.D′ = üres ∧ e.V′ ≠ üres\e.D′ ≠ üres ∧ e.V′ ≠ üres}{d : (e.K, e.D′)  {hiba(3) \atop t : hiext(dto)}  t : hiext(dto.K, dm.D)}

Térjünk vissza az eredeti állapottérre:

x ≠ ∅  ⟶ to ≠ ∅ ∨ m ≠ ∅
e : mem(x)  ⟶ k : mem(K(to) ∪ K(m))
e.D′ ≠ üres ∧ e.V′ = üres ⟶ k ∈ K(to) ∧ k ∉ K(m)
e.D′ = üres ∧ e.V′ ≠ üres ⟶ k ∉ K(to) ∧ k ∈ K(m)
e.D′ ≠ üres ∧ e.V′ ≠ üres ⟶ k ∈ K(to) ∧ k ∈ K(m)
t := t ∪ {d}  ⟶ t, ha d = ∅
t ∪ {d}, ha d ≠ ∅
x := x − {e}  ⟶ to := to − {k(to)}, ha k ∈ K(to) ∧ k ∉ K(m)

m := m − {k(m)}, ha k ∉ K(to) ∧ k ∈ K(m)

to := to − {k(to)}

m := m − {k(m)}, ha k ∈ K(to) ∧ k ∈ K(m)

A t := t ∪ {d} és az x := x − {e} programok függetlenek egymástól, így felcserélhetők. Felhasználva, hogy a d := f({e}) és az x := x − {e} utasításokat megvalósító programok feltételrendszere megegyezik, valamint beépítve az uniót a d := ∅- t nem tartalmazó ágakba, pontosan azt a programot kapjuk, mint az előbb.

2.2.2. Visszavezetés kétváltozós elemenkénti feldolgozásra

Feladatunkat talán legegyszerűbben a kétváltozós egyértékű elemenkénti feldolgozásra vezethetjük vissza (ill. a kétváltozós kétértékű elemenkénti feldolgozásra, ha a hibajelzéseket is kezelni akarjuk):

A = T × M × T, to : T, m : M, t : T.
B = T × M, to′ : T, m′ : M.
Q = (to = to′ ∧ az időszerűsités egyszerű és m′ egyértelmű),
R = (t = id(to′, m′)).

Az időszerűsítő függvény (a speciális feltételek miatt kulcs szerint elemenként feldolgozható) a következőképpen adható meg:

id(k, ∅) = k(to)

id(∅, k) = \{ \begin{matrix}∅ & , ha k(m).W 1 \\ (k, k(m).D) & , ha k(m).W 2 \\ ∅ & , ha k(m).W 3 \end{matrix}

id(k, k) = \{ \begin{matrix}∅ & , ha k(m).W 1 \\ k(to) & , ha k(m).W 2 \\ (k, k(m).D) & , ha k(m).W 3 \end{matrix}

A feladatot megoldó program triviális behelyettesítéssel adódik.

3. Nem egyértelmű módosítófile esete

Abban az esetben, ha nem tételezhetjük fel, hogy az m módosító file egyértelmű, a feladat már nem lesz elemenként feldolgozható.

Ekkor két megoldási absztrakció kínálkozik (továbbra is kihasználjuk természetesen, hogy állományaink kulcs szerint rendezettek).

3.1. Adatabsztrakciós megközelítés

Állapottértranszformációt alkalmazunk, a módosítófile-t úgy tekintjük, hogy elemei (kulcs, transzformációsorozat) típusúak, azaz:

M′ = seq(F′), ahol F′ = (K, V′′), ahol V′′ = seq(V).

Ekkor, ezzel a módosítófile-lal, újból elemenkénti feldolgozáshoz jutunk, csak a megfelelő transzformációsorozatot kell majd megvalósítani az eredeti állapottéren.

id(k, ∅) = k(to)
id(∅, k) = (k, k(m).V′′)
id(k, k) = (k, k(m).V′′(k(to).D))

(A transzformációk kompozíciója az egyes transzformációk értelmezési tartományai és értékkészletei miatt csak a transzformációk megfelelő sorozatára értelmes.)

A kapott program:

t := ∅ ; dto, to : lopop ; dm, m : lopop ; dto.K ≠ EXT R ∨ dm.K ≠ EXT R ; \overline{\frac{\ dto.K < dm.K  \ dm.K < dto.K \ dm.K = dto.K}{{t : hiext(dto) \atop dto, to : lopop}  T RANSZF (üres) {T RANSZF (dto.D) \atop dto, to : lopop}}} ; t : hiext(EXT R)

T RANSZF (P AR) d := P AR ; ak := dm.K ; ak = dm.K ; \overline{\  dm.W 1  \  dm.W 2  \  dm.W 3 ; \frac{\  d = üres  /}{\begin{aligned}hiba(1) \\ & d := üres \end{aligned}}\frac{\ d = üres  /}{\begin{aligned}d := dm.D \\ & hiba(2) \end{aligned}}\frac{\  d = üres  /}{\begin{aligned}hiba(3) \\ & d := dm.D \end{aligned}} ; dm, m : lopop} ; \  d = üres  / ; \begin{aligned}SKIP \\ & t : hiext(EXT R) \end{aligned}

3.2. Függvénytranszformációs módszer

A feladat megoldását általában önkéntelenül befolyásolja a specifikációja is. A fenti egyváltozós elemenkénti feldolgozásból kiindulva nem egyértelmű módosítófile esetén definiálhatunk egy rekurzívan megadott függvényt, amely a megfelelő transzformációsorozatot kiértékeli. A megoldás ebben a megközelítésben (X definícióját ld. fent, azzal a különbséggel, hogy most kulcs szerint nem egyértelmű):

A = X × T, x : X, t : T.
B = X, x′ : X.
Q = (x = x′ ∧ x kulcs szerint rendezett),
R = (t = CONC_{i=1}^{x′.dom}(f(i)_{1}, f(i + 1)_{3}).

ahol CONC csak olyan adatokat konkatenál, amire f_{3} ≠ üres. Az f függvény definíciója:

f : bbfZ → K × D′ × D′ f(0) = (min(x.low.K, EXT R), x.low.D′, üres)

f(i + 1) = \{ \begin{matrix}(f(i)_{1}, x_{i+1}.V′(f)i)_{2}), üres) & , ha f(i)_{1} = x_{i+1}.K \\ (x_{i+1}.K, x_{i+1}.V′(x_{i+1}.D′), f(i)_{2}) & , ha f(i)_{1} ≠ x_{i+1}.K \end{matrix}

open(x) ; dx, x : lopop ; z := ∅ ; dx.K ≠ EXT R ; \overline{\  f_{1} = dx.K  / ; \frac{f_{2} := dx.V′(f_{2})}{f_{3} := üres} ; k := f_{1} ; f_{1} := dx.K ; f_{3} := f_{2} ; f_{2} := dx.V′(dx.D′) ; z : hiext′((k, f_{3})) ; dx, x : lopop} ; z : hiext′((k, f_{3}))

open(x) dm, m : lopop ; dto, to : lopop ; f_{1} := min(dm.K, dt.K) ; \  f_{1} = dt.K  / ; \begin{aligned}f_{2} := dt.D \\ & f_{2} := üres \end{aligned} ; f_{3} := üres

dx, x : lopop \frac{\  dm.K = EXT R ∧ dt.K = EXT R  /}{dx.K := EXT R ; \frac{\ dt.K < dm.K \ dt.K > dm.K \ dt.K = dm.K}{dx.K := dt.K ; dx.D′ := dt.D ; dx.V′ := üres ; dto, to : lopop  dx.K := dm.K ; dx.D′ := üres ; dx.V′ := dm.V ; dm, m : lopop  dx.K := dm.K ; dx.D′ := dt.D ; dx.V′ := dm.V ; dto, to : lopop ; dm, m : lopop}}

f_{2} := dx.V′(p) \frac{\  dx.V′ = üres  /}{f_{2} := p ; \frac{\ dx.V′.W 1  \ dx.V′.W 2  \  dx.V′.W 3}{\frac{\ p = üres  /}{\begin{aligned}hiba \\ & f_{2} := üres \end{aligned}}\frac{\ p = üres  /}{\begin{aligned}f_{2} := dx.D \\ & hiba \end{aligned}}\frac{\  p = üres  /}{\begin{aligned}hiba \\ & f_{2} := dx.V (p) \end{aligned}}}}

z : hiext′((k, f_{3})) \frac{\  f_{3} = üres  /}{\begin{aligned}SKIP \\ & z : hiext((k, f_{3})) \end{aligned}}

LISTÁZÁS

...

HARMADIK RÉSZ

ALGORITMUSOK ÉS ADATSZERKEZETEK

Gráfalgoritmusok

... String keresése stringben

(Pl. Knuth-Morris-Pratt módszer, Boyer-Moore módszer, Dömölki módszere.) ...

Kódolás, tömörítés (Pl. Huffman-kódolás.) ...

PROGRAMOZÁSI TECHNIKA

A modul fogalma

... Szövegkezelés

... File-kezelés

... Menükezelés

...

KIEGÉSZÍTÉSEK, RÉSZLETES MAGYARÁZATOK

1 Bevezetés

Ez a jegyzet programozó matematikusok programozástanulásának bevezetéséhez készült. Ebből következik, hogy benne a programozás matematikai szemléletű megközelítésére törekszünk.

Az első dolgunk logikusan az lenne, hogy megmondjuk, mi is az a programozás. Ez azonban nem is olyan egyszerű feladat. Miért? Próbáljunk egy egyszerű meghatározást adni. ”A feladatot felbontjuk a gép számára már érthető utasítások sorozatára”, vagy ... stb.

Mindenképpen szerepel a meghatározásokban két szó: feladat és gép. De mi az, hogy feladat? Valójában nincs az életünknek olyan területe, problémája ami nem tekinthető ebben az értelemben feladatnak. Ahhoz, hogy értelme legyen a fogalomnak, meg kell keresni, hogy mi a közös a számtalan sok különböző feladatban.

És mit jelent az a szó, hogy gép? Tudjuk, hogy nagyon sok különböző számítógép van. Ezekhez rendkívül sokféle kiegészítő berendezés tartozhat. Sőt, több — esetleg nagyon sok — ”egyszerű” gép kapcsolódhat egymáshoz. Ezen kívül emberi tevékenységek, döntések is befolyásolják a gépek, a géprendszerek működését. Vajon ők nem részei a feladatot megoldó gépnek?

Lehet-e egyáltalán programozásról beszélni ilyen heterogén feltételek mellett? És mi lesz tíz vagy húsz év múlva?

Mi a megoldás? Az absztrakció és a szétválasztás.

A programozás során nem a konkrét feladat és a gépi lehetőségek között teremtünk közvetlen kapcsolatot, hanem választunk egy absztrakt modellt, amiben megfelelő pontossággal leírhatjuk a konkrét feladatot. Ennek az a haszna, hogy az absztrakt modell matematikai eszközökkel kezelhető, a programozási ismeretek pontosan megfogalmazhatók. A probléma szétválik a konkrét feladat modellezésére, az absztrakt programozási feladatra, és a gépi megvalósításra (az implementációra).

A későbbiekben még sokszor látjuk majd, hogy ez a két eszköz — az absztrakció és a szétválasztás — milyen alapvető a programozási tevékenység minden területén.

Még egy kérdést meg kell vizsgálnunk. Ki programozó? Ez sem triviális kérdés. Már régóta nagyon sokan ”programoztak”. Gondoljunk arra, hogy a logarléc is számológép, és annak használata is lényegében programozás volt, ugyanúgy, mint a jelenleg használt asztali és egyéb kalkulátorok, gépek használata.

Vajon mi különbözteti meg a programozót a programkészítőtől? Akinek pl. autója van, az valamilyen szinten képes az autót gondozni, apróbb hibáit kijavítani. Erre ”képesítése” is van, hiszen a jogosítvány megszerzésekor vizsgázott műszaki ismeretekből. Mégis világos, hogy nem mindenki autószerelő szakember, aki autót szerel. Miben különbözik az autószerelő az átlagos autót szerelőtől?

A két kérdésre hasonló a válasz.

A programozó felkészültsége, gyakorlata miatt, és mert bonyolultabb eszközökkel (nem gépi, hanem logikai, matematikai eszközökkel) rendelkezik — és azokat használni is tudja —, ezért képes bonyolultabb feladatok megoldására.

Ahogy egy amatőrnek lehetnek remek műszerei, és profi szakembereket felülmúló ügyessége, érzéke az autószereléshez, ugyanúgy elképzelhető, hogy valaki képesítés szerint nem, de tudása alapján programozó.

Ez azonban nem jelenti azt, hogy aki képesítése szerint programozó, annak nem volna kötelessége megfelelő ismeretekkel rendelkezni.

Ebben a jegyzetben csak az absztrakt programozási feladatokkal foglalkozunk. Ismertetünk egy lehetséges eszköztárat ezek tudományos igényű kezeléséhez.

2 Állapottér

Ha a konkrét valóság valamilyen részét modellezni akarjuk, el kell dönteni, hogy mik azok a jellemzők, amiket a modellben figyelembe veszünk, és ezek milyen értékeket vehetnek föl. Egy-egy jellemző lehetséges értékeinek halmazát jelöltük a definícióban A_{i_{j}} -vel, és neveztük típusértékhalmaznak. Ez az elnevezés azt fejezi ki, hogy az A_{i_{j}} halmaz hasonló, azonos tulajdonságú dolgok lehetséges értékeinek halmaza. Itt most nem foglalkozunk azzal, hogy a hasonlóság miben áll.

Mivel különböző jellemzők lehetséges értékeinek halmaza lehet azonos, ezért a definícióban az A_{i_{j}}-k nem feltétlenül különbözők.

Az A_{i_{j}} halmazokról feltehettük, hogy legfeljebb megszámlálhatóak, hiszen más halmazok úgysem kezelhetők számítástechnikai eszközökkel.

Az, hogy egy adott probléma modellezésénél mi lesz az állapottér, nem egyértelmű. Például egy pont térbeli helyezetét jellemezhetjük derékszögű- vagy polárkoordinátákkal is. Egy sík pontjai megadhatók kétdimenziós térben, de háromdimenziósban is.

Az állapottér megválasztása nagyon fontos dolog, hiszen alapvetően meghatározza, hogy mit és hogyan tudunk leírni. Ha az állapottér túl kevés komponensből áll, akkor van, amit nem tudunk leírni benne, s ha túl sok, akkor fölöslegesen bonyolult lesz a modell. Az, hogy túl sok, vagy túl kevés a komponens, relatív fogalom, attól függ, hogy milyen kérdések vizsgálatára használjuk a modellt.

Általában egy bonyolult, összetett probléma esetén először a legáltalánosabb, legmagasabb szintű kérdéseket vizsgáljuk. Ekkor a modell durva, csak a legfontosabb jellemzőket tartalmazza. Az egyre pontosabb, részletesebb vizsgálatokhoz fokozatosan finomítjuk a modellt is, az állapotteret új komponensekkel bővítjük.

Előfordulhat az is, hogy egy-egy részletkérdést mint önálló problémát az állapottér egy alterén vizsgálunk. (Megjegyzés. Az állapotteret elképzelhetjük úgy is, mint egy gép (adott program által használt) memóriája, regiszterei, adatai és eredményei lehetséges értékeinek halmazát. Ilyenkor az állapottér egy pontját felfoghatjuk az értékek egy sorozatának, amely egy adott időpontban a programozó számára minden fontos információt tartalmaz a gép állapotáról.)

3 A változó fogalma

A változók segítségével egyszerűsíthetjük az állapottéren értelmezett állítások, relációk, tehát feladatok, programfüggvények, predikátumok, leggyengébb előfeltételek stb. leírását.

Mivel minden változó értelmezési tartománya az állapottér, és értékkészlete egy típusértékhalmaz, egy változót jellemezhetünk egy típussal is — így beszélhetünk a változó típusáról. Azt, hogy egy x változó értékkészlete T, így jelöljük: x : T.

A jelölések egyszerűsége érdekében, ha egy formulában minden változó azonos argumentummal szerepel, azt seholsem írjuk ki. Ha x : T egy változó, f egy tetszőleges T -n értelmezett függvény, az f(x) jelölést f(x(a)) (ahol a ∈ A) rövidítéseként használjuk. Legyen például A = Z × Z és x, y : Z. Az R = (x > 0 ∧ y > 0) jelölés az (x(a) > 0 ∧ y(a) > 0 ∧ a ∈ A) állítást jelöli, és [R] = {(a_{1}, a_{2}) ∈ A|a_{1} > 0 ∧ a_{2} > 0}. Ha π predikátum, a π = (x > y) azt je-

lenti, hogy π(a) = \{ \begin{matrix}igaz & , ha x(a) > y(a) \\ hamis & , ha x(a) ≤ y(a) \end{matrix} .

A változók segítségével könnyen felírhatunk olyan függvényeket, amik az állapottér bizonyos komponensein értelmezett v_{1}, …, v_{n} változók függvényei, f ∘ (v_{1}, …, v_{n}) alakban. Ha nem okoz félreértést, ezt így is írjuk: f(v_{1}, …, v_{n}).

4 A feladat fogalma

A feladat definíciója azt fejezi ki, hogy minden programozási feladat megfogalmazható mint egy leképezés az állapottér bizonyos pontjaiból az állapottérbe. Ez a leképezés általában nem egyértelmű.

Lássunk egy példát. A feladat legyen az, hogy keressük meg egy természetes számnak egy természetes osztóját. Mi lehet az állapottér? Mivel két dologról van szó, két számról, ezért kézenfekvő lehetőség, hogy állapottérnek az A = N × N halmazt válasszuk. Az első komponens azoknak a lehetséges értékeknek a halmaza, amiknek az osztóját keressük, a második pedig azoké, amik előfordulhatnak mint osztók. Ekkor a feladat az, hogy olyan (x, y) ∈ A pontba jussunk, ahol y|x. Pontosabban egy (u, v) ∈ A pontból egy (x, y) ∈ A pontba kell jutni, ahol y|x és u = x. Tehát a feladat

F = {((u, v), (x, y)) ∈ A × A| x = u ∧ y|x}.

A konkrét feladat megfogalmazása olyan, hogy más absztrakt feladathoz is eljuthatunk:

F′ = {((u, v), (x, y)) ∈ A × A | y|u}.

Világos, hogy F és F′ különböző feladatok. Ez rámutat az absztrakt modell készítésének egyik fontos okára is: nagyon gyakori, hogy a modellezés közben azért jutunk különböző absztrakt feladatokhoz, mert a konkrét feladat nem pontos, gyakran csak a ”fejünkben van meg”, és ezért lényeges hiányosságok lehetnek benne.

Az absztrakt modell elkészítése után átgondoljuk ismételten, hogy abban vajon valóban az igazi céljainkat fogalmaztuk-e meg.

A következő példánk nem egy tetszőleges, hanem a legnagyobb valódi osztó megkeresése.

Az állapottér maradhat az, ami az előző feladatban volt, a feladat pedig a következő G vagy G′ reláció:

G = {((u, v), (x, y)) ∈ A × A| u összetett szám, x = u,

y az x legnagyobb valódi osztója},

G = {((u, v), (x, y)) ∈ A × A| u összetett szám,

y az u legnagyobb valódi osztója}.

Most a G reláció az összetett számokon értelmezett függvény.

Felmerülhet a kérdés, hogy miért nem az összetett számok halmazát választottuk az állapottér egyik komponensének. Erre a kérdésre később, a típus tárgyalásakor még visszatérünk, egyelőre az ”egyszerűbb” halmazok használata mellett döntünk. (Megjegyzés. Szokásos a programozási feladatot input-output modellként is felfogni: milyen adatokból milyen eredményt kell gyártani. Sokszor azonban — különösen bonyolultabb programrendszerek esetében — nehéz megmondani, mik az adatok és mik az eredmények. Ugyanakkor nyilvánvaló, hogy egy input-output szemléletben megfogalmazott feladat minden nehézség nélkül felírható a definíciónak megfelelő reláció formájában.)

5 A program fogalma

A konkrét programok egyik legszembetűnőbb tulajdonsága a dinamikus viselkedés, a működés. Itt azonban a program definíciója ”statikus”, nem a működés, hanem a működés eredményének absztrakciója. Ebben az a programozói tapasztalat is tükröződik, hogy a ”mit csinál” a fontos, és nem a ”hogyan”. Másrészt ebben a statikus modellben is értelmezhetők az elterjedt dinamikus fogalmak megfelelői. Pédául: a.) Az a ∈ R_{S} sorozatot az S program egy végrehajtásának mondjuk. b.) Az S program az a ∈ A pontból kiindulva a b ∈ A pontban terminál, ha

∃α ∈ S(a) ∩ A^{∗} : b = τ(α). c.) Az S program az a ∈ A pontból indítva terminál, ha S(a) ⊂ A^{∗}. d.) S egy mindenütt termináló program, ha ∀a ∈ A : S(a) ⊂ A^{∗}. e.) Az S program az a ∈ A pontból indítva a b ∈ A pontban abortál, ha

∃α ∈ S(a) ∩ A^{∞} ⇒ ∃i ∈ N : (∀j(j > i) : α_{j} = b). f.) Ha a feladat (program, programfüggvény) függvény, akkor a feladatot (prog-

ramot, programfüggvényt) determinisztikusnak, ellenkező esetben nemdeterminisztikusnak nevezzük.

(Megjegyzés. Az abortálásra is be lehetne vezetni a terminálásnak megfelelően az a pontból indítva abortáló, és a mindenütt abortáló program fogalmát.)

A definíció szerint a programot az egész állapottéren értelmeztük. Ez egyrészt megfelel a valóságnak — egy program valamit minden esetben csinál —, másrészt fölösleges lenne az értelmezési tartomány korlátozását itt lehetővé tenni, hiszen erre szolgál pl. a programfüggvény fogalma. Az a.) kikötés lényegében az üres sorozatot zárja ki a program értékkészletéből.

A program normális működését az állapottéren történő mozgásnak tekintjük. A sorozatok ezt a mozgást rögzítik. Ezért zártuk ki, hogy ilyenkor a sorozatokban egymás mellett szerepelhessen az állapottérnek ugyanaz a pontja. Ezt a lehetőséget, az ismétlődést, az abnormális működés jelzésére használjuk. Ilyenkor a program viselkedése nem írható le a modell keretein belül, s ilyen esetben a további működésről semmit sem tudunk mondani. (Megjegyzés. A megállás gépi szintű realizációja általában egy ugró utasítás saját magára. Azaz a program működik, de nem jut sehova, külső segítségre vár.)

6 A programfüggvény fogalma

A programozót elsősorban az érdekli, hogy egy program egy kezdeti állapotból elindítva mit csinál, azaz terminál-e (véges-e a sorozat), és ha igen, hova, milyen állapotba jutott (mi a sorozat utolsó eleme). Ezért vezettük be a programfüggvény fogalmát.

A programfüggvény nem a program működését, hanem csak a ”jól működés” eredményét adja meg. A ”nem rosszul működés” eredményét is megadhatjuk, erre szolgál a szabad programfüggvény (p′(S)).

D_{p′(S)} = {a ∈ A|S(a) ∩ A^{∗} ≠ ∅},
∀a ∈ D_{p′(S)} :
p′(S)(a) = {b ∈ A|∃α ∈ S(a) ∩ A^{∗} : τ(α) = b}.

Nyilvánvalóan D_{p(S)} ⊂ D_{p′(S)}.

A programfüggvényt nemcsak ”gyengébbre”, hanem ”erősebbre” is választhatjuk. A korlátos programfüggvény jele p_{k}(S).

D_{p_{k}(S)} = {a ∈ A|S(a) ⊂ A ∧ S(a) véges halmaz},
∀a ∈ D_{p_{k}(S)} :
p_{k}(S)(a) = {b ∈ A|∃α ∈ S(a) : τ(α) = b}.

Nyilván D_{p_{k}(S)} ⊂ D_{p(S)}.

A korlátos programfüggvény nemcsak azt garantálja, hogy a program terminál, hanem azt is, hogy korlátos idő alatt.

7 A megoldás fogalma

A megoldás definíciója azt a két kézenfekvő követelményt tartalmazza, hogy a) a program bármelyik lehetséges kezdeti állapotból elindítva biztosan termináljon, és b) a végállapot feleljen meg a feladat követelményeinek. Ha egy programot az állapottérnek egy rögzített pontjából többször elindítunk, előfordulhat, hogy különböző pontokban terminál.

A definíció b.) kikötése pontosan azt jelenti, hogy ezeknek a pontoknak mindegyike a feladatnak megfelelő legyen. Tehát egy feladat szempontjából nem a program, hanem csak a programfüggvény érdekes. Mivel az azonos programfüggvényű programok azonos hatásúaknak tekinthetők, ezért ezeket ekvivalens programoknak nevezzük. (Megjegyzés. Valójában az ekvivalens programok egyéb tulajdonságai nagyon különbözők lehetnek, ami nem elhanyagolható. Ilyen elsősorban a hatékonyság: milyen nagyságú gépet mennyi ideig vesz igénybe a program. Ha készítünk egy programot, és az megoldása a feladatnak, azt mondjuk, hogy a program helyes. Azonban ez még nem jelenti azt, hogy jó munkát végeztünk, hogy jó a program. Pl. egy helyes program lehet teljesen használhatatlan, mert olyan gépi kapacitásigénye van, ami sokszorosa egy vele ekvivalens másik programnak. A program ”jósága” nagyon sok dologtól függ, ennek tárgyalásával itt még nem foglalkozhatunk.)

8 A kiterjesztésre vonatkozó tételek

A tételek állításainak igazolása előtt bebizonyítjuk, hogy minden program ekvivalens a kiterjesztettjével. \underline{Lemma}

Legyen B altere A-nak, S egy program B-n, S′ az S kiterjesztettje A-n. Ekkor S és S′ ekvivalensek B-n. \underline{Bizonyitás}

Azt kell belátnunk, hogy pr_{B×B}(p(S′)) = pr_{B×B}(p(S)) = p(S). a.) pr_{B}(D_{p(S′)}) = D_{p(S)}.

A programfüggvények értelmezési tartományainak projekciója megegyezik. Ez abból következik, hogy a projekció nem változtatja meg egy sorozat hosszát.

b.) Legyen a ∈ D_{p(S′)}, b ∈ D_{p(S)} úgy, hogy pr_{B}(a) = b teljesül. Ilyen a és b létezik (ha D_{p(S)} ≠ ∅) a fentiek szerint. Belátjuk, hogy pr_{B}(p(S′)(a)) = p(S)(b). Mivel a ∈ D_{p(S′)}, ezért tetszőleges α ∈ S(a) véges, azaz létezik τ(α). pr_{B}(p(S′)(a)) = pr_{B}(∪_{α∈S′(a)}τ(α)) = ∪_{α∈S′(a)}pr_{B}(τ(α)) =

∪_{α∈S′(a)}τ(pr_{B}(α)) = p(S)(pr_{B}(a)) = p(S)(b). ▷◁

\underline{Az 1.) állitás igazolása}

Az állítás két összefüggés belátását kívánja. a.) D_{G} ⊂ D_{p(S)} igazolása.

Ez abból következik, hogy a feltételeink szerint a hasonló D_{G} ⊂ D_{p(S′)} fennáll, valamint abból, hogy pr_{B}(D_{p(S′)}) = D_{p(S)} és pr_{B}(D_{G}) = D_{G}.

b.) Tetszőleges b ∈ D_{G_{1}}-re p(S)(b) ⊂ G_{1}(b) kell, hogy teljesüljön. Ha b ∈ D_{G_{1}}, akkor ∃a ∈ D_{G}, amelyre pr_{B}(a) = b. A feltételek szerint S′ megoldása G-nek, így a ∈ D_{p(S′)} és p(S′)(a) ⊂ G(a). A lemmából következik, hogy pr_{B}(p(S′)(a)) = p(S)(pr_{B}(a)) = p(S)(b). Ezért p(S)(b) ⊂ pr_{B}(G(a)) ⊂ G_{1}(b). ▷◁

\underline{A 2.) állitás igazolása}

Az állítás két összefüggés belátását kívánja. a.) D_{F} ⊂ D_{p(S)} igazolása.

Mivel S_{1} megoldása F′-nek, fennáll D_{F′} ⊂ D_{p(S_{1})}. S_{1} és S ekvivalensek B-n, ezért pr_{B}(D_{p(S_{1})}) = D_{p(S)}. F′ az F feladat kiterjesztése, így pr_{B}(D_{F′}) = D_{F}. A felírt három összefüggésből már következik a bizonyítandó állítás.

b.) Be kell látni, hogy ∀b ∈ D_{F} : p(S)(b) ⊂ F (b). Írjuk fel, hogy mit jelent ebben a speciális esetben S_{1} és S ekvivalenciája. Tetszőlegesen rögzített b ∈ D_{F} esetén tekintsük mindazon a ∈ A pontokat, amelyekre pr_{B}(a) = b. Ekkor p(S)(b) = ∪_{pr_{B}(a)=b}pr_{B}(p(S_{1})(a)). Mivel S_{1} megoldása F′-nek ezért ∀a ∈ D_{F′} : p(S_{1})(a) ⊂ F′(a). Ezt felhasználva p(S)(b) = ∪_{pr_{B}(a)=b}pr_{B}(p(S)(a)) ⊂ ∪_{pr_{B}(a)=b}pr_{B}(F′(a)) = ∪_{pr_{B}(a)=b}F (pr_{B}(a)) = F (b). ▷◁

\underline{A 3.) állitás igazolása}

A lemma szerint S′ ekvivalens S-sel B-n. Másrészt nyilván pr_{B×B}(F′) = F (F′ éppen a legbővebb ilyen feladat). Ekkor alkalmazható egyik előző állításunk, mely szerint, ha S′ megoldása F′-nek, akkor S megoldása F -nek. a.) D_{F′} ⊂ D_{p(S)} igazolása.

Nyilván D_{p(S′)} = {a ∈ A|pr_{B}(a) ∈ D_{p(S)}} és D_{F′} = {a ∈ A|pr_{B}(a) ∈ D_{F} }. A feltétel szerint D_{F} ⊂ D_{p(S)}. Ezekből az összefüggésekből az állítás (pl. indirekt módon) könnyen belátható.

b.) Tekintsünk tetszőleges a ∈ D_{F′}-t. Legyen b = pr_{B}(a). Definíciónk alapján p(S′)(a) = {a′ ∈ A|pr_{B}(a′) ∈ p(S)(b) ∧ pr_{B}(a′) = pr_{B}(a)}, F′(a) = {a′ ∈ A|pr_{B}(a′) ∈ F (b)}. Mivel p(S)(b) ⊂ F (b), ezért az előzőkhöz hasonló módon adódik, hogy p(S′)(a) ⊂ F′(a). Mivel p(S′)(a) definíciójában a′-ra még további megszorítás is van, ezért általában p(S′)(a) ≠ F′(a). ▷◁

9 Leggyengébb előfeltétel

A leggyengébb előfeltétel Dijkstra-tól származó eredeti megfogalmazása: ”The condition that characterizes the set of all initial stets such that activation will certainly result in a properly terminating happening leaving the system in a final state satisfying a given post-condition is called ’the weakest pre-condition corresponding to that post-condition’”. Ennek a fogalomnak sokan sokféle definícióját fogalmazták meg (Wand, Guerreiro, Roever, Plotkin, Hehner stb.), illetve foglalkoztak ezek kapcsolataival. Mi most az eredeti definíció megfelelőjét fogalmaztuk meg a mi modellünk segíségével.

A leggyengébb előfeltétel kijelöli azt a legtágabb halmazt, aminek elemeire az S program biztosan terminál, és a végállapotra igaz R. Fontos észrevenni, hogy [lf(S, R)]-en kívül is lehetnek olyan pontjai az állapottérnek, amikből a program [R]-ben juthat, csak azokból nem biztos, hogy oda jut.

Definiálhatunk az lf(S, R)-nél gyengébb feltételt is, ami csak azt biztosítja, hogy ha a program valahova jut, azaz terminál, akkor ez csak [R]-ben lehet. Ezt a feltételt leggyengébb szabad előfeltételnek nevezzük:

[lf′(S, R)] ::= {a ∈ D_{p′(S)}|p′(S)(a) ⊂ [R]},

ahol p′(S) az szabad programfüggvény.

A leggyengébb korlátos előfeltételt a p_{k}(S) korlátos programfüggvény segítségével definiáljuk.

[lf_{k}(S, R)] ::= {a ∈ D_{p_{k}(S)}|p_{k}(S)(a) ⊂ [R]}.

Ha egy program leggyengébb előfeltételét minden A-beli részhalmazra megadjuk, akkor nyilván teljesen ismerjük a program viselkedését, hiszen ezzel a programfüggvényt is ismerjük. Valójában egy program viselkedését nem szükséges teljes egészében ismernünk, hanem csak bizonyos, céljainktól függő feltételek között.

Amikor programot készítünk, valamilyen célt akarunk elérni: azt, hogy a program valamilyen feltételeknek eleget tevő állapotban termináljon. Ha a program leggyengébb előfeltételét megadjuk a kedvező végállapotokat kijelölő feltételekre, akkor a számunkra fontos viselkedését ismerjük a programfüggvény megadása nélkül is.

10 A leggyengébb előfeltétel tulajdonságainak igazolása

\underline{Az a.) tulajdonság igazolása}

Tegyük fel, hogy létezik a ∈ A : a ∈ [lf(S, hamis)], azaz p(S)(a) ⊂ [hamis] = ∅. Ez pedig ellentmond annak, hogy a ∈ D_{p(S)} miatt a definíció szerint p(S)(a) ≠ ∅. ▷◁

\underline{Az b.) tulajdonság igazolása}

Legyen a ∈ [lf(S, Q)], azaz p(S)(a) ⊂ [Q]. Mivel [Q] ⊂ [R], ezért p(S)(a) ⊂ [R], azaz a ∈ [lf(S, R)]. ▷◁

\underline{A c.) tulajdonság igazolása}

[lf(S, Q)] ∩ [lf(S, R)] =
{a ∈ A|p(S)(a) ⊂ [Q]} ∩ {a ∈ A|p(S)(a) ⊂ [R]} =
{a ∈ A|p(S)(a) ⊂ [Q] ∧ p(S)(a) ⊂ [R]} =
{a ∈ A|p(S)(a) ⊂ [Q ∧ R]}.

▷◁

\underline{Az d.) tulajdonság igazolása}

[lf(S, Q)] ∪ [lf(S, R)] =
{a ∈ A|p(S)(a) ⊂ [Q]} ∪ {a ∈ A|p(S)(a) ⊂ [R]} =
{a ∈ A|p(S)(a) ⊂ [Q] ∨ p(S)(a) ⊂ [R]} ⊂
{a ∈ A|p(S)(a) ⊂ [Q ∨ R]}.

▷◁ Ha p(S) függvény, akkor itt is egyenlőség van.

11 A leggyengébb előfeltétel és a megoldás kapcsolata

\underline{Az a.) állitás igazolása} i.) A ⇒ eset igazolása.

Legyen S megoldása F -nek. Ez a következő két összefüggés fennállását jelenti:

- D_{F} ⊂ D_{p(S)},

- ∀a ∈ D_{F} : p(S)(a) ⊂ F (a). Ekkor tetszőleges a ∈ D_{F} -re fennáll, hogy a ∈ {a ∈ D_{F} |p(S)(a) ⊂ F (a)} = [lf(S, P(F (a)))].

ii.) A ⇐ eset igazolása.

Azt kell belátni, hogy az adott feltétel esetén S megoldása F -nek.

- Tetszőleges a ∈ D_{F} -re fennáll, hogy a ∈ [lf(S, P(F (a)))] ⊂ D_{p(S)}, azaz D_{F} ⊂ D_{p(S)}.

- Tetszőleges a ∈ D_{F} esetén a feltétel szerint a ∈ [lf(S, P(F (a)))] = {a ∈ D_{F} |p(S)(a) ⊂ F (a)}, p(S)(a) ⊂ F (a). ▷◁

\underline{A b.) állitás igazolása}

Az a.) pont állítása alapján ∀a ∈ D_{F} : a ∈ [lf(S, P(F (a)))] ⇔ ∀H ⊂ D_{F^{−1}} : F^{−1}(H) ⊂ [lf(S, P(H))]. i.) A ⇒ eset igazolása.

Legyen H ∈ D_{F^{−1}} tetszőleges. Tekintsük az F^{−1}(H) = {a ∈ A|a ∈ D_{F} ∧ F (a) = H} halmazt. Bármely a ∈ F^{−1}(H)-ra a feltétel szerint a ∈ [lf(S, P(F (a)))] = [lf(S, P(H))]. Következésképpen F^{−1} ⊂ [lf(S, P(H))].

ii.) A ⇐ eset igazolása. Legyen a ∈ D_{F} tetszőleges. Tekintsük azt a H ∈ D_{F^{−1}}-et, amelyre H = F (a). Ekkor nyilván a ∈ F^{−1}(H). A feltétel szerint F^{−1}(H) ⊂ [lf(S, P(H))] = [lf(S, P(F (a)))], a ∈ [lf(S, P(F (a)))]. ▷◁

12 A specifikáció tétele

Általában sok olyan program van, ami megoldása egy adott feladatnak. A programozás azt jelenti, hogy ezek közül legalább egyet előállítunk. Tehát a programozó nem az összes megoldó programra kíváncsi. Ezért számára nem fontos, hogy egy kritérium szükséges is legyen ahhoz, hogy a program megoldás legyen. A specifikáció tétele elégséges feltételt ad arra, hogy egy program megoldása legyen egy feladatnak.

\underline{A specifikáció tételének igazolása}

Minden a ∈ D_{F} -hez létezik olyan b ∈ B, hogy a ∈ [Q_{b}], és mivel [Q_{b}] ⊂ [lf(S, R_{b})], [Q_{b}] ⊂ D_{p(S)}, ezért a ∈ D_{p(S)}. Másrészt, ha a ∈ D_{F} és a ∈ [Q_{b}], akkor p(S)(a) ⊂ [R_{b}] és [R_{b}] ⊂ F (a), azaz p(S)(a) ⊂ F (a). ▷◁

Egy program feladatát a specifikáció tétele alapján Q_{b} ⇒ lf(S, R_{b}) (∀b ∈ B) formulával adjuk meg. A következő példában megmutatjuk, hogyan írjuk ezt fel változók segítségével.

\underline{P élda :} Legyen a feladat az, hogy határozzuk meg két szám maximumát.

A = Z × Z × Z, x, y, m : Z.
B = Z × Z, x′, y′ : Z.
Q_{x′,y′} = (x = x′ ∧ y = y′),
R_{x′,y′} = (m ≥ x′ ∧ m ≥ y′ ∧ (m = x′ ∨ m = y′)).

Ez a specifikáció azt jelenti, hogy olyan S programot kell keresni, amire ∀b ∈ Bre

x(a) = x′(b) ∧ y(a) = y′(b) ⇒
lf(S, m(a) ≥ x′(b) ∧ m(a) ≥ y′(b) ∧ (m(a) = x′(b) ∨ m(a) = y′(b))).

13 A specifikáció tétele nem megfordítható

A specifikáció tétele nem megfordítható, azaz van olyan F feladat, S program, B, F_{1} és F_{2}, hogy S megoldja a feladatot, de ∀b ∈ B : Q_{b} ⇒ lf(S, R_{b}) nem teljesül. A relációk alábbi megválasztásával erre mutatunk példát: A = {1, 2, 3}, B = {a, b}, F (1) = {1, 2}, F (2) = {1, 2, 3}, F (3) = {2, 3}, [Q_{a}] = {1, 2}, [R_{a}] = {1, 2}, [Q_{b}] = {2, 3}, [R_{b}] = {2, 3}, p(S)(1) = {1}, p(S)(2) = {1, 2, 3}, p(S)(3) = {2, 3}. És így nem teljesül, hogy [Q_{a}] ⊂ [lf(S, R_{a})].

14 Értékadás

Az értékadást általában változókkal írjuk fel. Ha x_{1}, …, x_{n} az állapottér változói, az a := F (a) programot

x_{1}, …, x_{n} := F_{1}(x_{1}, …, x_{n}), …, F_{n}(x_{1}, …, x_{n})

jelöli, kifejezve, hogy melyik változó ”hogyan változik”. Ha valamely i-re F_{i}(x_{1}, …, x_{n}) = x_{i} (és ez az esetek döntő többségében így van), akkor a jelölésből az x_{i}-t és F_{i}(X_{1}, …, x_{n})-t elhagyjuk. Ha így x_{k} := F_{k}(x_{1}, …, x_{n})-hez jutunk, akkor az értékadást egyszerűnek, egyébként szimultánnak nevezzük. Az is igen gyakori, hogy az F_{j} nem függ valójában minden x_{i}-től, ekkor tovább egyszerűsítjük a jelölést, és elhagyjuk a fölösleges x_{i}-ket.

Az egyszerű értékadásnak nagyon szemléletes jelentése van: felfoghatjuk, mint az állapottér egy tengelyén való mozgást.

Mivel az értékadás olyan program, aminek a programfüggvényét ismerjük, ezért ismerjük a leggyengébb előfeltételét is, s gyakran használjuk az alábbi jelölést:

lf(x_{k} := F_{k}(x_{1}, …, x_{n}), R) = R^{x_{k}←F_{k}(x_{1},...,x_{n})}.

Ha pedig az értékadás parciális, akkor a következőt:

lf(x_{k} := F_{k}(x_{1}, …, x_{n}), R) = F_{k}(x_{1}, …, x_{n}) ≠ ∅ ∧ R^{x_{k}←F_{k}(x_{1},...,x_{n})}.

15 Programok szekvenciája

A szekvencia olyan konstrukció, hogy ha mindkét komponense csupa véges sorozatból áll, akkor a szekvenciájuk is ilyen. Az is igaz, hogy determinisztikus programok szekvenciája is determinisztikus.

A szekvencia jelölése sruktogrammal:

S \frac{S1}{S2}

16 Elágazás

Az elágazás csupa determinisztikus programkomponens esetén is lehet nemdeterminisztikus, ha a feltételek igazsághalmazai nem diszjunktak. Az is lehet, hogy csupa véges sorozatból álló komponens esetén is tartalmaz végtelen (csupa azonos elemből álló) sorozatot is, hiszen a feltételek igazsághalmazainak úniója nem biztos, hogy kiadja az egész teret.

IF \frac{\ π_{1} \ π_{2} \ … \ π_{n}}{S_{1}  S_{2}  …  S_{n}}

IF \frac{\  π  /}{\begin{aligned}S_{1} \\ & S_{2} \end{aligned}}

17 Ciklus

A determinisztikus komponensből álló ciklus mindig determinisztikus, de véges komponens esetén is lehet a ciklus végtelen.

DO π ; \overline{S_{0}}

18 A szekvencia, az elágazás és a ciklus program

\underline{Bizonyitás}

A definíció mindhárom esetben kimondja, hogy mindegyik reláció, azaz része A × A-nak, és azt is, hogy a program b.) tulajdonsága (D_{S} = A) teljesül. Ellenőrizzük a többi feltétel teljesülését! a.) A szekvencia esetében, ha α ∈ S(a)(a ∈ A), akkor vagy α ∈ S_{1}(a), s ek-

kor nyilván teljesülnek a tulajdonságok, vagy α = χ(α_{1}, α_{2}), és ekkor a χ definíciója miatt teljesül c.), de α_{1} ∈ S_{1} miatt a.) is.

b.) Az elágazás esetében, mivel ∪_{i=1}^{n}w_{i}(a) és w(a) (ahol a ∈ A) nem lehet egyszerre üres, ezért vagy ∃i ∈ [1, n] : α ∈ S_{i}(a), vagy α = (a, a, a, …). Nyilván mindkét esetben mindegyik tulajdonság teljesül.

c.) A ciklus esetében, ha a ∉ [π], akkor triviális a teljesülés. Ha a ∈ [π], akkor S(a) nem lehet üres, mivel S program. Tehát létezik A^{∗∗}-beli sorozatoknak legalább egy olyan véges vagy végtelen α = (α_{1}, …) sorozata, ahol α_{1} ∈ S(a), és α_{i+1} ∈ S(τ(α_{i})). Másrészt minden ilyen tulajdonságú α = (α_{1}, …), α_{i} ∈ A sorozatra: vagy ∃i ∈ N : τ(α_{i}) ∈ [¬π], vagy nem. Ha egy sorozatra létezik ilyen i, akkor k legyen ezek közül a maximális. Ekkor χ_{k}(α_{1}, …, α_{k}) ∈ DO(a), és rendelkezik a c.) tulajdonsággal. Ha egy α sorozatra nem létezik ilyen i, akkor, ha α véges, azaz α = (α_{1}, …, α_{m}), a χ_{m}(α) ∈ DO(a). Ha α végtelen, a χ_{∞}(α) ∈ DO(a), és mindkét esetben a c.) pontnak megfelelő sorozatot kapunk. Tehát DO(a) nem üres, elemei rendelkeznek a c.) tulajdonsággal, és mivel α_{1} ∈ S(a), az a.)-val is. ▷◁

19 A programkonstrukciók programfüggvényei

\underline{A szekvenciára vonatkozó állitás bizonyitása}

Legyen (a, a′) ∈ A × A. (a, a′) ∈ p(S_{2}) ∘ p(S_{1}) akkor és csak akkor, ha ∃b ∈ A : (a, b) ∈ p(S_{1}) ∧ (b, a′) ∈ p(S_{2}), azaz S_{1}(a) ⊂ A^{∗}, és létezik α ∈ S_{1}(a), hogy S_{2}(τ(α)) ⊂ A^{∗} és létezik α′ ∈ S_{2}(τ(α)), amire τ(α′) = a′, vagyis (a, a′) ∈ p(S). ▷◁

\underline{Az elágazásra vonatkozó állitás bizonyitása}

Az elágazás definíciója szerint, egy a ∈ A pontban IF (a) ⊂ A^{∗} pontosan akkor, ha a-ra legalább egy π_{i} igaz, és ∪_{i=1}^{n}w_{i}(a) ⊂ A^{∗}. Ez nyilván teljesül, ha ∀i ∈ [1, n] : a ∈ [π_{j}] ⇒ a ∈ D_{p(S)}. Ekkor p(IF)(a) = τ(∪_{i=1}^{n}w_{i}(a)) = ∪_{i=1}^{n}pw_{i}(a). ▷◁

\underline{A ciklusra vonatkozó állitás bizonyitása}

Legyen a ∈ A. a ∈ D_{p(DO)} akkor és csak akkor, ha DO(a) ⊂ A^{∗}, azaz, ha DO(a) = {(a) ∈ A^{∗}|a ∉ [π]} ∪ {α ∈ A^{∗}|a ∈ [π] ∧ ∃n ∈ N : α = χ_{n}(α_{1}, …, α_{n}) ∧ α_{1} ∈ S_{0}(a) ∧ (∀i ∈ [1, n] : α_{i+1} ∈ S_{0}(τ(α_{i}))) ∧ τ(α_{i}) ∈ [π] ∧ τ(α_{n}) ∉ [π]}. És ez éppen a π-re vonatkozó lezárt definíciója. ▷◁

20 A szekvencia levezetési szabálya

\underline{Az állitás bizonyitása}

Ha q ∈ [Q], akkor 2. miatt p(S_{1})(q) ∈ Q′. De mivel 1. miatt minden q′ ∈ Q′- re p(S_{2})(q′ ⊂ [R], ezért p(S_{2}) ∘ p(S_{1})(q) ⊂ [R], azaz q ∈ [lf(S, R)]. ▷◁

21 Az elágazás levezetési szabálya

\underline{Az állitás bizonyitása}

Ha q ∈ Q, és létezik i, hogy q ∈ [π_{i}], akkor mivel minden i-re q ∈ [π_{i}]-ből következik, hogy q ∈ D_{p(S_{i})}, és p(S_{i})(q) ⊂ [R], ezért q ∈ D_{p(IF)} és p(IF)(q) ⊂ [R] is teljesül. ▷◁

22 A ciklus levezetési szabálya

\underline{Az állitás bizonyitása} Legyen q ∈ [Q]. Mivel [Q] ⊂ [P], ezért q ∈ [P] ∩ [¬π], vagy q ∈ [P] ∩ [π].

a) Legyen q ∈ [P] ∩ [¬π]. Ekkor a ciklus definíciója miatt p(DO)(q) = (q), ész a 2. miatt q ∈ [R], azaz q ∈ [lf(DO, R)].

b) Jelöljük g-vel p(S_{0}) leszűkítését [π]-re. Azaz g = p(S_{0}) ∩ ([π] × A). Legyen q ∈ [P] ∩ [π]. Ekkor q ∈ D_{p(S_{0})} a 4. pont miatt. Ha b ∈ g(q), akkor 4. miatt vagy b ∈ [P] ∩ [π], b ∈ [P] ∩ [¬π], azaz g(q) ⊂ ([P] ∩ [π]) ∪ ([P] ∩ [¬π]). Ha feltesszük, hogy valamely k-ra g^{(k)}(q) ⊂ ([P] ∩ [π]) ∪ ([P] ∩ [¬π]), akkor ha b ∈ g^{(k)}(q), vagy b ∈ [¬π] ∩ [P], és 2. miatt b ∈ [R], vagy b ∈ [P] ∩ [π], és akkor 4. miatt p(S_{0})(b) ⊂ ([P] ∩ [π]) ∪ ([P] ∩ [¬π]), azaz g^{(k+1)}(q) ⊂ ([P] ∩ [π]) ∪ ([P] ∩ [¬π]). Így g^{(k)}(q) ⊂ ([P] ∩ [π]) ∪ ([P] ∩ [¬π]) minden k-ra igaz. Másrészt, ha q ∈ [P] ∩ [π], akkor létezik n ≤ t(q), hogy g(q)^{(n)} ∈ [¬π]. Tegyük fel, hogy nem igaz az állítás. Mivel 5. miatt, ha b ∈ p(S_{0})(q), akkor t(b) < t(q) (hiszen t(q) ≤ t(q)−1+1 triviális fennállása alapján 5.- ből a t(b) ≤ t(q)−1 < t(q) állítást kapjuk), ezért (mivel a t függvénynek g^{(i)}(q)-n t(q) felső korlátja) max_{b∈g^{(k+1)}(q)}t(b) < max_{b∈g^{(k)}(q)}t(b), azaz max_{b∈g^{(t(q)+1)}(q)}t(b) < 0, ez pedig ellentmond a 3. feltételnek, tehát q ∈ D\overline{p(S_{0})|_{π}}, azaz D_{p(DO)} és p(DO)(q) ∈ [R] a 2. tulajdonság miatt. ▷◁ Miért nevezzük ezeket a tételeket levezetési szabályoknak? Az alapvető

kérdés minden programmal kapcsolatban az, hogy vajon megoldja-e az adott feladatot! Ez a kérdés a programkonstrukciókkal kapcsolatban is. A levezetési szabályokat megfogalmazó tételek lényege az, hogy ha a feltételeiknek megfelelő módon konstruálunk programot, akkor garantált, hogy azok megoldják a feladatot. Ha a tételek feltételeinek eleget tevő specifikációjú meghatározott feladatokat megoldó komponensekből indulunk ki, akkor az összetett program megoldja az eredeti feladatot.

Vegyük figyelembe, hogy a megoldandó feladatot a specifikáció tételének megfelelően a paramétertér segítségével adjuk meg Q_{b} és R_{b} elő- és utófeltételek formájában.

Így a szekvencia levezetési szabálya alapján azt mondjuk: ha S_{1} és S_{2} olyan programok, hogy a paramétertér minden elemére Q_{b} ⇒ lf(S_{1}, Q′_{b}), és Q′_{b} ⇒ lf(S_{2}, R_{b}), akkor (S_{1}; S_{2} megoldja a Q_{b}, R_{b} párokkal megadott feladatot.

Hasonlóan az elágazás esetén: ha minden b paraméterre, mindegyik S_{i} programra Q_{b} ∧ π_{i} ⇒ lf(S_{i}, R_{b}), akkor az IF = (π_{1} : S_{1}, …, π_{n} : S_{n}) program megoldja a feladatot, ha minden b-re ∃i : π_{i}.

Így újrafogalmazhatjuk — valamivel egyszerűbben — a ciklusra vonatkozó tételt is. Azaz: ha minden b ∈ B-re teljesülnek az

1. Q_{b} ⇒ P_{b},

2. P_{b} ∧ ¬π ⇒ R_{b},
3. P_{b} ∧ π ⇒ t_{b} > 0

feltételek, és S_{0} egy olyan program, amely megoldja a következő feladatot: Az állapottér az eredeti feladat állapottere, a változók szintén. A paramétertér legyen az eredeti bővítése, B′ = B × Z, és az új paraméterváltozót jelöljük t′-vel. Az elő- és utófeltételpárok: P_{b} ∧π ∧T′ = t, ill. P_{b} ∧ T′ > t.

akkor a ciklus megoldja az eredeti, Q_{b}, R_{b} feltételpárokkal megadott feladatot.

23 Direktszorzat és rekord típusok

A direktszorzat típusok legtöbbször rekordok is, de nem mindig. Példa egy nem rekord direktszorzatra a racionális számok. A racionális számokat definiálhatjuk egészek direktszorzataként úgy, hogy ha ((a, b), t), ((a′, b′), t′) ∈ R, akkor a ∗ b′ = a′ ∗ b.

24 Lineáris keresés

A feladat az, hogy az egész számok egy zárt intervallumán keressük meg a legkisebb adott tulajdonságú egész számot.

Ez a feladat valójában nagyon sok konkrét feladatot jelenthet. Például ilyenek ”az adott intervallumba eső legkisebb prímszám megkeresése”, ”két azonos értelmezési tartományú függvény típusú változó első eltérő elemének kijelölése” (azaz a közös értelmezési tartományból ki kell választani a legkisebb olyan elemet, aminek az a tulajdonsága, hogy a hozzá tartozó függvényértékek különbözők), vagy ”egy függvény típusú változónak melyik az első olyan helye, ahol a függvényérték az értékrészlet egy rögzített elemével egyenlő”. A példákat még sokáig lehetne sorolni. Az a közös bennük, amit a feladatban megfogalmaztunk.

Először egy nagyon egyszerű esetet vizsgálunk. Legyen β egy feltétel az A = Z állapottéren, és [m, n] ⊂ Z olyan zárt intervallum, amire [β] ∩ [m, n] ≠ ∅. Keressük meg a legkisebb i ∈ [m, n] ∩ [β] elemet !

Állapottérnek az A = Z × Z × Z -t választjuk, és a megfelelő változók m, n, i : Z. A paramétertér legyen B = Z × Z, és a változói m′, n′ : Z. A program specifikációja ezután a következő elő- és utófeltételekkel adódik:

\begin{matrix}Q_{m′,n′} = (m = m′ ∧ n = n′ ∧ [m, n] ∩ [β] ≠ ∅), \\ R_{m′,n′} = (Q_{m′,n′} ∧ i ∈ [m, n] ∧ β(i) ∧ ∀j ∈ [m, i − 1] : ¬β(j)) \end{matrix}

Az R állítást lényegében úgy foghatjuk föl, hogy az az [m, i] intervallum minden eleméről állít valamit. Az ilyen esetekben gyakran ciklus oldja meg a feladatot. Ezért most is ezzel próbálkozunk.

Ha ciklusra akarjuk levezetni a programot, akkor az első dolgunk egy invariáns tulajdonságot keresni. Az invariáns tulajdonságot mindig úgy próbáljuk meghatározni, hogy az utófeltételt mint speciális esetet kaphassuk meg belőle. Azt is mondjuk, hogy az invariáns tulajdonság az utófeltétel általánosítása, vagy más szóval gyöngítése.

R_{m′,n′} kézenfekvő gyöngítése, ha elhagyjuk a β(i) tényezőt. Válasszuk így az invariáns tulajdonságot:

P_{m′,n′} = (Q_{m′,n′} ∧ i ∈ [m, n] ∧ ∀j(m ≤ j < i) : ¬β(j)).

Ezután a ciklusra vonatkozó levezetési szabályban szereplő feltételek teljesülését biztosítjuk.

Az első, Q ⇒ P nem teljesül, ezért egy szekvenciává bontjuk először a programot.

S ::= (S_{1}; S_{2}),

ahol S_{1} specifikációja az előzőeknek megfelelően Q_{m′,n′} ⇒ lf(S_{1}, P_{m′,n′}) lesz. Most azt kell meggondolnunk, lehetséges-e P -t úgy specializálni, szűkíteni, hogy az (könnyen) teljesíthető legyen (S_{1} -el). A Q_{m′,n′} ∧ i = m állításból következik P_{m′,n′}. Ezért S_{1} specifikációja Q_{m′,n′} ⇒ lf(S, Q_{m′,n′} ∧ i = m) lehet. Mivel pedig tetszőleges R -re lf(i := m, R) = R^{i←m}, így lf(i := m, Q_{m′,n′} ∧ i = m) = (Q_{m′,n′} ∧ m = m) = Q_{m′,n′}, azaz azt kaptuk, hogy S_{1} ::= i := m.

Ezután vizsgáljuk a második feltétel teljesülését: P ∧¬π ⇒ R. Mivel P_{m′,n′}∧ β(i) = R_{m′,n′}, ezért π -nek ¬β(i) -t választva a második feltétel is teljesül, hiszen β -ról feltettük, hogy megengedett feltétel, a negáció pedig megengedett művelete a feltételek képzésének.

A harmadik feltétel teljesülését elérhetjük, ha t -nek (n − i) -t választjuk, hiszen egyrészt P_{m′,n′} -ből következik, hogy i ∈ [m, n], tehát i ≤ n, másrészt ¬β(i) miatt az egyenlőség sem teljesül.

Most már csak az van hátra, hogy olyan ciklusmagot válasszunk, amire teljesül a negyedik és az ötödik feltétel. A t függvény csökkentését elérhetjük az i := i+1 programmal, mert P_{m′,n′} ∧π ∧t ≤ t_{0} +1 ⇒ lf(i := i+1, t ≤ t_{0}) minden t_{0} értékre, mivel

lf(i := i + 1, t ≤ t_{0}) = (n − i ≤ t_{0})^{i←i+1} = (n − i − 1 ≤ t_{0}) = (n − i ≤ t_{0} + 1).

Másrészt

lf(i := i + 1, P_{m′,n′}) = P_{m′,n′}^{i←i+1} = Q_{m′,n′} ∧ i + 1 ∈ [m, n] ∧ ∀j ∈ [m, i] : ¬β(j) =

Q_{m′,n′} ∧ i + 1 ∈ [m, n] ∧ β(i) ∧ ∀j ∈ [m, i − 1] : ¬β(j).

Könnyen látható, hogy az első és a harmadik tényező közvetlenül adódik P_{m′,n′} -ből, a negyedik π -ből, a második P_{m′,n′} -ből (i ∈ [m, n] és ∀j ∈ [m, i] : ¬β(j)) és abból, hogy Q_{m′,n′} miatt i ≠ n. Tehát (GLO m : Z, V IR i : Z) az

i := m ; ¬β(i) ; \overline{i := i + 1}

programra és tetszőleges m′, n′ értékekre Q_{m′,n′} ⇒ lf(S, R_{m′,n′}), azaz S megoldás.

A kapott programra a lineáris keresés első változata néven fogunk hivatkozni. Azt is mondhatnánk, hogy most beláttuk a következő tételt : Az S program megoldása a keresési feladatnak.

Egy adott programról nagyon nehéz lenne eldönteni, hogy az megoldása-e valamilyen feladatnak. Ezért az állítást nem ilyen formában mondtuk ki, hanem bizonyítás, levezetés közben állítottuk elő a tételt.

Most egy kicsit általánosítjuk a feladatot, és nem kötjük meg, hogy β megengedett feltétel legyen. A programot az előző levezetéshez hasonlóan készítjük el, csak egy kicsit másképpen választjuk meg az invariáns tulajdonságot.

Legyen most az invariáns tulajdonság

\begin{matrix}P′_{m′,n′} = (Q_{m′,n′} ∧ m − 1 ≤ i ≤ n ∧ (∀j ∈ [m, i − 1] : ¬β(j))∧ \\ ¬l = ∀j ∈ [m, i] : ¬β(j)). \end{matrix}

A változás az eredeti invariáns tulajdonsághoz képest annyi, hogy a második állításban nem követeljük meg, hogy i ≥ m is teljesüljön, és kiegészítettük egy negyedik tényezővel. Most az S_{1} ::= i, l := m − 1, ↓ választással biztosíthatjuk P′_{m′,n′} teljesülését.

Mivel P′_{m′,n′} ∧ l ⇒ R_{m′,n′}, ezért ciklusfeltételnek ¬l választható. A termináló függvény ugyanaz, mint az előbb. A ciklusmagot gyakran állítjuk elő mint szekvenciát. A szekvencia egyik tagjától azt várjuk, hogy csökkentse a termináló függvény értékét, a másiktól pedig azt, hogy biztosítsa az invariáns tulajdonság megmaradását. Mivel sokszor fordul elő, hogy a termináló függvény csökkentése nagyon egyszerű programmal elvégezhető, ezért az itt bemutatott eljárás nagyon gyakran használható.

Legyen S_{3} ::= (S′_{3}; S′′_{3}). Mint az előzőekben már láttuk, az i := i+1 program csökkenti t -t, ezért S′′_{3} -at így választjuk meg. Ekkor

lf(i := i + 1, P′_{m′,n′}) = P_{m′,n′}^{′i←i+1} =

Q_{m′,n′} ∧ i + 1 ∈ [m − 1, n] ∧ (∀j ∈ [m, i − 1] : ¬β(j)) ∧ ¬β(i)∧

¬l = ((∀j ∈ [m, i] : ¬β(j)) ∧ ¬β(i + 1)) =

Q_{m′,n′} ∧ i + 1 ∈ [m − 1, n] ∧ ∀j ∈ [m, i] : ¬β(j) ∧ ¬l = ¬β(i + 1).

Jelöljük a jobboldalt R′ -vel. Így az S′_{3} programra a következő kikötést kaptuk :

P′_{m′,n′} ∧ ¬l ∧ t = t_{0} ⇒ lf(S′_{3}, R′ ∧ t = t_{0}).

Legyen S′_{3} ::= l := β(i + 1). Ekkor

\begin{matrix}lf(S′_{3}, R′ ∧ t = t_{0}) = Q_{m′,n′} ∧ i + 1 ≤ n ∧ (∀j ∈ [m, i] : ¬β(j))∧ \\ ¬β(i + 1) = ¬β(i + 1) ∧ n − i = t_{0}, \end{matrix}

ez pedig következik P_{m′,n′} ∧ ¬l ∧ t = t_{0} -ból, mert Q_{m′,n′} tényezője P_{m′,n′} - nek, P_{m′,n′} ∧¬l ∧Q_{m′,n′} miatt i < n, a harmadik tényező következik P_{m′,n′} ∧¬l - ből, a negyedik azonosan igaz, az ötödik azonos t = t_{0} -al. Tehát (GLO m : Z, V IR i : Z, LOC l : L) a programunk

i, l := m − 1, ↓ ; ¬l ; \overline{\frac{l := β(i + 1)}{i := i + 1}}

Ezt az eredményt nevezzük a lineáris keresés második változatának.

További általánosítása a feladatnak, ha nem tesszük fel, hogy létezik a keresett tulajdonságú érték. Ilyenkor kezelhetjük a problémát úgy, hogy a keresett tulajdonságot kiegészítjük egy alkalmasan választott másik tulajdonsággal, amelyről tudjuk, hogy a szóbanforgó intervallumon valamikor teljesül.

Tegyük fel, hogy β = γ ∨ δ, és [δ] ∩ [m, n] ≠ ∅. Keressük meg a legkisebb i ∈ [m, n] ∩ [β] elemet, és mondjuk meg azt is, hogy γ(i) igaz-e ! Nagyon gyakori a δ(i) ::= (i = n) választás.

Az állapotteret A = Z × Z × Z × L -nek választjuk, a változók rendre m, n, i, u. A paramétertér — mint az előzőekben — B = Z × Z, a paraméterváltozók m′, n′.

Q_{m′,n′} = (m = m′ ∧ n = n′ ∧ [m, n] ∩ [δ] ≠ ∅),

R_{m′,n′} = (Q_{m′,n′} ∧ u = (∃j ∈ [m, n] : γ(j) ∧ ∀k ∈ [m, j − 1] : ¬δ(k))∧ u ⇒ (i ∈ [m, n] ∧ γ(i) ∧ ∀j ∈ [m, i − 1] : ¬γ(j)).

Az előző levezetéshez hasonlóan ciklussal próbálkozunk. Bővítsük az állapotteret egy új L komponenssel és legyen v : L lokális változó.

\begin{matrix}P_{m′,n′} = (Q_{m′,n′} ∧ i ≤ n ∧ ¬u = ∀j ∈ [m, i] : ¬γ(j)∧ \\ ¬v = ∀j ∈ [m, i] : ¬δ(j) ∧ ∀j ∈ [m, i − 1] : ¬β(j)) \end{matrix}

Az i, u, v := m − 1, ↓, ↓ program garantálja hogy P_{m′,n′} teljesül. Erről helyettesítések után könnyen meggyőződhetünk.

A P_{m′,n′} ∧ ¬(¬u ∧ ¬v) = P_{m′,n′} ∧ (u ∨ v) -ből következik R_{m′,n′}. Ugyanis, ha u igaz, akkor γ(i) ∧ i ∈ [m, n], az invariáns tulajdonság utolsó része miatt pedig minden i -nél kisebb j -re γ(j) és δ(j) is hamis. Ha u hamis, akkor — π hamis volta miatt — v igaz, következésképpen δ(i) is az. Így valóban nincs olyan j, amire γ igaz és minden kisebb k -ra δ hamis. Tehát a ciklusfeltétel

¬u ∧ ¬v.

Termináló függvénynek a t = n − i most is megfelel, a csökkentésére ugyancsak jó az i := i+1 program. A P_{m′,n′} ∧(¬u∧¬v)∧(t = t_{0}) ⇒ lf(S, P_{m′,n′}^{i←i+1} ∧t = t_{0}) követelményt az

u, v := γ(i + 1), δ(i + 1)

értékadás kielégíti, erről a helyettesítések elvégzése után könnyen meggyőződhetünk. Tehát a program a következő (GLO m : Z, V IR i : Z, u : L, LOC v : L) :

i, u, v := m − 1, ↓, ↓ ; ¬u ∧ ¬v ; \overline{\frac{u, v := γ(i + 1), δ(i + 1)}{i := i + 1}}

Ezt a programot nevezzük a lineáris keresés harmadik változatának. Jelentősége abban van, hogy elég általánosan oldja meg a feladott problémát. Alkalmas például akkor is a keresésre, ha nem biztos, hogy található az adott intervallumban a keresett tulajdonságú érték. Ha γ -nak a keresett tulajdonságot választjuk és δ(i) = (i = n), a harmadik változat megoldja a feladatot.

A program azonban ennél általánosabban is használható. Például olyan feladatok megoldására, mint hogy ”keressünk egy adott prímszámnál kisebb olyan számot, aminek legalább három prímosztója van”.

Még egy nagyon fontos észrevételt teszünk a feladattal kapcsolatban, ami azonban nem csak rá vonatkozik.

A β állításról az mondtuk, hogy az az egész számokra vonatkozik. Ezonban nem zárja ki, hogy β tetszőleges típusú változóktól függjön. Ha az (x_{1}, ..., x_{n}, i) változóktól függ, a Q előfeltételt kiegészítjük az x_{1} = x′_{1}∧...∧x_{n} = x′_{n} állításokkal, ahol x′_{i} -k a megfelelő paraméterváltozók. Mivel R = (Q ∧ ...) volt, ezért ezek az állítások R -ben is szerepelnek. Ilyenkor β paraméterezett állításnak tekinthető.

25 Logaritmikus keresés

Legyen H egy olyan halmaz, amin értelmezve van egy rendezési reláció. Legyen f : Z → H monoton növekedő függvény. A feladat az, hogy eldöntsük egy adott h ∈ H értékről, hogy felveszi-e azt az f függvény egy adott [m, n] ⊂ Z intervallumon, és ha igen, akkor adjuk meg egy olyan pontját, ahol a függvényérték h.

Az állapottér legyen A = Z ×Z ×Z ×H ×L, a megfelelő változók m, n, i, h, l. A paramétertér B = Z × Z × H, a paraméterváltozók m′, n′, h′. Az elő- és utófeltételek

\begin{matrix}Q_{m′,n′,h′} = (m = m′ ∧ n = n′ ∧ h = h′ ∧ ∀k, j ∈ Z : k ≤ j ⇒ f(k) ≤ f(j)), \\ R_{m′,n′,h′} = (Q_{m′,n′,h′} ∧ l = (∀j ∈ [m, n] : f(j) = h) ∧ l ⇒ f(i) = h). \end{matrix}

A feladatot megoldhatnánk mint lineáris keresési feladatot, ha γ(i) ::= (f(i) = h) és δ(i) ::= (i = n). Ez a megoldási út járható, de nem célszerű, mert nem veszi figyelembe a függvény monotonitását, pedig ennek a tulajdonságnak a kihasználása jobb programhoz vezet. A jobb itt most azt jelenti, hogy kevesebb lépésben találja meg a keresett elemet. (Megjegyzés. Az, hogy két program közül melyik a jobb, nagyon bonyolult kérdés, és a jelenlegi ismeretek alapján nem is tudunk rá válaszolni. Bizonyos körülmények között lehet az a program jobb, ami más feltételek mellett rosszabb volt.)

A ciklus invariáns tulajdonsága a lineáris keresésnél az volt, hogy a keresett elem biztosan nincs az [m, i] intervallumban. Hasonló meggondolással próbálkozunk most is:

\begin{matrix}P_{m′,n′,h′} = (Q_{m′,n′,h′} ∧ [u, v] ⊂ [m, n] ∧ ∀j ∈ [m, n] − [u, v] : f(j) ≠ h \\ ∧ l = (i ∈ [u, v] ∧ f(i) = h)). \end{matrix}

Az u, v, i, l := m, n, m − 1, ↓ értékadás után P_{m′,n′} nyilvánvalóan igaz.

P_{m′,n′} ∧ l -ből következik R_{m′,n′}, mert f(i) = h ∧ i ∈ [m, n]. Ha l hamis, akkor ahhoz, hogy R_{m′,n′} következzen P_{m′,n′} -ből még az szükséges, hogy az [u, v] intervallum üres legyen, hiszen a ∀j ∈ [m, n] − [u, v] : f(j) ≠ h az R_{m′,n′} második állításának jobb oldaláról mondja ki, hogy hamis. Tehát a ciklusfeltétel: ¬(l ∨ u > v) = ¬l ∧ u ≤ v.

Termináló függvénynek a még vizsgálandó intervallum hosszát választjuk:

t = \{ \begin{matrix}u − v + 1, & ha ¬l \\ 0, & ha l \end{matrix} A ciklusfeltételből következik, hogy t > 0.

A következő feladatunk a t, azaz az [u, v] intervallum hosszának csökkentése. Ha most u -t növelnénk eggyel, a lineáris kereséshez jutnánk. Kihasználva az f függvény monotonitását azt mondhatjuk, hogy ha vesszük az [u, v] intervallum bármely x pontját, akkor vagy f(x) = h, és akkor minden rendben van, vagy f(x) < h, és akkor csak [x + 1, v] -ben lehet a keresett pont, vagy f(x) > h, és akkor csak [u, x − 1] -ben lehet a keresett pont.

Ezért a ciklusmagot most egy olyan S_{1}; S_{2} szekvenciának választjuk, ahol S_{1} utófeltétele a következő Q′ állítás:

Q′ = (Q ∧ [u, v] ⊂ [m, n] ∧ ∀j ∈ [m, n] − [u, v] : f(j) ≠ h ∧ ¬l ∧ u ≤ v ∧ i ∈ [u, v]).

Ekkor Q′ ∧ f(i) = h ⇒ lf(l :=↑, P_{m′,n′}) = P_{m′,n′}^{l←↑} nyilvánvalóan teljesül, Q′ ∧ f(i) < h ⇒ lf(u := i + 1, P_{m′,n′}) és Q′ ∧ f(i) > h ⇒ lf(v := i − 1, P_{m′,n′}) mivel i belső pontja volt [u, v] -nek, szintén teljesül. Ha S_{1} - nek i := [(u + v)/2] -t választjuk, akkor P_{m′,n′} ∧ π ⇒ lf(S_{1}, Q′), amiről helyettesítéssel meggyőződhetünk. Mivel S_{1} nem változtatja sem u -t, sem v -t sem l - et, ezért a termináló függvényt sem. Az l :=↑, u := i + 1 és v := i − 1 programok — mivel i belső pont — egyaránt csökkentik t -t. Tehát (GLO m, n : Z, GLO h : H, V IR l : L, i : Z, LOC u, v : Z) az

u, v, i, l := m, n, m − 1, ↓ ; ¬l ∧ (u ≤ v) ; \overline{i := [(u + v)/2] ; \ f(i) < h \ f(i) > h \ f(i) = h ; u := i + 1  v := i − 1  l :=↑}

program megoldása a feladatnak.

Megjegyezzük, hogy az i := [(u+v)/2] helyett bármilyen i :∈ [u, v] program is megfelelne. Ez a választás csökkenti a leggyorsabban az intervallum hosszát. Ha lineárisan keresünk, a vizsgálatok átlagos száma az elemek számával, logaritmikus keresés esetén az elemek számának logaritmusával arányos. Innen erednek az elnevezések.

26 Maximumkeresés

Legyen H egy tetszőleges rendezett halmaz és f : Z → H egy függvény. Feladatunk az, hogy egy adott [u, v] ⊂ Z intervallumban keressük meg az f függvény maximumát és egy olyan helyét, ahol ezt a maximumértéket felveszi.

Az állapottér A = H × Z × Z × Z, a megfelelő változók m : H, u, v, i : Z. A paramétertér B = Z × Z és a változói u′, v′ : Z. Az elő- és utófeltételek:

\begin{matrix}Q_{u′,v′} = (u = u′ ∧ v = v′), \\ R_{u′,v′} = (Q_{u′,v′} ∧ i ∈ [u, v] ∧ m = f(i) ∧ ∀j ∈ [u, v] : f(j) ≤ f(i)). \end{matrix}

A második és harmadik tényező azt jelenti, hogy i maximumhely [u, v] - ben, a negyedik pedig azt, hogy m a maximum értéke.

Az előző feladatokhoz hasonlóan gondolkodunk: nem követeljük meg, hogy m az egész [u, v] intervallumon maximum legyen, hanem annak csak egy részén. Azaz ismét ciklussal próbálkozunk, ahol az invariáns tulajdonság:

P_{m′,n′} = (Q_{u′,v′} ∧ k ∈ [u, v] ∧ i ∈ [u, k] ∧ m = f(i) ∧ ∀j ∈ [u, k] : f(j) ≤ f(i)).

Az invariáns tulajdonság teljesülése az i, k, m := u, u, f(u) programmal elérhető. P_{m′,n′} ∧ k = v ⇒ R_{m′,n′}, ezért a ciklusfeltétel k ≠ v. Ha termináló függvénynek v − k -t választjuk, P_{m′,n′} ∧ k ≠ v -ből következik, hogy v − k pozitív; t csökkentésére a k := k + 1 program alkalmas.

Az

\begin{matrix}lf(k := k + 1, P_{m′,n′}) = (Q_{u′,v′} ∧ k + 1 ∈ [u, v] ∧ m = f(i) ∧ f(k + 1) ≤ f(i)∧ \\ ∀j ∈ [u, k] : f(j) ≤ f(i)) \end{matrix}

feltétel teljesülését kell még biztosítani. Jelöljük a jobboldalt Q′ -vel.

Mivel P_{m′,n′} ∧ k ≠ v, ezért Q′ első három tényező közvetlenül következik, csak a másik kettővel kell foglalkozni. Ha f(k + 1) ≤ f(i), akkor Q′ teljes egészében igaz, ha nem , akkor az i, m := k + 1, f(k + 1) program biztosítja a teljesülését. Ezek a programok t értékét nem változtatják, ezért a megoldó program (GLO u, v : Z, V IR i : Z, m : H, LOC k : Z)

i, k, m := u, u, f(u) ; k ≠ v ; \overline{\  m < f(k + 1)  / ; \begin{aligned}i, m := k + 1, f(k + 1) \\ & SKIP \end{aligned} ; k := k + 1}

27 Adott tulajdonsággal rendelkező elemek megszámolása

Legyen β egy az egész számokon értelmezett logikai függvény. A feladat az, hogy számoljuk meg, hány helyen igaz β az [m, n] ⊂ Z intervallumban.

Az állapottér legyen A = Z × Z × N_{0}, a változók m, n : Z, s : N_{0}. A paramétertér B = Z × Z, a változói m′, n′ : Z. Az elő- és utófeltételek

\begin{matrix}Q_{m′,n′} = (m = m′ ∧ n = n′), \\ R_{m′,n′} = (Q_{m′,n′} ∧ s = ∑_{i=m}^{n} χ(β(i))), \end{matrix}

ahol χ : L → N_{0}, χ(↑) = 1, χ(↓) = 0.

Kézenfekvő, hogy a megoldásra ciklussal próbálkozzunk. Az R_{m′,n′} -ben s az összes [m, n] -beli igaz helyek számát jelenti. Ennél kevesebbet mondunk ki invariáns tulajdonságnak: csak [m, n] egy részére legyen igaz az állítás.

P_{m′,n′} = (Q_{m′,n′} ∧ k ≤ n ∧ s = ∑_{i=m}^{k} χ(β(i))).

Nyilván, ha k < m, akkor s = 0, ezért a k, s := m − 1, 0 program biztosítja P_{m′,n′} teljesülését.

A ciklusfeltétel k ≠ n, mivel P_{m′,n′} ∧ k = n ⇒ R_{m′,n′}. Termináló függvénynek n − k megfelel, mert k ≤ n ∧ k ≠ n miatt n − k pozitív. Csökkentése a szokásos módon, a k := k + 1 programmal történik.

Most már csak a P_{m′,n′}^{k←k+1} állítás teljesülését kell elérni.

P_{m′,n′}^{k←k+1} = (Q_{m′,n′} ∧ k + 1 ≤ n ∧ s = χ(β(k + 1)) + ∑_{i=m}^{k} χ(β(i)))

P_{m′,n′} ∧ k ≠ n -ből az első két tényező következik, és ha β(k + 1) hamis, a harmadik is. Ha β(k+1) igaz, az s := s+1 program biztosítja a harmadik tényező teljesülését. Tehát a program (GLO m, n : Z, V IR s : N_{0}, LOC k : Z):

k, s := m − 1, 0 ; k ≠ n ; \overline{\  β(k + 1)  / ; \begin{aligned}s := s + 1 \\ & SKIP \end{aligned} ; k := k + 1}

28 Rendezés

Legyen T tetszőleges rendezett típus, és X = seq(T), legyen továbbá x : X. Rendezzük át az x sorozatot úgy, hogy az elemei növekedő sorrendben legyenek.

Az állapottér A = X, a változó x : X. A paramétertér B = X, a változó x′. Az elő- és utófeltételek

\begin{matrix}Q_{x′} = (x = x′), \\ R_{x′} = (x ∈ perm(x′) ∧ (∀i, j ∈ [1, x.dom] : i ≤ j ⇒ x_{i} ≤ x_{j})) \end{matrix}

Definiálunk két logikai függvényt a további állítások egyszerűbb leírásához.

\begin{matrix}ρ(x, i, j) = (∀k, l(i < k < l ≤ j) : x_{k} ≤ x_{l}), \\ μ(x, i, j) = (∀k, l(1 ≤ k ≤ i < l ≤ j) : x_{k} ≤ x_{l}) \end{matrix}

A ρ jelentése szavakban: az x_{i}-nél nagyobb indexű elemei j -ig rendezettek. A μ jelentése: az x -ben i -ig kisebb elemek vannak, mint i -től j -ig. ρ segítségével ismét felírjuk R -et:

R_{x′} = (x ∈ perm(x′) ∧ ρ(x, 0, x.dom))

Ezután foglalkozunk a feladattal. A megoldás alapötlete az, hogy a sorozatot két szeletre bontjuk úgy, hogy az egyik szelet növekvően rendezett legyen, a másik szelet elemei pedig nem nagyobbak a rendezett szelet elemeinél.

Ezt fejezi ki a P invariáns tulajdonság:

P_{x′} = (x ∈ perm(x′) ∧ 0 ≤ k ≤ x.dom ∧ ρ(x, k, x.dom) ∧ μ(x, k, x.dom)).

Mivel k = x.dom esetén P_{x′} igaz, ezért P_{x′} teljesülését a k := x.dom program biztosítja. A ciklusfeltétel k ≠ 0, mert P_{x′} ∧ k = 0 ⇒ R_{x′}. Mivel P_{x′} ∧ k ≠ 0 esetén k pozitív, k -t választjuk termináló függvénynek.

A ciklusmagot egy szekvenciaként állítjuk elő. A rendezetlen részből egy új rendezett szeletet állítunk elő, és ezt csatlakoztatjuk a rendezett szelethez. Legyen

Q′ = (ρ(x, m, k) ∧ μ(x, m, k) ∧ (0 ≤ m < k ≤ x.dom) ∧ P_{x′}).

Ha P_{x′} ∧ k ≠ 0 ⇒ lf(”UJSZELET ”, Q′), akkor az (GLO x : X, LOC l, m : N_{0})

k := x.dom ; k ≠ 0 ; \overline{\frac{UJSZELET}{k := m}}

program megoldás, mert m < k miatt t csökken, és P_{x′}^{k←m} következik Q′ -ből.

Az ”UJSZELET” program is ciklus lesz. ”Elengedjük” Q′ -ből azt, hogy az új szelet vége k, azaz, hogy csatlakozik a rendezett részhez:

P′ = (ρ(x, m, l) ∧ μ(x, m, l) ∧ m < l ∧ 1 ≤ l ≤ k ∧ P_{x′})

Az m, l := 0, 1 programra P_{x′} ∧ k ≠ 0 ⇒ lf(m, l := 0, 1, P′), ami a helyettesítés után nyilvánvaló. Mivel P′ ∧ l = k ⇒ Q′, ezért a ciklusfeltétel l ≠ k. Termináló függvénynek így k − l választható, amit az l := l + 1 programmal csökkenthetünk. Ekkor

P^{′l←l+1} = (ρ(x, m, l + 1) ∧ μ(x, m, l + 1) ∧ m < l + 1 ∧ 1 ≤ l + 1 ≤ k ∧ P_{x′}).

Az utolsó állítás benne van P′ -ben, az utolsó előtti a ciklusfeltétel miatt teljesül, és m < l miatt m < l + 1. Ezért csak az első két állítás teljesüléséről kell gondoskodni. Ha x_{l+1} ≥ x_{l}, akkor nyilván ρ(x, m, l + 1) és μ(x, m, l + 1) is igaz, ha ρ(x, m, l) és μ(x, m, l) igaz volt. Ha x_{l+1} < x_{l}, az m, x_{l}, x_{l+1} := l, x_{l+1}, x_{l} program után ρ(x, m, l + 1) és μ(x, m, l + 1) igaz, m < l + 1 is teljesül, és P_{x′} is igaz marad, mert l + 1 ≤ k és x ∈ perm(x′). Tehát az ”UJSZELET” program a következő (GLO x : X, k : N_{0}, V IR m : N_{0}, LOC l : N):

UJSZELET m, l := 0, 1 ; l ≠ k ; \overline{\  x_{l+1} < x_{l}  / ; \begin{aligned}m, x_{l}, x_{l+1} := l, x_{l+1}, x_{l} \\ & SKIP \end{aligned} ; l := l + 1}

Ezzel kaptunk egy olyan programot, amelyik rendezi a sorozatot. Azonban más megoldó program is lehetséges. A logaritmikus keresést azért hoztuk létre, mert kihasználva a függvény monotonitását, a lineáris keresésnél bizonyos tekintetben jobb — kevesebb lépésben jut végállapotba — programot készítettünk.

A rendezés esetében is próbálkozhatunk jobb program készítésével.

A program elkészítésének alapgondolata most is nagyon egyszerű: a rendezett és rendezetlen részből álló sorozatban a rendezett rész hosszát növeljük, mégpedig úgy, hogy a rendezetlen rész első eleme kerüljön át a rendezett részbe.

Tehát az invariáns tulajdonság

P_{x′} = (ρ(x, 0, l) ∧ 1 ≤ l ≤ x.dom ∧ x ∈ perm(x′)).

Ez az állítás teljesül az l := 1 program után. Mivel P_{x′} ∧ l = x.dom ⇒ R, ezért a ciklusfeltétel l ≠ x.dom. A termináló függvény x.dom − l, ami P_{x′} ∧ l ≠ x.dom miatt pozitív, és az l := l+1 program csökkenti. Most a P_{x′} ∧l ≠ x.dom ⇒ lf(S_{1}, P_{x′}^{l←l+1}) programot kell elkészíteni, ahol P_{x′}^{l←l+1} = (ρ(x, 0, l + 1) ∧ 1 ≤ l + 1 ≤ x.dom ∧ x ∈ perm(x′)). A ciklusfeltétel miatt l + 1 ≤ x.dom. Az S_{1} program legyen szintén ciklus P′ invariáns tulajdonsággal:

P′ = ((0 ≤ k ≤ l) ∧ ρ(x, 0, k) ∧ μ(x, k, l + 1) ∧ x ∈ perm(x′)).

Ha k = l, a P′ következik P_{x′} -ből. Ezért a k := l program garantálja P′ teljesülését.

Mivel P′ ∧ (k = 0 ∨ x_{k+1} ≥ x_{k}) ⇒ ρ(x, 0, l + 1) ∧ x ∈ perm(x′), ezért a ciklusfeltétel k ≠ 0 ∧ x_{k+1} < x_{k}. A termináló függvény k, csökkentése a k := k − 1 programmal történik. A p^{′k←k+1} teljesülését az x_{k}, x_{k+1} := x_{k+1}, x_{k} program garantálja. Tehát a teljes program (GLO x : X, LOC l : N_{0}):

l := 1 ; l ≠ x.dom ; \overline{\frac{S1}{l := l + 1}}

S1 k := l ; k ≠ 0 ∧ x_{k+1} < x_{k} ; \overline{\frac{x_{k}, x_{k+1} := x_{k+1}, x_{k}}{k := k − 1}}

Ez a program lényegében egyenértékű az előző változattal, azonban az x_{k}, x_{k+1} := x_{k+1}, x_{k} program helyett kevesebb műveletet igénylő programot is választhatunk, ugyanis a legtöbb jelenlegi gép ún. szekvenciális gép, és a fenti szimultán értékadás csak három egyszerű értékadással valósítható meg.

A P′ helyett válasszunk egy olyan P′′ invariáns tulajdonságot, amiben nem követeljük meg az x ∈ perm(x′) teljesülését, csak azt, hogy kon((x_{1}, ..., x_{k}), (e), (x_{k+2}, ..., x_{x.dom}) ∈ perm(x′). Ekkor az e, k := x_{l+1}, l program biztosítja P′′ teljesülését, a ciklusfeltétel pedig k ≠ 0 ∧ e < x_{k} , a ciklusmag pedig x_{k+1} := x_{k}; k := k + 1 lesz. Az x_{k+1} := e után teljesül P^{l←l+1} . Azaz (GLO x : X, l : N , LOC k : N , e : T_{0})

S1′ k, e := l, x_{k+1} ; k ≠ 0 ∧ e < x_{k} ; \overline{{x_{k+1} := x_{k} \atop k := k − 1}} ; x_{k+1} := e

Ez a program már olcsóbb műveleteket tartalmaz mint az előző, gyorsabban hajtódik végre a szekvenciális gépen.

Vajon ez már az ideális program? Korántsem. Ennek vizsgálata azonban már egy más tárgy feladata.

29 Elemenkénti feldolgozás — első változat

Először a legegyszerűbb esettel foglalkozunk, amikor a leképezés egyváltozós egyértékű függvény. Ezt a továbbiakban

z = f(x)

típusú feladatnak nevezzük.

Legyen tehát f : X → Y, X, Y ⊂ 2^{H} függvény. Az állapottér A = A_{1} × A_{2}, ahol A1 = set(H_{1}), A_{2} = set(H_{2}), H_{1} ⊂ H, H_{2} ⊂ H. A változók legyenek x : A_{1}, z : A_{2}. A paramétertér B = A_{1}, változója x′ : A_{1}, az elő- és utófeltételek

\begin{matrix}Q_{x′} = (x = x′), \\ R_{x′} = (z = f(x′)) \end{matrix}

Kihasználva f elemenkénti feldolgozhatóságát, programunk egy ciklus lesz a

P = (z ∪ f(x) = f(x′) ∧ z ∩ f(x) = ∅)

invariáns tulajdonsággal.

Az z := ∅ program után P teljesül. Ciklusfeltételnek választható x ≠ ∅ is, de f(x) ≠ ∅ is, mivel P ∧ f(x) = ∅ ⇒ R, és x = ∅ ⇒ f(x) = ∅ az elemenkénti feldolgozhatóság miatt. A célszerűbb f(x) ≠ ∅ mellett maradunk, ha az primitív feltétel. Termináló függvénynek x.dom megfelel, hiszen x nem lehet üres a ciklusfeltétel miatt.

A ciklusmag x egy elemének kiválasztásából és ennek feldolgozásából áll, azaz egy S_{1}; S_{2} szekvencia lesz. A közbülső Q′ állítás legyen

Q′ = (P ∧ e ∈ x).

Ez az S_{1} ::= e : mem(x) programmal elérhető, hiszen

lf(S_{1}, Q′) = (x ≠ ∅ ∧ s ∈ x ⇒ P^{e←s} ∧ s ∈ x),

ez pedig következik P ∧ f(x) ≠ ∅ -ból. Az S_{2} program is egy szekvencia: x := x ˜−{e} csökkenti a t -t, ekkor

\begin{matrix}Q′′ = lf(x := x ˜−\{e\}, P) = \\ ((z ∪ f(x ˜−\{e\}) = f(x′) ∧ z ∩ f(x ˜−\{e\}) = ∅ ∧ x ∩ \{e\} ≠ ∅), \end{matrix}

és

lf(z := z˜∪f({e}), Q′′) =

z ∪ f({e}) ∪ f(x ˜−{e}) = f(x′) ∧ z ∪ f({e}) ∩ f(x ˜−{e}) =
∅ ∧ x ∩ {e} ≠ ∅ ∧ z ∩ f({e}) = ∅).

Ez pedig Q′ -ből következik, mert e ∈ x és f elemenkénti feldolgozhatósága miatt f({e}) ∪ f(x ˜−{e}) = f(x) és f({e}) ∩ f(x ˜−{e}) = ∅. Ezért csak azt kell belátni, hogy z ∩ f({e}) = ∅ és z ∩ f(x ˜−{e}) = ∅ is teljesül. Mivel azonban P - ben z ∩ f(x) = ∅ és f({e}) és f(x ˜−{e}) is része f(x) -nek, ezért metszetük z - nal üres. Tehát az z = f(x) feladatot megoldó program (GLO x : A_{1}, V IR z : A_{2}, LOC e_{1} : H):

z := ∅ ; f(x) ≠ ∅ ; \overline{e : mem(x) ; z := z˜∪f(\{e\}) ; x := x ˜−\{e\}}

Mit értünk el ezzel a programmal? Figyeljük meg, hogy az S programban már csak egyelemű halmazokra kell alkalmazni f -et, azaz f helyett elég egy olyan f′ -vel foglalkoznunk, amelyik nem 2^{H_{1}} -ből képez 2^{H_{2}} -be, hanem csak H_{1} - ből H_{2} -be képez.

30 Elemenénti feldolgozás — második változat

Most az első változattal szemben azt tesszük fel, hogy az f kétváltozós függvény. Így az állapottér A = A_{1} × A_{2} × A_{3}, A_{i} = set(H_{i}), H_{i} ⊂ H (i=1,2,3), a változók x : A_{1}, y : A_{2}, z : A_{3}. A paramétertér B = A_{2} × A_{3}, a változói x′ : A_{1}, y′ : A_{2}. Az elő- és utófeltételek

\begin{matrix}Q_{x′,y′} = (x = x′ ∧ y = y′), \\ R_{x′,y′} = (z = f(x′, y′)). \end{matrix}

Ezt a változatot a z = f(x, y) típusú feladatnak nevezzük.

A megoldó programot az előzőhöz hasonlóan kapjuk. Az invariáns tulajdonság kicsit kibővül, hogy a teljes diszjunktság teljesüljön:

P = (z ∪ f(x, y) = f(x′, y′) ∧ f(x, y) ∩ z = ∅ ∧ (x′ − x) ∩ y = ∅ ∧ (y′ − y) ∩ x = ∅).

A ciklusfeltétel f(x, y) ≠ ∅, a termináló függvény x ∪ y elemeinek száma. A ciklusmag most is egy olyan szekvencia, aminek első tagja e : mem(x ∪ y), ami után a Q′ = P ∧ e ∈ x ∪ y teljesül, hasonlóan mint az előző változatnál.

A szekvencia második tagja most egy elágazás lesz annak megfelelően, hogy e ∈ x ∪ y háromféleképpen fordulhat elő: e csak x -nek, csak y -nak, vagy mindkettőnek eleme. Könnyen látható, hogy igazak a következő állítások:

Q′ ∧ e ∈ x ∧ e_{s}y ⇒ lf(z := z˜∪f({e}, ∅); x := x ˜−{e}, P), Q′ ∧ e_{s}x ∧ e ∈ y ⇒ lf(z := z˜∪f(∅, {e}); y := y ˜−{e}, P), Q′ ∧ e ∈ x ∧ e ∈ y ⇒ lf(z := z˜∪f({e}, {e}); x := x ˜−{e}; y := y ˜−{e}, P).

Pl. a harmadik teljesülése a helyettesítések elvégzése után:

Q′ ∧ e ∈ x ∧ e ∈ y ⇒ (z ∪ f({e}, {e}) ∪ f(x ˜−{e}, y ˜−{e}) = f(x′, y′) ∧ f(x ˜−{e}, y ˜−{e}) ∩ (z ∪ f({e}, {e})) =

∅ ∧ (x′ − (x − {e})) ∩ (y − {e}) = ∅ ∧ (y′ − (y − {e})) ∩ (x − {e}) =
∅ ∧ x ∩ {e} ≠ ∅ ∧ y ∩ {e} ≠ ∅ ∧ z ∩ f({e}, {e}) = ∅).

Figyelembe véve, hogy f tulajdonsága miatt f({e}, {e}) ∪ f(x − {e}, y − {e}) = f(x, y) és f({e}, {e})∩f(x−{e}, y−{e}) = ∅, továbbá e, x ˜−{e} ∈ x és e, y ˜−{e} ∈ y is igazak, ezért az előző implikáció valóban fennáll.

Tehát a második változat programja (GLO x : A_{1}, y : A_{2}, V IR z : A_{3}, LOC e : H):

z := ∅ ; f(x, y) ≠ ∅ ; \overline{e : mem(x ∪ y) ; \ e ∈ x ∧ e ∉ y \ e ∉ x ∧ e ∈ y \ e ∈ x ∧ e ∈ y ; {z := z˜∪f(\{e\}, ∅) \atop x := x ˜−\{e\}} {z := z˜∪f(∅, \{e\}) \atop y := y ˜−\{e\}} z := z˜∪f(\{e\}, \{e\}) ; x := x ˜−\{e\} ; y := y ˜−\{e\}}

31 Elemenkénti feldolgozás — harmadik változat

Most az első változatot úgy módosítjuk, hogy az f függvényről feltesszük, hogy (f_{1}, f_{2}) alakú. Azaz az állapottér A = A_{1}xA_{2}xA_{3}, A_{i} = set(H_{i} ⊂ H)

(i=1,2,3), a változók pedig x : A_{1}, y : A_{2}, z : A_{3}. A paramétertér B = A_{1}, a változója x′. Az elő- és utófeltételek

\begin{matrix}Q_{x′} = (x = x′), \\ R_{x′} = (y = f_{1}(x′) ∧ z = f_{2}(x′)). \end{matrix}

Az első változatból kis átalakítással kapjuk, hogy

P = (y ∪ f_{1}(x) = f_{1}(x′) ∧ y ∩ f_{1}(x) = ∅ ∧ z ∪ f_{2}(x) = f_{2}(x′) ∧ z ∩ f_{2}(x) = ∅).

Most a ciklusfeltétel f_{1}(x) ≠ ∅∨f_{2}(x) ≠ ∅, vagy x ≠ ∅. A termináló függvény ismét x.dom lehet. Ezek után könnyen ellenőrizhető, hogy a megoldó program (GLO x : A_{1}, V IR y : A_{2}, z : A_{3}, LOC e : H):

y, z := ∅, ∅ ; f_{1}(x) ≠ ∅ ∨ f_{2}(x) ≠ ∅ ; \overline{e : mem(x) ; y, z := y˜∪f_{1}(\{e\}), z˜∪f_{2}(\{e\}) ; x := x ˜−\{e\}}

32 Elemenkénti feldolgozás — általános változat

Különösebb probléma nélkül elkészíthető rögzített m -re, n -re a z_{i} = f_{i}(x_{1}, ..., x_{n}) (i = 1, ..., m) feladat programja is az előzőek mintájára. A levezetés formulái így alakulnak:

\begin{matrix}P = (∀i ∈ [1, m] : (z_{i} ∪ f_{i}(x_{1}, ..., x_{n}) = f_{i}(x′_{1}, ..., x′_{n})∧ \\ z_{i} ∩ f_{i}(x_{1}, ..., x_{n}) = ∅) ∧ (∀i, j ∈ [1, n] : (x′_{i} − x_{i}) ∩ x_{j} = ∅)). \end{matrix}

A ciklusfeltétel f_{1}(x_{1}, ..., x_{n}) ∪ ... ∪ f_{m}(x_{1}, ..., x_{n}) = ∅, vagy ∪_{i=1}^{n}x_{i} ≠ ∅. A termináló függvény ∪_{i=1}^{n}x_{i} elemeinek száma. A ciklusmagban levő elágazás ”ágainak” száma 2^{n} − 1. A program sémája a következő:

y_{1}, ..., y_{m} := ∅, ..., ∅ ; ∪_{i=1}^{m}f_{i}(x_{1}, ..., x_{n}) ≠ ∅ ; \overline{e : mem(∪_{i=1}^{n}x_{i}) ; \… \  e ∈ x_{i_{1}} ∧ … e ∈ x_{i_{k}} ∧ e ∉ x_{i_{k+1}} ∧ e ∉ x_{i_{n}}  \…; …  {y := y˜∪f(sl(\{i_{1} … i_{k}\}, e)) \atop x_{i_{1}}, …, x_{i_{k}} := x_{i_{1}} ˜−\{e\}, …, x_{i_{k}} ˜−\{e\}}  …}
ahol i_{1}, ..., i_{n} az 1, ..., n permutációja, sl : 2^{{1,...,n}} × H → Y,

sl(\{i_{1}, .., i_{k}\}, e)_{i} = \{ \begin{matrix}\{e\}, & ha i ∈ i_{1}, ..., i_{k} \\ ∅, & ha i ∉ i_{1}, ..., i_{k} \end{matrix}

az elágazás ”ágainak” száma 2^{n} − 1,

Megjegyezzük végül, hogy mindegyik változat levezethető elemenként feldolgozható reláció esetén is a függvényhez hasonló módon, értelemszerű módosításokkal. Ezt a feladatot az olvasóra bízzuk.