Problema: mit jelent formalis tipusspecifikacio -> aktualis tipusspecifikacio ? specifikacio morfizmus. Specialis esetei: 1) Atnevezes. 2) Benne foglaltatas, tartalmazas, bovites. 3) Abrazolas, reprezentacio. 4) Parameter atadas. Specialisan, formalis parameterek helyettesitese aktualis parameterekkel (parameter passing): spec(spec_1) -> spec(spec_2). -=- Megjegyzesek. 1. Standard parameteratadas: spec(spec_1) -> spec(spec_2) spec_1 formalis spec_2 aktualis parameter ertekadassal torteno specifikacio, 2. Ismetelt parameteratadas: spec(spec_1(spec_A)) -> spec(spec_2(spec_B)); -=- Szignaturamorfizmus Adott: SZIGMA = (S, OP), SZIGMA' = (S', OP'), mellett a h_SZIGMA:SZIGMA->SZIGMA' lekepezest szignaturamorfizmusnak nevezzuk, ha h_SZIGMA = (h_S:S->S', h_{OP}: OP->OP'); ugy, hogy (\forall N: s_1 ... s_n -> s \in OP)(h_{OP}(N):h_S(s_1)...h_S(s_n)->h_S(s) \in OP'). -=- Kituntetett sortu szignaturamorfizmus: h_s(pt(SZIGMA)) = pt(SZIGMA'). Pelda: kituntetett elemu szignatura morfizmusra a verem eseteben: pt(SZIGMA) = stack; pt(SZIGMA') = vector nat; h_S(stack) = vector nat. -=- sorts: = -=- A h: SZIGMA -> SZIGMA' szignaturamorfizmus kiterjesztese valtozokra: Legyenek X, X' rendre a SZIGMA, SZIGMA' valtozoi. Tovabbiakban altalaban: h=h_{SZIGMA}; h(s) = h_s; h(N) = h_{OP}(N); h_X:(\union_{s \in S} X_S) -> (\union_{s' \in S'} X'_{S'}) ha x\in X_S, s \in S, akkor h_X(x) \in X'_{h(s)=s'}; -=- A h: SZIGMA -> SZIGMA' szignaturamorfizmus kiterjesztese termekre: Adottak: T_{SZIGMA(X)}, T_{SZIGMA'(X')} rendere a SZIGMA, SZIGMA' termeknek halmazai. Minden t\in T_{SZIGMA(X)}-hez tartozo h_T(t)\in T_{SZIGMA'(X')} definicoja: - (\forall x\in X)(h_T(x)=h_X(x)); - (\forall(N:->s)\in OP)(h_T(N:->s)=h_X(h(N):->s); - (\forall N:s_1...s_n->s)\in OP)(h_T(N(t_1, ..., t_n)) = h(N)(h_T(t_1), ..., h_T(t_n)); -=- A h:SZIGMA -> SZIGMA' szignaturamorfizmus kiterjesztese egyenletek formajaban adott axiomakra. Legyen e=(X, L, R) \in E, akkor e helyettesitendo h^*(e) = (X^*, h^*(L), h^*(R)) egyenlettel\in E', ahol \forall x \in X_{s\in S} valtozo helyettesitendo x^*\in X^*_{h(s)=s'\in S\} valtozoval, L es R kepzesnel pedig \forall N:s_1 ... s_n -> s \in OP, eseten N(t_1, ..., t_n) \in T_{OP}(X), helyettesitendo h(N)(h^*(t_1), ..., h^*(t_n)) operacioval. Roviden: - minden x valtozo helyere h(s) = s'-nek megfelelo valtozo; - L, R term a h(N) = N'-nek helyere megfelelo operaciokkal kepezett L'=R' lep. -=- Specifikaciomorfizmus Adva: SPEC=(SZIGMA, S, OP, E), SPEC'=(SZIGMA', S', OP', E'), h_{SPEC}:SPEC->SPEC'; h_{SPEC}=(h_{SZIGMA}, h_E); h_{SZIGMA}:SZIGMA->SZIGMA'; h_E:E->E'; E'=h_E(E) = {h^*(e) | (\forall e= (X, L, R)\in E)}. -=- Definicio: Adva parameteres tipusspecifikacio: PSPEC=(SPEC, SPEC1); ahol SPEC=(S, OP, E), SPEC1=SPEC \union (S1, OP1, E1). Adva tovabba h:SPEC->SPEC' specifikacio morfizmus, ahol SPEC'=(S', OP', E'). Patameteratado morfizmus diagramja: p:tartalmazas SPEC ---------------> SPEC1 = SPEC \union (S1, OP1, E1) | | | h: SPEC->SPEC' | h1 | | V V SPEC'---------------> SPEC1' p': tartalmazas -=- A parameteratadas jelentese: - Ha p es p' tartalmazas az osszes reszspecifikacio eseten; - h1: (\forall s \in S \union S1)(h1(s) = if s\in S1 then s else h(s) fi); (\forall(N:s_1 ... s_n)\in OP\union OP', n>=0)(h1(N:s_1 ... s_n) = if (N:s_1 ... s_n)\in OP then n:h1(s_1) ... h1(s_n)->h1(s) else h(N):h(s_1) ... h(s_n)->h(s) fi; - SPEC1'=SPEC' \union (S', OP', E1'), ahol S1'=S1, OP1'=h1(OP1), E1'=h1^*(E1). -=- p data -----------------------------> string(data) | | | | | h = | h1 | | V V nat -----------------------------> string(nat) p' -=- h_1 SPEC_A ---------------------------> SPEC_B | | | | |h_2 = | h_3 | | | | V V SPEC_C ---------------------------> SPEC_D h_4 = jelentese: h_3 kor h_1 = h_2 kor h_4; -=- Adattipusosztaly specifikacioja: PAR: formalis parameterek specifikacioja; EXP=PAR\union(S1,OP1,E1): export felulet specifikacioja; IMP=PAR\union(S2,OP2,E2): import felulet specifikacioja; BOD=IMP+eb(EXP):megvalositas specifikacioja; e PAR -----------------------> EXP | | | i = | eb V V IMP -----------------------> BOD ib -=- Specifikacio: PAR, IMP; Kituntetett sortu specifikacio: EXP = (S_{EXP}, OP_{EXP}, E_{EXP}); pt(S_{EXP}) \in S_{EXP}; BOD = (S_{BOD}, OP_{BOD}, E_{BOD}); pt(S_{BOD}) \in S_{BOD}; Tartalmazas: e, i, ib; (Ha az absztrakt es a konkret parameterek azonosak!) eb: EXP -> BOD; kituntetett sortu morfizmus; Jelolese a torzs reszben: oprs: rep: pt(S_{BOD})->pt(S_{EXP}) -=- Absztrakt adattipus specifikacioja: PAR ----------------> EXP e -=- Absztrakt adattipus az adattipusoknak egy olyan osztalya, amely zart az adattartomanyok, a muveletek, a tartomanyok peldanyainak es a muveleteknek az elnevezese alapjan. Igy az absztrakt adattipus fuggetlen az adatok abrazolasatol es az adott abrazolasok mellett a muvelek megvalositasatol. -=- is a class specification parameters= parameters= exports= sorts: class sort: oprs: oprs: eqns: eqns: imports= body= sorts: sorts: oprs: oprs: rep:pt(S_{BOD})->pt(S_{EXP}); eqns: eqns: end ; -=- Osztalyspecifikacio, specialis esetek: SPEC --------> SPECEXP --------> SPEC0 | | | | V V PSPEC ------> PSPECEXP -------> CLASS SPEC=(0, BOD, 0, BOD); SPECEXP=(0, EXP, 0, BOD); SPEC0=(0, EXP, IMP, BOD); PSPEC=(PAR, BOD, 0, BOD); PSPECEXP=(PAR, EXP, 0, BOD); CLASS=(PAR, EXP, IMP, BOD); -=- Modul interfesz szerkezet szolgaltatas Modulokbol allo rendszer modulo interakcio moduloperaciok (valtoztatasok) Absztrakt modul: 1. import interfesz 2. export interfesz 3. parameter resz 4. torzs resza 5. reszek kozotti relaciok