II. Programtranszformációk

Definicíciók: Jelölések: A = A_{1} × ... × A_{m}, a_{i} : A_{i}, i = 1, 2, ..., m, S ⊆ A × A^{∗∗}

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

2. Azt mondjuk, hogy az a_{i} : A_{i}, i ∈ [1..m], 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}, i ∈ [1..m], változót, ha ∀a ∈ D_{p(S)} : ∀b ∈ p(S)(a) : b_{i} = a_{i}.

Tételek:

1. Nem megengedett elágazásfeltételek kitranszformálása Legyenek S_{i} ⊆ A×A^{∗∗}, i = 1, 2, ..., n, programok és π_{j} : A → L, i = 1, 2, ..., j,

logikai függvények, ahol A = A_{1} × ... × A_{m}. Legyen S_{IF} = IF (π_{1} : S_{1}, ..., π_{n} : S_{n}). Legyen A′ = A_{1} × ... × A_{m} × L_{1} × ... × L_{n} és a_{i} : A_{i}, i = 1, 2, ..., m, l_{j} : L_{j}, j = 1, 2, ..., n. Legyen továbbá

S′ ⊆ A′ × A′^{∗∗} :

l_{1} := π′_{1}(a_{1}, ..., a_{m}, l_{1}, ..., l_{n}) ; ... ; l_{n} := π′_{n}(a_{1}, ..., a_{m}, l_{1}, ..., l_{n})

ahol π′_{j} : A′ → L és π′_{j}(a_{1}, ..., a_{m}, l_{1}, ..., l_{n}) = π_{j}(a_{1}, ..., a_{m}), j = 1, 2, ..., n. Ekkor az S′_{IF} ::= (S′; IF (l_{1} : S′_{1}, ..., l_{n} : S′_{n}), program ahol S′_{j} az S_{j} program kiterjesztése az A′ térre, j = 1, 2, ..., n, ekvivalens A-n az S programmal.( biz.: lev. szab. )

2. Nem megengedett ciklusfeltétel kitranszformálása

Legyen A = A_{1} × ... × A_{m}, S_{0} ⊆ A × A^{∗∗} program és π : A ← L állítás. Legyen S_{DO} = DO(π : S_{0}). Legyen A′ = A_{1} × ... × A_{m} × L, a_{i} : A_{i}, i = 1, 2, ..., m és l : L. Jelölje S′_{0} az S_{0} program kiterjesztését az A′ térre.

S′_{DO} ⊆ A′ × A′^{∗∗} :

l := π′(a_{1}, ..., a_{m}, l) ; l ; \overline{\frac{S′_{0}}{l := π′(a_{1}, ..., a_{m}, l)}}

program, ahol π′(a_{1}, ..., a_{m}, l) = π(a_{1}, ..., a_{m}), ekvivalens A-n az S_{DO} programmal. ( biz.: lev. szab. )

3. Szimultán értékadás kitranszformálása S ⊆ A × A^{∗∗} és S ::= a_{i_{1}}, ..., a_{i_{j}} := f_{1}(a_{i_{1}}, ..., a_{i_{j}}), ..., f_{j}(a_{i_{1}}, ..., a_{i_{j}}), ahol A = A_{1} × ... × A_{m}. Legyen A′ = A_{1} × ... × A_{m} × A′_{i_{1}} × ... × A′_{i_{j}}, a_{i} : A_{i}, i = 1, ..., m, a′_{i_{k}} : A′_{i_{k}} és

A′_{i_{k}} = A_{i_{k}}, k = 1, ..., j.

Legyen

S′ ⊆ A′ × A′^{∗∗} :

\frac{a′_{i_{1}}, ..., a′_{i_{j}} := f_{1}(a_{i_{1}}, ..., a_{i_{j}}), ..., f_{j}(a_{i_{1}}, ..., a_{i_{j}})}{a_{i_{1}}, ..., a_{i_{j}} := a′_{i_{j}}, ..., a′_{i_{j}}}

valamint

S′′ ⊆ A′ × A′^{∗∗} :

a′_{i_{1}} := f_{1}(a_{i_{1}}, ..., a_{i_{j}}) ; ... ; a′_{i_{j}} := f_{j}(a_{i_{1}}, ..., a_{i_{j}}) ; a_{i_{1}} := a′_{i_{1}} ; ... ; a_{i_{j}} := a′_{i_{j}}

Ekkor az S′ program ekvivalens A-n az S programmal és S′′ program ekvivalens A-n az S programmal. ( biz.: szekv. lev. szab. )

4. Szekvencia két tagjának felcserélése Legyenek S_{1} és S_{2} programok az A állapottéren. Legyen S_{12} = (S_{1}; S_{2}) és

S_{21} = (S_{2}; S_{1}). Tegyük fel, hogy minden olyan állapottérkomponenst, amelytől p(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: Legyen S_{0} program, π állítás az A állapottéren. Legyen S = DO(π : S_{0}).

Tegyük fel, hogy S_{0} = (i := i + 1; S_{01}). Legyen \overline{S_{0}} = (S_{01}^{i←i+1}; i := i + 1). Ha i konstans függvény S_{01}-ben, akkor S ekvivalens \overline{S} = DO(π : \overline{S_{0}})-vel az A-n.

6. Függvény helyettesítése változóval

Legyen f az A = A_{1} × ... × A_{m} állapottér A_{i_{1}} × ... × A_{i_{k}} alterén értelmezett függvény, melynek értékkészlete a H halmaz. ( f ∘ (a_{i_{1}}, ..., a_{i_{k}}) az A-n értelmezett fgv. ) Ha S-ben az a_{i_{1}}, ..., a_{i_{k}} változók konstans függvények, akkor S ekvivalens az

\overline{S} = (z := f(a_{i_{1}}, ..., a_{i_{k}}); S′^{f(a_{i_{1}} ,...,a_{i_{k}})←z})

programmal az A-n, ahol \overline{S} ⊆ A′ × A′^{∗∗} és A′ = A_{1} × ... × A_{m} × H, a_{i} : A_{i}, i=1,2,...,m és z : H és S′ az S program kiterjesztése A′-ra. .

7. Rekurzív függvény kitranszformálása

Legyen A = A_{1} × ... × A_{m} állapottér, S_{0} és S_{1} programok A-n, valamint π állítás A-n. Legyen továbbá H egy tetszőleges halmaz, k > 0 egy egész szám, továbbá f : Z → H, h : Z × H^{k} → H 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)).

Legyen S :

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

program A-n, és tegyük fel, hogy i konstans függvény S_{1}-ben és S_{0}-ban, valamint S_{0}-ban hivatkozás történik f(i + 1)-re. Ekkor S ekvivalens a következő S′ ⊆ A′ × A′^{∗∗} 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, z, z_{−1}, .., z_{−k+1}), z, .., z_{−k+2} \\ S′_{0} & f(i+1)←z \\ i := i + 1 \end{matrix}}

ahol A′ = A_{1} × ... × A_{m} × H × H_{−1} × ... × H_{−k+1}, a_{i} : A_{i}, i = 1, 2, ..., m, z : H és z_{i} : H_{i}, i = −1, ..., −k + 1. S′_{0} az S_{0} kiterjesztése A′-ra, S′_{1} az S_{1} kiterjesztése A′-ra, és π′(a_{1}, ..., a_{m}, z, z_{−1}, ..., z_{−k+1}) = π(a_{1}, ..., a_{m}).

8. Programinverzió - általános eset

Jelölések:

A továbbiakban legyen i = 1, ..., n és j = 1, ..., m. Legyenek U_{i}, V_{j} tetszőleges típusértékhalmazok, H tetszőleges halmaz.

\begin{matrix}X ::= X_{1} × ... × X_{n}, X_{i} ⊆ 2^{H}(i = 1, ..., n), \\ Y ::= Y_{1} × ... × Y_{m}, Y_{j} ⊆ 2^{H}(j = 1, ..., m). \end{matrix}

Legyenek f_{1}_{i} : U_{i} → X_{i}, f_{2} : X → Y, f_{3}_{j} : Y_{j} → V_{j} függvények. Legyen f_{2} elemenként feldolgozható és

∀e ∈ X :

(∀e_{0} ∈ H : ∀i ∈ [1, n] : (e_{i} = ∅ ∨ e_{i} = {e_{0}}) → ∀j ∈ [1, m] : (|f_{2}(e)_{j}| ≤ 1))

Definicíciók: Elemenként előállító program

Az S_{1}_{i} ⊆ A_{1}_{i} × A_{1}_{i}^{∗∗}, S_{1}_{i} ::= (S_{11}_{i}(u); x_{i} := ∅; DO(π_{1}_{i}; S_{130}_{i})) programot elemenként előállító programnak nevezzük, ha

i) megoldása az alábbi Q_{u_{i}}′ és R_{u_{i}}′ elő-, ill. utófeltétel párral specifikált feladatnak,

ii) P_{u_{i}}′ az S_{13}_{i} program ciklusinvariánsa, valamint iii) S_{11}_{i}(u_{i}) és S_{1301}_{i}(u_{i}, e_{i})-ben x_{i} konstans függvény, ahol

A_{1}_{i} = U_{i} × X_{i}, u_{i} : U_{i}, x_{i} : X_{i}

B_{1}_{i} = U_{i}, u_{i}′ : U_{i}

Q_{u_{i}}′ = (u_{i} = u_{i}′),

R_{u_{i}}′ = (x_{i} = f_{1}_{i}(u_{i}′)).

P_{u_{i}}′ = (x_{i} ∪ f_{1}_{i}(u_{i}) = f_{1}_{i}(u_{i}′) ∧ ∀p, q ∈ H : (p ∈ x_{i} ∧ q ∈ f_{1}_{i}(u_{i}) → p < q).

S_{11}_{i}(u_{i}) ; x_{i} := ∅ ; π_{1}_{i} ; \overline{\frac{S_{1301}_{i}(u_{i}, e_{i})}{x_{i} := x_{i} ˜∪e_{i}}}

Elemenként felhasználó program

Az S_{3}_{j} ⊆ A_{3}_{j} × A_{3}_{j}^{∗∗}, S_{3}_{j} ::= (S_{31}_{j}(v_{j}); DO(y_{j} ≠ ∅; S_{320}_{j}); S_{33}_{j}(v_{j})) programot elemenként felhasználó programnak nevezzük, ha

i) megoldása az alábbi Q_{y_{j}}′ és R_{y_{j}}′ elő-, ill. utófeltétel párral specifikált feldatnak,

ii) P_{y_{j}}′ az S_{32}_{j} program ciklusinvariánsa, valamint iii) S_{31}_{j}(v_{j}), S_{3203}_{j}(v_{j}, g_{j}) és S_{33}_{j}(v_{j})-ban y_{j} konstans függvény.

A_{3}_{j} = Y_{j} × V_{j}, y_{j} : Y_{j}, v_{j} : V_{j} B_{3}_{j} = Y_{j} y_{j}′ : Y_{j} Q_{y_{j}}′ = (y_{j} = y_{j}′), R_{y_{j}}′ = (v_{j} = f_{3}_{j}(y_{j}′)) P_{y_{j}}′ = ......

S_{31}(v_{j}) ; y_{j} ≠ ∅ ; \overline{g_{j} := mem(y_{j}) ; y_{j} := y_{j} ˜−\{g_{j}\} ; S_{3203}_{j}(v_{j}, g_{j})} ; S_{33}_{j}(v_{j})

Tétel:

Legyen f ::= f_{3} o f_{2} o f_{1}, ahol f_{1} ::= (f_{1}_{1}, ..., f_{1}_{n}),f_{3} ::= (f_{3}_{1}, ..., f_{3}_{m}). Az alábbi S program megoldása az

A = U_{1} × ... × U_{n} × V_{1} × ... × V_{m}, u_{i} : U_{i}, v_{i} : V_{i} B = U_{1} × ... × U_{n} u_{i}′ : U_{i} Q_{u_{1}′,...,u_{n}′} = (u_{1} = u_{1}′ ∧ ... ∧ u_{n} = u_{n}′), R_{u_{1}′,...,u_{n}′} = ((v_{1}, ...v_{m}) = f(u_{1}′, ..., u_{n}′))

specifikációval definiált feladatnak.

S_{11}_{1}(u_{1}) ; S_{1301x}_{1}(u_{1}, e_{1}) ; …; S_{11}_{n}(u_{n}) ; S_{1301x}_{n}(u_{n}, e_{n}) ; S_{31}_{1}(v_{1}) ; ... ; S_{31}_{m}(v_{m}) ; π_{1}_{1} ∨ ... ∨ π_{1}_{n} ; \overline{e : min_{i=1}^{n}(e_{i}) ; \… \  e = e_{i_{1}} ∧… ∧ e = e_{i_{k}} ∧ e ≠ e_{i_{k+1}} ∧… ∧ e ≠ e_{i_{n}}  \…; …  (g_{1}, ..., g_{m}) := f(sl(\{i_{1} … i_{k}\}, e)) ; S_{1301x}_{i_{1}}(u_{i_{1}}, e_{i_{1}}) ; ... ; S_{1301x}_{i_{k}}(u_{i_{k}}, e_{i_{k}}) ; S_{3202x}_{1}(v_{1}, g_{1}) ; ... ; S_{3202x}_{m}(v_{m}, g_{m})  …} ; S_{33}_{1}(v_{1}) ; ... ; S_{33}_{m}(v_{m})

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, e_{i} : X_{i}, g_{j} : Y_{j}, S_{1301x}_{i}(u_{i}, e_{i}) ::= IF (π_{1}_{i} : S_{1301}_{i}(u_{i}, e_{i}); ¬π_{1}_{i} : e_{i} := ∅), S_{3202x}_{j}(v_{j}, g_{j}) ::= IF (g_{j} ≠ ∅ : S_{2302}_{j}(v_{j}, g_{j}); g_{j} = ∅ : SKIP), π_{1}_{i}, S_{11}_{i}(u_{i}), S_{1301}_{i}(u_{i}, e_{i}) az S_{1}_{i} program, S_{31}_{j}(u_{j}), S_{3203}_{j}(v_{j}, g_{j}), S_{33}_{j}(v_{j})

az S_{3}_{j} program megfelelő részei.

9. Kiemelési szabályok

a) IF (π_{1} : (S; S_{1}), π_{2} : (S; S_{2})) ekvivalens A-n az S′ = (S; IF (π_{1} : S_{1}, π_{2} : S_{2}) programmal, ha π_{1} és π_{2} függvényekre és az S programra alkalmazható a fv. helyettesítése változóval transzformáció.

b) ...

III. Típustranszformációk programozási tételekre

1. Sorozatról (a) file(lopop,ext)-ra (x) : ( előreolvasási technikával )

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

2. Halmazról (x, y, z szig. mon. rend. sorozatra (a, b, c) (elemenkénti feldolg.)

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 ([m, n] , i ∈ [m, n]) értelmezett függvényről sorozatra x

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

4. Sorozatról a vektorra v , i, j ∈ [v.lob, v.hib] , i ≤ j ( fv. típusra )

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