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

1. 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 → 𝕃 é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 ∈ ℕ : α_{i} = t_{0}).

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

kiv(t, i) ::= \{ \begin{matrix}α_{i} & , ha 1 ≤ i ≤| α | ∧ (α, t) ∈ ψ_{I} \\ 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 → ℕ_{0} függvényt. Legyen (α, t) ∈ ψ_{I}, ekkor

dom(t) ::= \{ \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) lov : T → T_{0}. lov(t) ::= α_{1}, ha dom(t) ≠ 0.

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

b) ext : T × T → T. Ha (α_{1}, t_{1}), (α_{2}, t_{2}) ∈ ψ_{I}, akkor ext(t_{1}, t_{2}) ::= ψ_{I}(kon(α_{1}, α_{2})). ext(t_{1},…, t_{k}) ::= ext(ext(t_{1},…, t_{k−1}), t_{k}).

c) rem : T × T → T.

rem(t_{1}, t_{2}) ::= \{ \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}) ::= ext(ψ_{I}(t_{0}), t), e) hiext : T × T_{0} → T. hiext(t, t_{0}) ::= ext(t, ψ_{I}(t_{0})),

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

g) lorem : T → T. loext(lorem(t), lov(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} → ℕ_{0}. Ha α ∈ ψ_{I}^{−1}(t) és t_{0} ∈ T_{0}, akkor

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

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

5. A függvény típus: Legyen H tetszőleges rendezett halmaz. A H halmazon értelmezettek a pred, succ, ord függvények, ord(succ(x))−ord(x) = 1, ord(x)−ord(pred(x)) = 1. T = seq(T_{0}). Az F = (domain : H, values : 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.Ekkor

a) dom : F → ℕ_{0}. dom(f) ::= dom(f.values)

b) lob : F → H. lob(f) ::= f.domain

c) hib : F → H. hib(f) ::= succ^{dom(f)−1}(f.domain)

d) kiv : F × H → T_{0}. Ha lob(f) ≤ i ≤ hib(f) kiv(f, i) ::= f.values_{ord(i)−ord(lob(f))+1}

e) lov : F → T_{0}. Ha dom(f) ≠ 0 : lov(f) ::= f.values_{1}

f) hiv : F → T_{0}. Ha dom(f) ≠ 0 : hiv(f) ::= f.values_{dom(t)}

g) hiext : F × T_{0} → F. Ha ord(f.domain) + dom(f) < |H| : hiext(f, t_{0}) ::= ψ_{D}(f.domain, hiext(f.values, t_{0}))

h) loext : F × T_{0} → F. Ha ord(f.domain) ≠ 1 : loext(f, t_{0}) ::= ψ_{D}(pred(f.domain), loext(t_{0}, f.values))

i) hirem : F → F. Ha dom(f) ≠ 0 : hirem(f) ::= ψ_{D}(f.domain, hirem(f.values))

j) hirem : F → F. Ha dom(f) ≠ 0 : lorem(f) ::= ψ_{D}(succ(f.domain), lorem(f.values))

II. 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_{i} é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 t′.s_{j} = t.s_{j}, ha i ≠ j, t′.t_{i} = t_{i}.

2. Egyesítés típusok műveletei: t.s_{i} logikai függvények, m := t_{i}, t_{i} := m. Legyen T = (s_{1} : T_{1}; …; s_{n} : T_{n}), i ∈ [1,…, n].

a) t.s_{i} = (t ∈ ψ_{U}(T_{i})).

b) m := t_{i}, lf(m := t_{i}, R) = R^{m←t_{i}}

c) t_{i} := m, lf(t_{i} := m, R) = R^{t_{i}←m}

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} ∈ t logikai függvény.

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

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

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

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) t_{0} ∈ t logikai függvény.

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

c) t := t − t_{0}, lf(t := t − t_{0}, R) = t_{0} ∈ t ∧ R^{t←t−t_{0}}, ahol (t − t_{0}) ∈ T ∧ ism(t, t_{0}) = ism(t − t_{0}, t_{0}) + 1 ∧ ∀x ∈ T_{0} − {t_{0}} : ism(t, x) = ism(t − t_{0}, x)

d) t := t ∪ t_{0}, lf(t := t ∪ t_{0}, R) = t_{0} ∈ t ∧ R^{t←t∪t_{0}}, ahol (t ∪ t_{0}) ∈ T ∧ (t ∪ t_{0}) − t_{0} = t

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

5. Sorozat típusok műveletei:

dom, lov, hiv, 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 : ℕ_{0}.

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

c) lf(t_{0} := t.hiv, R) = dom(t) ≠ 0 ∧ R^{t_{0}←hiv(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} × ℕ é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←lov(t),lorem(t)}

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

6) Függvény típusok műveletei: dom, lob, hib, hiv, lov, 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.lov, R) = dom(f) ≠ 0 ∧ R^{t_{0}←lov(f)}

e) lf(t_{0} := f.hiv, R) = dom(f) ≠ 0 ∧ R^{t_{0}←hiv(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←hiv(f),hirem(f)}

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

7. Szekvenciális input file:

A SeqInp(T_{0}) = (seq(T_{0}); st, dt, t : read) típust szekvenciális input file-nak nevezzük, ahol

lf(st, dt, t : read, R) = \{ \begin{matrix}R^{st,dt,t←norm,lov(t),lorem(t)} & , t ≠ ∅ \\ R^{st←abnorm} & ,t = ∅ \end{matrix} .

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

9. A verem típus:

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

a) pop(v) ::= v : hirem,

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

c) top(v, t_{0}) ::= t_{0} := v.hiv,

d) empty(v) ::= (v.dom = 0).

10. A sor típus:

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

a) pop(s) ::= s : lorem,

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

c) top(s, t_{0}) ::= t_{0} := s.lov,

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

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