Fundamentos de Linguagens de Programação
Nelma Moreira
Departamento de Ciência de Computadores da FCUP
Fundamentos de Linguagens de Programação
Aula 13
Nelma Moreira (DCC-FC)
Fundamentos de Linguagens de Programação
Aula 13
1/9
Semântica axiomática
Exercı́cio
Mostrar que
`p {V}z := x + 1; if z − 1 = 0 then y := 1 else y := z{y = x + 1}
Nelma Moreira (DCC-FC)
Fundamentos de Linguagens de Programação
Aula 13
2/9
Comandos dedutivamente equivalentes
Comandos dedutivamente equivalentes
Dois comando c1 e c2 são dedutivamente equivalentes se para todas as
pré-condições P e todas as pós-condições Q se tem:
`p {P}c1 {Q} se e só se `p {P}c2 {Q}
Exemplo
Mostrar que os seguintes comandos são dedutivamente equivalentes:
1
c ; skip e c
2
c1 ; (c2 ; c3 ) e (c1 ; c2 ); c3
Nelma Moreira (DCC-FC)
Fundamentos de Linguagens de Programação
Aula 13
3/9
Integridade e completude da semântica axiomática
Vamos ver que o sistema `p é ı́ntegro em relação à semântica natural
operacional (analogamente podia-se provar para a semântica
denotacional).
Quanto à completude e no caso de se usar como linguagem de asserções
uma lógica de primeira ordem com aritmética o Teorema de Gödel apenas
permite versões fracas.
Validade
Uma asserção {P}c{Q} é válida se e só se:
∀s ∈ State⊥ , (Ps = V ∧ hc, si → s 0 ) ⇒ Q s 0 = V
e escreve-se |=p {P}c{Q}.
Nelma Moreira (DCC-FC)
Fundamentos de Linguagens de Programação
Aula 13
4/9
Integridade da semântica axiomática
Teorema (Integridade)
Para todas as asserções de correção parcial {P}c{Q},
`p {P}c{Q} implica |=p {P}c{Q}
A demonstração é por indução na árvore de inferência de `p {P}c{Q}.
Caso assp . Suponhamos que `p {P[x 7→ A[[a]]]}x := a{P}. Seja
hx := a, si → s 0 e P[x 7→ A[[a]]] s = P s[x 7→ A[[a]]s] = V.
Temos que provar que P s 0 = V. Por [asssn ] temos que
s 0 = s[x 7→ A[[a]]s], e portanto P s 0 = P s[x 7→ A[[a]]s] = V
Nelma Moreira (DCC-FC)
Fundamentos de Linguagens de Programação
Aula 13
5/9
Integridade da semântica axiomática
Caso skipp . Supomos que `p {P} skip {P} . Seja hskip, si → s 0 .
Como por [skipsn ], s 0 = s o resultado é imediato.
Caso compp . Suponhamos que |=p {P}c1 {R} e |=p {R}c2 {Q} .
Queremos mostrar que |=p {P}c1 ; c2 {Q}. Sejam s e s 00
estados, tal que P s = V e hc1 ; c2 , si → s 00 . Pela regra
[compsn ] existe s 0 tal que
hc1 , si → s 0 e hc2 , s 0 i → s 00
Da hc1 , si → s 0 , P s 0 = V e |=p {P}c1 {R}, temos que
R s 0 = V. De hc2 , s 0 i → s 00 , R s 0 = V e |=p {R}c2 {Q},
temos que Q s 00 = V. Que é o que queriamos.
Nelma Moreira (DCC-FC)
Fundamentos de Linguagens de Programação
Aula 13
6/9
Integridade da semântica axiomática
Caso ifp . Suponhamos que |=p {B[[b]] ∧ P}c1 {Q} e
|=p {¬B[[b]] ∧ P}c2 {Q}.
Para provar que
|=p {P} if b then c1 else c2 {Q}
sejam s e s 0 estados tais que P s = V e
hif b then c1 else c2 , si → s 0 .
Se B[[b]]s = V então por [ifsn ], temos que hc1 , si → s 0 .
Então dado que |=p {B[[b]] ∧ P}c1 {Q}, concluı́mos que
Q s 0 = V.
Analogamente se concluı́, caso B[[b]]s = F.
Nelma Moreira (DCC-FC)
Fundamentos de Linguagens de Programação
Aula 13
7/9
Integridade da semântica axiomática
Caso whilep . Suponhamos que
|=p {B[[b]] ∧ P}c{P}.
(1)
Para provar que |=p {P} while b do c {¬B[[b]] ∧ P}, sejam
s e s 00 estados tais que P s = V e hwhile b do c, si → s 00 .
Temos que mostrar que (¬B[[b]] ∧ P)s 00 = V. Há dois casos
a considerar, consoante [whilesn ]. Se B[[b]]s = F então
s 00 = s e (¬B[[b]] ∧ P)s 00 = V.
Senão, B[[b]]s = V e existe s 0 tal que hc, si → s 0 e
hwhile b do c, s 0 i → s 00 .
Temos que (B[[b]] ∧ P)s = V e pela hipótese (1) temos que
P s 0 = V. Aplicando a hipótese de indução a
hwhile b do c, s 0 i → s 00 , temos que (¬B[[b]] ∧ P)s 00 = V,
como queriamos.
Nelma Moreira (DCC-FC)
Fundamentos de Linguagens de Programação
Aula 13
8/9
Integridade da semântica axiomática
Caso consp . Suponhamos que
|=p {P 0 }c{Q 0 }, P ⇒ P 0 , e Q 0 ⇒ Q.
(2)
Para provar que |=p {P}c{Q}, sejam s e s 0 tal que P s = V
e hc, si → s 0 .pause
Como P s = V e P ⇒ P 0 então P 0 s = V e pela hipótese (2),
Q 0 s 0 = V. Mas como Q 0 ⇒ Q, temos que Q s 0 = V, como
queriamos.
Nelma Moreira (DCC-FC)
Fundamentos de Linguagens de Programação
Aula 13
9/9