Programinverzió

(példákkal kiegészítve)

Legyen E és U tetszőleges halmazok, legyen X ⊆ 2^{E}. Legyen f_{1} : U → X. Tekintsük az alábbi specifikációval definiált F_{1} feladatot:

A =𝕌 u×𝕏 x

B ={𝕌 \atop u′}

Q : (u = u′)

R : (x = f_{1}(u′))

Tegyük fel, hogy az alábbi S_{1} program megoldja a fenti feladatot.

S_{11}(u) ; x := ∅ ; π_{1} ; \overline{\frac{S_{12}(u, e)}{x := x˜∪\{e\}}}

Az S_{1} programot elemenként előállító programnak nevezzük.

Legyen F és V tetszőleges halmazok, legyen Y ⊆ 2^{F}. Legyen f_{3} : Y → V. Tekintsük az alábbi specifikációval definiált F_{3} feladatot:

A =𝕐 y×𝕍 v

B ={𝕐 \atop y′}

Q : (y = y′)

R : (v = f_{3}(y′))

Tegyük fel, hogy az alábbi S_{3} program megoldja a fenti feladatot.

S_{31}(v) ; y ≠ ∅ ; \overline{d :∈ y ; y := y ≃ \{d\} ; S_{32}(v, d)} ; S_{33}(v)

Az S_{3} programot elemenként felhasználó programnak nevezzük. Legyen f_{2} : X → Y elemenként feldolgozható függvény.

Jelöle S_{2} az f_{2} értékét meghatározó programot. Tekintsük a következő feladatot:

A =𝕌 u×𝕍 v

B ={𝕌 \atop u′}

Q : (u = u′) R : (v = f(u′)) Ahol f : f_{3} ∘ f_{2} ∘ f_{1}.

Könnyen belátható, hogy a következő program megoldja a fenti faladatot:

S_{1} ; S_{2} ; S_{3}

Programinverzió tétele Az alábbi program megoldja az f függvény kiszámításával kapcsolatos feladatot.

S_{11}(u) ; S_{31}(v) ; π_{1} ; \overline{S_{12}(u, e) ; d := f_{2}(\{e\}) ; S_{32}(v, d)} ; S_{33}(v)

Á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 rendezett 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}) ; IF (π_{1}_{1} : S_{1301}_{1}(u_{1}, e_{1}), ¬π_{1}_{1} : e_{1} = ∅) ; …; S_{11}_{n}(u_{n}) ; IF (π_{1}_{n} : S_{1301}_{n}(u_{n}, e_{n}), ¬π_{1}_{n} : e_{n} = ∅) ; S_{31}_{1}(v_{1}) ; ... ; S_{31}_{m}(v_{m}) ; ⋃_{i=1}^{n} e_{i} ≠ ∅ ; \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)) ; IF (π_{1}_{i_{1}} : S_{1301}_{i_{1}}(u_{i_{1}}, e_{i_{1}}), ¬π_{1}_{i_{1}} : e_{i_{1}} = ∅) ; ... ; IF (π_{1}_{i_{k}} : S_{1301}_{i_{k}}(u_{i_{k}}, e_{i_{k}}), ¬π_{1}_{i_{k}} : e_{i_{k}} = ∅) ; IF (g_{1} ≠ ∅ : S_{2302}_{1}(v_{1}, \overline{g_{1}}), g_{1} = ∅ : SKIP) ; ... ; IF (g_{m} ≠ ∅ : S_{2302}_{m}(v_{m}, \overline{g_{m}}), g_{m} = ∅ : SKIP)  …} ; S_{33}_{1}(v_{1}) ; ... ; S_{33}_{m}(v_{m})

ahol \overline{g_{j}} a g_{j} egyetlen eleme, ha g_{j} ≠ ∅, j = 1, ..., m, i_{1}, ..., i_{n} az 1, ..., n permutációja, sl : 2^{{1,...,n}} × H → X,

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

és az {i_{1}, ..., i_{k}} indexhalmazt az {1, ..., n} indexhalmaz minden lehetséges részhalmazára képezzük. Tehát az elágazás ”ágainak” száma 2^{n}−1 és mindíg pontosan egy feltétel teljesül. Továbbá

e_{i} : H, g_{j} : Y_{j},

π_{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.

1. Példa

Tekintsünk egy input file-t, amely 0 és 1-eseket tartalmaz. Hány k-nál hosszabb maximális összefüggő egyes sorozat van a file-ban?

A feladat specifikációja:

A =𝔽 f×{ℕ_{0} \atop s}

B ={𝔽 \atop f′}

Q : (f = f′)

R : (Q ∧ s = ∑_{i=f′.lob}^{f′.hib} χ(β(i)))

Ahol 𝔽 = Infile(E) és E = {0, 1}. β(i) jeleti, hogy az i-edik pozíciótól a file-ban k-nál hosszabb maximális összefüggő egyes sorozat kezdődik.

Legyen 𝕏 = Infile(N_{0}). Definiáljuk 𝔽 és 𝕏 között a következő ρ reprezentációt: f ∈ 𝔽 reprezentálja azt az x ∈ 𝕏 elemet, amelyet f-ből úgy kapunk, hogy a maximális összefüggő egyes sorozatokat az illető sorozat hosszával helyettesítjük. Tekintettel a ρ reprezentációra, hozzunk létre egy olyan típust az 𝔽 és a read művelete segítségével, amely megfelel az (𝕏, read) specfikációnak. A megoldás a következő:

Absztrak open

sf, df, f : read

Absztrak read

\frac{\  sf = norm  /}{sx := norm ; \  df = 0  / ; \frac{dx := 0}{sf, df, f : read} ; dx := 0 ; sf = norm ∧ df = 1 ; \overline{\frac{dx := dx + 1}{sf, df, f : read}} ; {sx := \atop abnorm}}

A kitűzött feladatot a bevezetett állapottér-transzformáció szerint az Infile(N_{0}) típusú szekvenciális input file-ra vonatkozó feltételes számlálás tétele alkalmazásával oldhatjuk meg.

Így a megoldás:

OP EN(x) ; sx, dx, x : read ; s := 0 ; sx = norm ; \overline{\  dx > k  / ; \begin{aligned}s := s + 1 \\ & SKIP \end{aligned} ; sx, dx, x : read}

Legyen 𝕐 = Outfile(N_{0}).

Képezzük az absztrakt file elemeit az𝕐 típusú output file-ban!

sf, df, f : read ; y := <> ; sf = norm ; \overline{\  df = 0  / ; \frac{dx := 0}{sf, df, f : read} ; dx := 0 ; sf = norm ∧ df = 1 ; \overline{\frac{dx := dx + 1}{sf, df, f : read}} ; z : hiext(dx)}

Ezt a programot elemenként előállító programnak nevezhetjük.

Az alábbi programot elemenként felhasználó programnak nevezhetjük.

sx, dx, x : read ; s := 0 ; sx = norm ; \overline{\  dx > k  / ; \begin{aligned}s := s + 1 \\ & SKIP \end{aligned} ; sx, dx, x : read}

Alkalmazva Programinverzió tételét n = 1 és m = 1 esetén, a következő megoldást kapjuk:

sf, df, f : read ; s := 0 ; sf = norm ; \overline{\  df = 0  / ; \frac{dx := 0}{sf, df, f : read} ; dx := 0 ; sf = norm ∧ df = 1 ; \overline{\frac{dx := dx + 1}{sf, df, f : read}} ; \  dx > k  / ; \begin{aligned}s := s + 1 \\ & SKIP \end{aligned}}

Az absztrak műveletek megvalósításának figyelembe vételével a következő megoldáshoz juthatunk:

sf, df, f : read ; \  sf = norm  / ; sx := norm ; \  df = 0  / ; \frac{dx := 0}{sf, df, f : read} ; dx := 0 ; sf = norm ∧ df = 1 ; \overline{\frac{dx := dx + 1}{sf, df, f : read}} ; {sx := \atop abnorm} ; s := 0 ; sx = norm ; \overline{\  dx > k  / ; \begin{aligned}s := s + 1 \\ & SKIP \end{aligned} ; \  sf = norm  / ; sx := norm ; \  df = 0  / ; \frac{dx := 0}{sf, df, f : read} ; dx := 0 ; sf = norm ∧ df = 1 ; \overline{\frac{dx := dx + 1}{sf, df, f : read}} ; {sx := \atop abnorm}}

Belátható, hogy a fenti program és a programinverzióval kapott program az 𝔽 × ℕ_{0} altéren ekvivalensek.

Adottak az x szekvenciális file-ban (megengedett művelet: sx, dx, x : read) egy évfolyam hallgatóinak adatai. Egy elem a hallgató nevét, csoportszámát és tíz db. osztályzatot tartalmaz. A file csoportszámok szerint növekvően rendezett. Állítsuk elő az y sorozatot, amely a hallgatók nevét, csoportszámát és átlagát, valamint a z sorozatot, amely a csoportátlagokat tartalmazza!

Legyen T = (nev : seq(CH), cs : ℕ, jegy : seq([1..10], {1, 2, 3, 4, 5}), T′ = (nev : seq(CH), cs : ℕ, atl : ℝ) és T′′ = (cs : ℕ, atl : ℝ) rekord típusok. Legyenek 𝕏 = Infile(T), valamint Y = seq(T′) és Z = seq(T′′).

A z sorozat előállítása

A feladat specifikációja:

A =𝕏 x×ℤ z

B ={𝕏 \atop x′}

Q : (x = x′)

R : (z = trf_{2}(x′))

Állítsuk elő az x_{cs} Outfile(T) típusú szekvenciális output file-t, amely a cs-ben tárolt csoportkódnak megfelelő csoport adatait tartalmazza. Ezt a feladatot a következő elemenként előállító programmal tehetjük meg.

x_{cs} := <> ; sx = norm ∧ dx.cs = cs ; \overline{dx_{cs} := dx ; sx, dx, x : read ; x_{cs} : hiext((cs, dx_{cs}))}

Az x_{cs} file ismeretében számoljuk ki a csoportátlagot az atl változóba. Ez a feladat a szekvenciális input file típusra transzformált összegzés tételével oldható meg a következő módon:

sx_{cs}, dx_{cs}, x_{cs} : read ; atl, sz := 0, 0 ; sx_{cs} = norm ; \overline{\frac{atl, sz := s = ∑_{i=1}^{10} dx_{cs}.jegy[i], sz + 1}{sx_{cs}, dx_{cs}, x_{cs} : read}} ; atl := atl/sz

Ezt a programot elemenként felgolgozó programnak tekinthetjük. Alkalmazva a Programinverzió tételét n = 1 és m = 1 és az f_{2} identitás, igy

triviálisan elemenként feldolgozható függvény esetén, a következő megoldáshoz juthatunk:

atl, sz := 0, 0 ; sx = norm ∧ dx.cs = cs ; \overline{dx_{cs} := dx ; sx, dx, x : read ; atl, sz := ∑_{i=1}^{10} dx_{cs}.jegy[i], sz + 1} ; atl := atl/sz

Tekintettel arra, hogy az x file a csoportkódókra rendezett, az eredeti feladat megoldását a következő program adja:

sx, dx, x : read ; z := <> ; sx = norm ; \overline{atl, sz := 0, 0 ; cs := dx.cs ; sx = norm ∧ dx.cs = cs ; \overline{dx_{cs} := dx ; sx, dx, x : read ; atl, sz := ∑_{i=1}^{10} dx_{cs}.jegy[i], sz + 1} ; atl := atl/sz ; z : hiext((cs, atl))}

A dx_{cs} változót kiküszöbölhetjük, ha a következő transzformációt végezzük:

sx, dx, x : read ; z := <> ; sx = norm ; \overline{atl, sz := 0, 0 ; cs := dx.cs ; sx = norm ∧ dx.cs = cs ; \overline{\frac{atl, sz := (∑_{i=1}^{10} dx.jegy[i])/10, sz + 1}{sx, dx, x : read}} ; atl := atl/sz ; z : hiext((cs, atl))}

Az y sorozat előállítása

A feladat specifikációja:

A =𝕏 x×𝕐 y

B ={𝕏 \atop x′}

Q : (x = x′)

R : (y = trf_{1}(x′))

Könnyen látható, hogy a megoldást egyváltozós egyértékű elemenként feldolgozható függvény értékének kiszámítása adja az 𝕏 = Infile(T), valamint a Z = seq(T′) típusokkal kapcsolatban.

Az egyes feladatok megoldásai egyetlen programba fésülhetők össze a következő módon:

sx, dx, x : read ; y := <> ; z := <> ; sx = norm ; \overline{atl, sz := 0, 0 ; cs := dx.cs ; sx = norm ∧ dx.cs = cs ; \overline{atl, sz := (∑_{i=1}^{10} dx.jegy[i])/10, sz + 1 ; y : hiext((dx.nev, dx.cs, (∑_{i=1}^{10} dx.jegy[i])/10)) ; sx, dx, x : read} ; atl := atl/sz ; z : hiext((cs, atl))}

Természetesen a (∑_{i=1}^{10} dx.jegy[i])/10 függvényt ki kell transzformálni. Ehhez a megfelelő

programtranszfomációt kell alkalmazni.

Megjegyzés:

Az alábbi formátumú

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 előállító programot általában valamely összetett tipus, pl. file, sorozat, halmaz, stb., ”kibontására” alkalmazhatjuk, ahol az S_{1301}_{i}(u_{i}, e_{i}) program lehetővé teszi valamely absztrak read művelet megvalósítását is.

Ezekben az esetekben a programinverzió tételéhez eljuthatunk úgy is, hogy az f_{1} leképezést elhagyjuk az alábbi módon, majd a kapott tétel alapján típustranszfomáció alkalmazásával jutunk el a programinverzió megfelelő tételéhez.

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

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

specifikációval definiált feladatnak.

S_{31}_{1}(v_{1}) ; ... ; S_{31}_{m}(v_{m}) ; ∨_{i=1}^{n}x_{i} ≠ ∅ ; \overline{e :∈ ( ⋃_{i=1}^{n} x_{i}) ; \… \  e ∈ x_{i_{1}} ∧… e ∈ x_{i_{k}} ∧ e ∉ x_{i_{k+1}} ∧ e ∉ x_{i_{n}}  \…; …  (g_{1}, ..., g_{m}) := f(sl(\{i_{1} … i_{k}\}, e)) ; x_{i_{1}},…, x_{i_{k}} := x_{i_{1}} ≃ \{e\},…, x_{i_{k}} ≃ \{e\} ; IF (g_{1} ≠ ∅ : S_{2302}_{1}(v_{1}, \overline{g_{1}}), g_{1} = ∅ : SKIP) ; ... ; IF (g_{m} ≠ ∅ : S_{2302}_{m}(v_{m}, \overline{g_{m}}), g_{m} = ∅ : SKIP)  …} ; S_{33}_{1}(v_{1}) ; ... ; S_{33}_{m}(v_{m})

ahol \overline{g_{j}} a g_{j} egyetlen eleme, ha g_{j} ≠ ∅, j = 1, ..., m, i_{1}, ..., i_{n} az 1, ..., n permutációja, sl : 2^{{1,...,n}} × H → X,

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

és az {i_{1}, ..., i_{k}} indexhalmazt az {1, ..., n} indexhalmaz minden lehetséges részhalmazára képezzük. Tehát az elágazás ”ágainak” száma 2^{n}−1 és mindíg pontosan egy feltétel teljesül. Továbbá

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.