Post on 15-Oct-2019
transcript
D. Lucanu – Programare Algebrica
Curs 5• Verificarea corectitudinii programelor
– asertiuni– satisfacerea asertiunilor de catre memorii– programe adnotate (formule de corectitudine)– utilizarea Maude pentru verificarea programelor
D. Lucanu – Programare Algebrica
Motivatie• Este urmatorul program corect?
if (a < b)swap(a, b); // interschimba a cu b
if (b < c)swap(b, c); // interschimba b cu c
• un program corect = un program care rezolva (corect) o problema• ce problema rezolva programul de mai sus?• o posibila formulare:
assert(true)if (a < b)
swap(a, b); if (b < c)
swap(b, c);assert(a < b < c)
D. Lucanu – Programare Algebrica
Asertiuni
D. Lucanu – Programare Algebrica
Relatia de satisfacere
D. Lucanu – Programare Algebrica
Formule de corectitudine
D. Lucanu – Programare Algebrica
Formule de corectitudine: exemple• atribuire
assert(y == 3)x = 2*y + 5;assert(x == 11)
• maximul a doua variabileassert(x == a and y == b)m = x;if (m < y)m = y;
assert(m == max(a, b))
D. Lucanu – Programare Algebrica
Formule de corectitudine: exemple (continuare)• ordonarea a doua variabile
assert(x == a and y == b)if (x < y){t = x; x = y; y = t;
}assert(x ≤ y and {x,y}=={a,b})
• cmmdcassert(a > 0 and b > 0)x = a; y = b;while ( y > 0){
r = x % y; x = y; y = r;}assert(x == gcd(a,b))
D. Lucanu – Programare Algebrica
Corectitudinea programelor
D. Lucanu – Programare Algebrica
Extinderea specificatiei numerelor intregi cu expresii
fmod EXPINT ispr INT .*** equiv operator ***op _equiv_ : Int Int -> Bool [comm prec 34] .var I J K L : Int .eq I equiv I = true .eq (I + J) equiv (K + J) = I equiv K .eq (I - J) equiv (K - J) = I equiv K .cq I equiv J = false if (I < J) or (J < I) .cq I equiv J = true if I == J .eq ((I + 1)*(I + 1)) equiv (I * I + 2 * I + 1) =
true .eq ((I + 1)*(I + 1)*(I + 1)) equiv
(I * I * I + 3 * I * I + 3 * I + 1) = true .endfm
D. Lucanu – Programare Algebrica
Verificarea corectitudinii programelor in Maude: atribuire• formula de corectitudine
assert(y == 3)x = 2*y + 5;assert(x == 11)
• codul Maude:fmod ASS-VAR issort MySimVar MyArrVar .ops x y : -> MySimVar .
endfm
view ASS-VAR-VIEW from VAR to ASS-VAR is sort SimVar to MySimVar .sort ArrVar to MyArrVar .
endv
fmod ASS-OBJ isprotecting OBJCODE{ASS-VAR-VIEW} .op instr : -> ObjInstr .eq instr = (x <- 2 * y + 5 ;) .
endfm
D. Lucanu – Programare Algebrica
Verificarea corectitudinii programelor in Maude: atribuirea
• modulul pentru demonstratie:fmod ASS-PROOF is
pr ASS-OBJ + SEM{ASS-VAR} .op s : -> Store .*** preconditieeq s[[ y ]] = 3 .
endfm• verificarea postconditiei
Maude> red (s [[ instr ]]) [[ x === 11 ]] . reduce in ASS-PROOF : s[[instr]][[x === 11]] .rewrites: 14 in 13001ms cpu (0ms real) (1
rewrites/second)result Bool: true
D. Lucanu – Programare Algebrica
Verificarea corectitudinii programelor in Maude: swap• formula de corectitudineassert(x == a and y == b) - preconditiont = x;x = y;y = t;
assert(x == b and y == a) - postcondition• codul Maudefmod SWAP-VAR issort MySimVar MyArrVar .ops t x y : -> MySimVar .
endfmview SWAP-VAR-VIEW from VAR to SWAP-VAR is sort SimVar to MySimVar .sort ArrVar to MyArrVar .
endvfmod SWAP-OBJ ispr OBJCODE{SWAP-VAR-VIEW} .op body : -> ObjInstrSeq .eq body = (t <- x ;) (x <- y ;) (y <- t ;) .
endfm
D. Lucanu – Programare Algebrica
Verificarea corectitudinii programelor in Maude: swap (cont.)• definirea starii initiale care satisface preconditiafmod SWAP-PROOF is
pr SWAP-OBJ + SEM{SWAP-VAR-VIEW} .ops a b : -> Int .op s : -> Store .*** preconditioneq s[[ x ]] = a .eq s[[ y ]] = b .
endfm
• verificarea postconditiei
red (s[[ body ]])[[ x === b ]] . ***> it should be true
red (s[[ body ]])[[ y === a]] . ***> it should be true
D. Lucanu – Programare Algebrica
Verificarea corectitudinii programelor in Maude: max • formula de corectitudine
assert(x == a and y == b)m = x;if (m < y) m = y;assert(m == max(a, b))
• codul Maudefmod MAX-VAR issort MySimVar MyArrVar .ops m x y : -> MySimVar .
endfmview MAX-VAR-VIEW from VAR to MAX-VAR is sort SimVar to MySimVar .sort ArrVar to MyArrVar .
endvfmod MAX-OBJ ispr OBJCODE{MAX-VAR-VIEW} .op body : -> ObjInstrSeq .eq body = (m <- x ;) (if (m < y) m <- y ;) .
endfm
D. Lucanu – Programare Algebrica
Verificarea corectitudinii programelor in Maude: max (cont. I)
• modulul pentru demonstratiefmod MAX-PROOF ispr MAX-OBJ + SEM{MAX-VAR-VIEW} .ops a b : -> Int .op s : -> Store .*** preconditioneq s[[ x ]] = a .eq s[[ y ]] = b .
endfm
D. Lucanu – Programare Algebrica
Verificarea corectitudinii programelor in Maude: max (cont. II)• verificarea postconditiei*** case 1fmod MAX-PROOF-CASE1 is
pr MAX-PROOF .eq (a < b) = true .
endfmred (s[[ body ]])[[ m ]] == max(a, b) .
***> it should be true*** case 2fmod MAX-PROOF-CASE1 is
pr MAX-PROOF .eq (a < b) = false .
endfmred (s[[ body ]]) [[ m ]] == max(a, b) .
***> it should be trueclose
D. Lucanu – Programare Algebrica
Corectitudine partiala: reguli de deductie
assert(x < a )
x = x + 1;
assert(x <= a)
assert(x <= a )
a = a + 5;
assert(x <= a - 5)
assert(x < a )
x = x + 1;
a = a + 5;
assert(x <= a - 5)
D. Lucanu – Programare Algebrica
Corectitudine partiala: reguli de deductie
assert(x < a ){ x = x + 1;a = a + 5;
}assert(x <= a - 5)
assert(x < a )x = x + 1;a = a + 5;assert(x <= a - 5)
D. Lucanu – Programare Algebrica
Corectitudine partiala: reguli de deductie (continuare)
assert(x > 0)if (x < 2)x = x + 2;
assert(x >= 2)
assert(x > 0 and x < 2)x = x + 2;assert(x >= 2)
x > 0 and !(x < 2) ⇒ x >= 2
D. Lucanu – Programare Algebrica
Corectitudine partiala: reguli de deductie (continuare)
assert(x == a and y == b and x > y)
z = x;assert(z == max(a, b))
assert(x == a and y == b and !(x > y))
z = y;assert(z == max(a, b))
assert(x == a and y == b)if (x > y)z = x;
elsez = y;
assert(z = max(a, b))
D. Lucanu – Programare Algebrica
Corectitudine partiala: reguli de deductie (continuare)
assert(x + y = a + b and y > 0){ x = x + 1;y = y - 1;
}assert(x + y = a + b)
assert(x + y = a + b)while (y > 0) {x = x + 1;y = y - 1;
}assert(x + y = a + b and !(y > 0))
D. Lucanu – Programare Algebrica
assert(x + y = a + b)while (y > 0) {
x = x + 1;y = y - 1;
}assert(x + y = a + b and not(y > 0))
• formula (x + y = a + b) se numeste invariant• mai notam:
assert(inv: x + y = a + b)while (y > 0) {
x = x + 1;y = y - 1;
}
Corectitudine partiala: reguli de deductie (continuare)
D. Lucanu – Programare Algebrica
Corectitudine partiala: reguli de deductie (continuare II)
assert((x == 0) and (y == a) )x = x + 1;y = y – 1;assert(x + y == a)
assert(x + y == a)x = x + 1;y = y – 1;assert(x + y == a)
(x == 0) and (y == a) ⇒x + y == a
D. Lucanu – Programare Algebrica
Verificarea corectitudinii programelor in Maude: swap• formula de corectitudineassert(x == a and y == b) - preconditiont = x;x = y;y = t;
assert(x == b and y == a) - postcondition• codul Maudefmod SWAP-VAR issort MySimVar MyArrVar .ops t x y : -> MySimVar .
endfmview SWAP-VAR-VIEW from VAR to SWAP-VAR is sort SimVar to MySimVar .sort ArrVar to MyArrVar .
endvfmod SWAP-OBJ ispr OBJCODE{SWAP-VAR-VIEW} .op body : -> ObjInstrSeq .eq body = (t <- x ;) (x <- y ;) (y <- t ;) .
endfm
D. Lucanu – Programare Algebrica
Verificarea corectitudinii programelor in Maude: swap (cont.)• definirea starii initiale care satisface preconditiafmod SWAP-PROOF is
pr SWAP-OBJ + SEM{SWAP-VAR-VIEW} .ops a b : -> Int .op s : -> Store .*** preconditioneq s[[ x ]] = a .eq s[[ y ]] = b .
endfm
• verificarea postconditiei
red (s[[ body ]])[[ x === b ]] . ***> it should be true
red (s[[ body ]])[[ y === a]] . ***> it should be true
D. Lucanu – Programare Algebrica
Verificarea corectitudinii programelor in Maude: cmmdc
• formula de corectitudine
int x, y, r, a, b;assert(a > 0 and b > 0)x = a; y = b;while ( y > 0){
r = x % y; x = y; y = r;}assert(x == gcd(a,b))
D. Lucanu – Programare Algebrica
Verificarea corectitudinii partiale a programelor in Maude: cmmdc• codul Maudefmod CMMDC-VAR is
sort MySimVar MyArrVar .ops a b x y r : -> MySimVar .
endfm
view CMMDC-VAR-VIEW from VAR to CMMDC-VAR is sort SimVar to MySimVar .sort ArrVar to MyArrVar .
endv
fmod CMMDC-OBJ ispr OBJCODE{CMMDC-VAR-VIEW} .ops init body wbody : -> ObjInstrSeq .eq init = (x <- a ;) (y <- b ;) .eq wbody = (r <- x % y ;) (x <- y ;) (y <- r ;) .eq body = init while (y > 0) { wbody } .
endfm
D. Lucanu – Programare Algebrica
Verificarea corectitudinii programelor in Maude: cmmdc (cont.)
• definirea starii initiale care satisface preconditiafmod CMMDC-PROOF is
pr CMMDC-OBJ + SEM{CMMDC-VAR-VIEW} .op s : -> Store .
*** preconditioneq s[[a]] > 0 = true .eq s[[b]] > 0 = true .
endfm
D. Lucanu – Programare Algebrica
Verificarea corectitudinii partiale a programelor in OBJ3: (cont.)
• invariant:gcd(x,y) = gcd(a,b) ∧ y >= 0
• verificarea invariantului (premiza regulei 6)fmod CMMDC-PROOF-INV is
pr CMMDC-PROOF .op s' : -> Store .eq gcd(s'[[x]], s'[[y]]) =
gcd(s[[a]], s[[b]]) .eq s'[[y]] > 0 = true .
endfm
red gcd((s'[[wbody]])[[x]], (s'[[wbody]])[[y]])== gcd(s[[a]], s[[b]]) .
red (s'[[wbody]])[[y]] >= 0 .
D. Lucanu – Programare Algebrica
Verificarea corectitudinii partiale a programelor in Maude: (cont.)
• aplicam regula 7 (while)assert(gcd(x,y) == gcd(a,b) ∧ y >= 0)while ( y > 0){
r = x % y; x = y; y = r;}assert(gcd(x,y) == gcd(a,b) ∧ y >= 0
∧ y <= 0)• putina logica
– (y >= 0) ∧ (y <= 0)⇒ y == 0– (y = 0) ⇒ gcd(x,y) == x– (y = 0 ∧ gcd(x,y) == gcd(a,b)) ⇒
x == gcd(a,b)
D. Lucanu – Programare Algebrica
• aplicam regula 8 (implicatia)assert(gcd(x,y) = gcd(a,b) ∧ y >= 0)while ( y > 0){
r = x % y; x = y; y = r;}assert(x == cmmdc(a,b))
• verificam initializarea
red gcd((s[[init]])[[x]], (s[[init]])[[y]]) ==gcd(s[[a]], s[[b]]) .
red (s[[init]])[[y]] >= 0 .
Verificarea corectitudinii partiale a programelor in Maude: (cont.)
D. Lucanu – Programare Algebrica
Verificarea corectitudinii partiale a programelor in Maude: (cont.)
• aplicam regula 3 (compunerea)assert(a > 0 ∧ b > 0)x = a; y = b;while ( y > 0){
r = x % y; x = y; y = r;}assert(x == gcd(a,b))
D. Lucanu – Programare Algebrica
Verificarea corectitudinii partiale a programelor in Maude: (cont.)
assert{a > 0 ∧ b > 0}x = a; y = b;assert(inv: gcd(x,y) = gcd(a,b) ∧ y >= 0)while ( y > 0){
r = x % y;x = y;y = r;
}assert{x == gcd(a,b)}
D. Lucanu – Programare Algebrica
Gasirea invariantilor
a = 0;b = 0;y = 0;while (y <= x){y <- y + 3 * a + 3 * b + 1; a <- a + 2 * b + 1 ; b <- b + 1;
}
D. Lucanu – Programare Algebrica
Gasirea invariantilorfmod 3SQRTX-VAR issort MySimVar MyArrVar .ops a b x y : -> MySimVar .
endfm
view 3SQRTX-VAR-VIEW from VAR to 3SQRTX-VAR is sort SimVar to MySimVar .sort ArrVar to MyArrVar .
endv
fmod 3SQRTX-OBJ ispr OBJCODE{3SQRTX-VAR-VIEW} .ops init body whilebody : -> ObjInstrSeq .eq init = (a <- 0 ;) (b <- 0 ;) (y <- 0 ; ) .eq whilebody = (y <- y + 3 * a + 3 * b + 1 ;)
(a <- a + 2 * b + 1 ;)(b <- b + 1 ;) .
eq body = init while (y <= x) { whilebody }.endfm
D. Lucanu – Programare Algebrica
Gasirea invariantilor
• testarefmod 3SQRTX-TEST is
pr 3SQRTX-OBJ + SEM{3SQRTX-VAR-VIEW} .op s : -> Store .eq s[[x]] = 125 .
endfm
red (s[[body]])[[b]] .red (s[[body]])[[y]] .
D. Lucanu – Programare Algebrica
Gasirea invariantilor• testare (cont.)
fmod 3SQRTX-TEST ispr 3SQRTX-OBJ + SEM{3SQRTX-VAR-VIEW} .op s : -> Store .op m : -> Int .eq s[[x]] = m .
endfm
red (s[[init whilebody]])[[a]] .result NzNat: 1red (s[[init whilebody]])[[b]] .result NzNat: 1red (s[[init whilebody]])[[y]] . result NzNat: 1
D. Lucanu – Programare Algebrica
Gasirea invariantilor
red (s[[init whilebody whilebody]])[[a]] .result NzNat: 4red (s[[init whilebody whilebody]])[[b]] .result NzNat: 2red (s[[init whilebody whilebody]])[[y]] .result NzNat: 8
• care vor fi urmatoarele valori?
D. Lucanu – Programare Algebrica
Gasirea invariantilorfmod 3SQRTX-TEST is
pr 3SQRTX-OBJ + SEM{3SQRTX-VAR-VIEW} .op s : -> Store .ops m nb : -> Int .eq s[[x]] = m .eq s[[a]] = nb * nb .eq s[[b]] = nb .eq s[[y]] = nb * nb * nb .
endfmred (s[[whilebody]])[[a]] .result Int: 1 + nb * nb + nb * 2red (s[[whilebody]])[[b]] .result Int: nb + 1red (s[[whilebody]])[[y]] .result Int: 1 + nb * nb * nb + nb * 3 + nb * nb * 3
D. Lucanu – Programare Algebrica
Gasirea invariantilor*** inv: a = b*b and y = b*b*b and
(b-1)*(b-1)*(b-1) <= x .
fmod 3SQRTX-PROOF-INV ispr 3SQRTX-OBJ + SEM{3SQRTX-VAR-VIEW} .op s : -> Store .eq s[[a]] = s[[b]] * s[[b]] .eq s[[y]] = s[[b]] * s[[b]] * s[[b]] .eq s[[b]] * s[[b]] * s[[b]] <= s[[x]] . *** y <= x
endfm
red (s[[whilebody]])[[a ]] equiv (s[[whilebody]])[[b]] * (s[[whilebody]])[[b]] .
red (s[[whilebody]])[[y]] equiv(s[[whilebody]])[[b]] * (s[[whilebody]])[[b]] *
(s[[whilebody]])[[b]] .red ((s[[whilebody]])[[b]] – 1) *
((s[[whilebody]])[[b]] – 1) * ((s[[whilebody]])[[b]] – 1)