Cursul 9
L i i ii (RWL)
• Logica rescrierii (RWL) – sisteme tranzitionale
regulile de rescriere = specificatori de tranzitii – regulile de rescriere = specificatori de tranzitii – sisteme tranzitionale algebrice
– satisfaceresat s ace e – model initial – deductie
Dorel Lucanu Programare algebrica
Sisteme tranzitionale - definitii
ti h t t (S )
• neetichetate: (S, →) – S - multime de stari
→ ⊆ S x S relatie de tranzitie – → ⊆ S x S – relatie de tranzitie s1 → s2 → s3 → s4 → ...
• etichetate: (S, →, Act)et c etate (S, →, ct) – S - multime de stari
– Act – multime de actiuni (etichete)
– → = {-a→ ⊆ S x S | a ∈ Act} – relatie de tranzitie s1 –a1→ s2 –a2→ s3 –a3→ s4 –a4→ ...
Sisteme tranzitionale – exemple
bil lb i
• cana cu bile albe si negre – stari: {a,n}* (comutativ)
tranzitii:
– tranzitii:
aav → nv anv → av
a → a
nnv → nv
aann → nnn → nn → n
→ aan → aa → n
→ nn → n
Dorel Lucanu Programare algebrica
Sisteme tranzitionale – exemple (continuare)
ti ti l t iti l l
• semantica operationala tranzitionala a programelor – stare = configuratie = (stare-mem, stare-prog)
tranzitie: (s p) → (s' p') – tranzitie: (s, p) → (s ,p )
(s1, x = a; y = x+3;) → (s2, y = x+3;) → (s3, skip;) s2[[x]] = s1[[a]], s3[[y]] = s2[[x+3]] = s1[[a]] + 3
s [[ ]] s [[a]], s3[[y]] s [[ 3]] s [[a]] 3
RWL: signaturi
• sunt specificatii MEL: (Ω, E) confluente si cu proprietatea de terminare
f d CANA i fmod CANA is
sorts Bila Cana .
subsorts Bila < Cana subsorts Bila < Cana . ops a n : -> Bila .
op p _ _ : Cana Cana -> Cana [assoc comm] .[ ] endfm
• un term t ∈ TΩ,E(X) specifica o multime de stari
Dorel Lucanu Programare algebrica
RWL: propozitii (formule)
RWL: propozitii (formule)
R t i tii
• Restrictii
– sort(t) si sort(t') sa fie in aceeasi componenta conexa conditiile pot fi:
– conditiile pot fi:
• ecuatii
• asertiuni de apartenentaase t u de apa te e ta
• specificatori de tranzitii neconditionale si neetichetati
– var(t), var(t'), var(φi) ⊆ X
Dorel Lucanu Programare algebrica
Maude: module sistem
mod CANA is
sorts Bila Cana .
subsorts Bila < Cana . ops a n : -> Bila .
op : Cana Cana > Cana [assoc comm]
op _ _ : Cana Cana -> Cana [assoc comm] . rl [r1] : a a => n .
rl [r2] : a n => a . rl [r2] : a n > a . rl [r3] : n n => n . endm
RWL: modele
d
• deoarece
a a –r1→ n, n n –r3→ n
• rezulta
• rezulta
a a n n –r1 r3→ n n
• deoarece
a a a n –r1→ a n n, a n n –r3→ a n
• rezulta
a a a n –r1 ; r3→ a n
D. Lucanu – Programare Algebrica
RWL: modele
RWL: relatia de satisfacere
Dorel Lucanu Programare algebrica
RWL: deductie
RWL: deductie
Dorel Lucanu Programare algebrica
Semantica operationala tranzitionala a programelor mod OTSEM is
...
rl [at1] : <S, X <- E; P> =>
<S[[ X <- E ]], P> . rl [at2] : <S A[I] < E; P> =>
rl [at2] : <S, A[I] <- E; P> =>
<S[[ A[I] <- E ]], P> .
rl [if1] : <S, if T INSTR1 else INSTR2 P> =>
rl [if1] : <S, if T INSTR1 else INSTR2 P> >
<S, INSTR1 P> if S[[T]] == true . rl [if2] : <S, if T INSTR1 else INSTR2 P> =>
Semantica operationala tranzitionala a programelor rl [wh1] : <S, while T INSTR P> =>
<S, INSTR while T INSTR P>
if S[[T]] == true .
rl [wh2] : <S, while T INSTR P> =>
<S P>
<S, P>
if S[[T]] == false .
Dorel Lucanu Programare algebrica
Maude: sortare
mod SORTING is
protecting INT . sort IntSeq
sort IntSeq .
subsort Int < IntSeq .
op <_;_> : MachineInt MachineInt -> Pair .
t tS
op empty : -> IntSeq .
op __ : IntSeq IntSeq -> IntSeq [assoc] . vars X Y : Int .
crl [srt] : Y X => X Y if Y > X .
endm endm
RWL: reflectare
ifi i l
• specificare universala:
– exista o specificare-RWL U a.i.:
• pot fi reprezentate specificatii RWL in U
• pot fi reprezentate specificatii-RWL in U
• notam cu T reprezentarea lui T in U
• pentru orice specificare-RWL T:pe t u o ce spec ca e
T |- t → t' ddaca U |- 〈T, t〉 → 〈T, t'〉
Dorel Lucanu Programare algebrica
RWL: metalevel
• o specificatie fmod MYNAT is
sort MyNat .
op 0 : -> MyNat .
op s : MyNat > MyNat op s_ : MyNat -> MyNat .
op _+_ : MyNat MyNat -> MyNat [assoc comm id: 0] .
var N M : MyNat .
eq s N + s M = s s (N + M) .
RWL: metalevel
M d > d i META LEVEL M d l ('MYNAT f l ) Maude> red in META-LEVEL : upModule('MYNAT, false) . reduce in META-LEVEL : upModule('MYNAT, false) .
rewrites: 1 in 1847253591ms cpu (2ms real) (0 rewrites/second)
rewrites/second)
result FModule: fmod 'MYNAT is protecting 'BOOL .
sorts 'MyNat sorts MyNat . none
op '0 : nil -> 'MyNat [none] . op ' + : 'MyNat 'MyNat > 'MyNat op '_+_ : 'MyNat 'MyNat -> 'MyNat
[assoc comm id('0.MyNat)] . op 's_ : 'MyNat -> 'MyNat [none] . none
none
eq '_+_['s_['N:MyNat],'s_['M:MyNat]] =
's_['s_['_+_['N:MyNat,'M:MyNat]]] [none] . endfm
endfm Maude>
D. Lucanu – Programare Algebrica
RWL: metalevel
op fmod is sorts endfm : op fmod_is_sorts_.____endfm :
Header
ImportList SortSet
SortSet
SubsortDeclSet OpDeclSet
MembAxSet EquationSet ->
Fmodule .
RWL: metalevel
Ma de> red in META LEVEL
Maude> red in META-LEVEL :
getOps(upModule('MYNAT, false)) . reduce in META-LEVEL :
getOps(upModule('MYNAT, false)) .
rewrites: 2 in 986424581ms cpu (0ms real) (0 rewrites/second)
result OpDeclSet:
op '0 : nil -> 'MyNat [none] .
op ' + : 'MyNat 'MyNat -> 'MyNat op _+_ : MyNat MyNat > MyNat
[assoc comm id('0.MyNat)] .
op 's_ : 'MyNat -> 'MyNat [none] . M d >
Maude>
Dorel Lucanu Programare algebrica
