Curso Prático
de Métodos Formais
Revisando Pré-Condições e Provando
Refinamentos de Especificações em Z
(Alexandre Mota e Augusto Sampaio)
Tópicos Abordados



Exemplo: A Tabela de Símbolos (TS)
Pré-condições: Estruturando
Provando Refinamentos
– Mesmo Estado
– Estados Diferentes
Exemplo: A Tabela de Símbolos
[VAL,SYM]
Update
D State
s?: SYM
v?: VAL
s? dom st
st’ = st  {s?  v?}
Delete
D State
s?: SYM
s?  dom(st)
st’={s?} st
ST == SYM
VAL
State
st: ST
NotPresent
X State
s?: SYM
rep!: Report
s?  dom(st)
rep!=Symbol_not_present
Report ::= Ok
| Symbol_not_present
^ [rep!:Report | rep!=Ok]
Success =
StDelete ^
= (Delete  Success)  NotPresent
Pré-condição: Estruturando
Disjunções:  - or. Por exemplo, considere StDelete:
pre StDelete  pre Delete  pre NotPresent
A estruturação é realizada a partir do cálculo intermediário
das pré-condições envolvidas. Para o exemplo acima temos:
theorem preStDelete
" State; s?:SYM; v?: VAL  pre Delete  pre NotPresent
Passos da prova:
1. try lemma preStDelete;
2. cases; (cálculos intermediários)
3. prove by reduce;
4. next; (próximo predicado)
5. prove by reduce; (2 objetivo)
6. next; (objetivo OU)
7. prove by reduce; (objetivo final)
Refinamento de Operações
(Mesmo Estado)



Verificar se operações compostas refinam operações
simples;
As obrigações são: a aplicabilidade e a corretude.
Há simplificação dos teoremas pois o esquema Retrieve
é a relação identidade
Delete
StDelete ???
theorem aplicMesmoEstado
pre Delete  pre StDelete
theorem corrMesmoEstado
pre Delete  StDelete  Delete
Estratégia para Refinamento





Os teoremas de refinamento usam as pré-condições
mais de uma vez;
Portanto, neste caso é interessante guardar o resultado;
Desta forma, deve-se calcular as pré-condições;
Armazenar os resultados obtidos como esquemas;
Introduzir estes resultados nas obrigações de prova.
\begin{schema}{Delete}
...
\end{schema}
\begin{schema}{preDeleteRes}
...
\end{schema}
\begin{theorem}{aplicacao}
... preDeleteRes ...
\end{theorem}
Refinamento de Dados
(funcional)


No caso geral, é necessário estabelecer uma relação
entre os dois estados (abstrato e concreto);
Aqui, consideraremos que esta relação é sempre
funcional.
Inicialização:
Cinit  Retr’  Ainit
Aplicabilidade:
pre Aop  Retr  pre Cop
Corretude:
pre Aop  Retr  Cop  Retr’ Aop
Refinamento de Dados (Geral)
Propor um novo estado;
 Propor um esquema Retrieve;
 Propor refinamentos para as operações;
 Construir as obrigações de prova como
teoremas;
 Provar os teoremas.

Refinamento de Dados
(Exemplo 1)
State1
st1: seq(SYM  VAL)
Retrieve1
State
State1
Update1
D State1
s?: SYM
v?: VAL
st = ran st1
s? dom(ran st1)
st1’ = st1 ^ (s?, v?)
A estratégia geral para o cálculo de refinamento é calcular
as pré-condições envolvidas e usar estes resultados nos
teoremas de aplicabilidade e corretude.
Refinamento de Dados
(Exemplo 1 - continuação)



Calcular a pré-condição de Update e de Update1;
Armazenar como esquemas;
Usar esquema em teoremas.
Exemplo: Calcular SymtabA SymtabC, considerando
simplesmente as operações Update e Update1
preUpdateRes
State
s?: SYM
v?: VAL
preUpdate1Res
State1
s?: SYM
v?: VAL
s?  dom st
s?  dom (ran st1)
Refinamento de Dados
(Exemplo 1 - continuação)
theorem inicializacao
Init1 \land Retr1’ \implies Init
theorem aplicacao
preUpdateRes \land Retr1 \implies preUpdate1
theorem corretude
preUpdateRes \land
Retr1 \land
Update1 \land
Retr1’ \implies Update
Refinamento de Dados
(Exemplo 2)
Report ::= Yes | No
Especificação
Abstrata
Especificação
Concreta
State
b: bag IN
State1
s: seq IN
find
X State
n?: IN
rep!: Report
find1
X State1
n?: IN
rep!: Report
n?  dom b
rep! = Yes
n?  ran s
rep! = Yes
Refinamento de Dados
(Exemplo 2 - Escolha do Retr)
Alternativa 1:
Retr1
State
State1
b = items s
Alternativa 2:
Retr2
State
State1
dom b = ran s
" n  dom b  b(n) = #(s |` {n})