Curso Prático
de Métodos Formais
Calculando Pré-Condições e Provando
Propriedades de Especificações em Z
(Alexandre Mota e Augusto Sampaio)
Tópicos Abordados





O Provador de Teoremas Z-EVES
A Tabela de Símbolos (TS)
Cálculo de Pré-condições: Simples e Compostas
Provando Propriedades
Propriedades Complexas
O Provador de Teoremas
Z-EVES
Interpretador Lisp executado no Windows
 Carrega-se uma especificação através da
seqüência: FileImport (Menu)
 O comando reset; (digitado) é usado para
poder carregar outra especificação
 Finalização é feita através de FileQuit
(Menu) ou quit; (digitado)

Exemplo: A Tabela de Símbolos
[VAL,SYM]
Update
D State
s?: SYM
v?: VAL
st’ = st  {s?  v?}
Delete
D State
s?: SYM
s?  dom(st)
st’={s?} st
ST == VAL
SYM
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
Calculando Pré-condições

try " State;In?:TIn  pre Schema-Name;
(Objetivo)
Calculando a pré-condição de Delete:
=> try \forall State; s?:SYM @ \pre Delete;
=> prove by reduce;
st \in SYM \pfun VAL \\
\land s? \in SYM \\
\implies s? \in \dom st

+ VAL
st  SYM 
^ s?  SYM
 s?  dom st
Exercício: Calcular a pré-condição de Update e de NotPresent
Pré-condição de Esquemas
Compostos
Conjunções:  - and. Por exemplo, considere StUpdate:
pre StUpdate  pre Update
Disjunções:  - or. Por exemplo, considere StDelete:
pre StDelete  pre Delete  pre NotPresent
pre StDelete
\begin{theorem}{preDelete_Or_preNotPresent}
(Resultado de pre Delete) \lor \\
(Resultado de pre NotPresent)
\end{theorem}
Finalmente, try lemma preDelete_Or_preNotPresent;
Exercício: Calcular a pré-condição de StLookUp
Provando Propriedades
Expressa-se a propriedade desejada
através de um teorema;
 Usa-se o comando try lemma Teorema;
 Usa-se o comando prove by reduce;

Exemplo: Provar que o Esquema StLookUp resulta em Ok,
quando s?  dom st.
\begin{theorem}{LookUpOk}
\forall StLookUp | s? \in \dom st @ rep!=Ok
\end{theorem}
1. try lemma LookUpOk;
2. prove by reduce;
Provando Propriedades
Exercício 1: Provar que a composição
seqüencial de Update com Delete não
altera o estado do sistema quando s?
incluído for o mesmo removido.
 Exercício 2: Provar que a aplicação de
Delete quando s?  dom st resulta em um
estado final indefinido.

Propriedades Complexas

As vezes o Z-EVES não consegue reduzir
um predicado automaticamente, então:
–
–
–
–
Uso de teoremas do Z-EVES;
Criação de novos teoremas;
Uso de comandos especiais;
etc.
Teoremas do Z-EVES
Z-EVES vem com um conjunto de
teoremas (arquivo ToolKit.zed);
 Usa-se o comando apply teorema;
 Em seguida, o comando prove.

Exemplo: Pode-se remover o operador de power set de um
predicado aplicando o teorema inPower.
=> apply inPower;
=> prove;
Criação de Teoremas

A introdução de teoremas é importante:
– Os teoremas do Z-EVES são insuficientes;
– Reduzir o número de passos de uma prova.
Introduz-se um teorema através do ambiente
theorem;
 Teoremas automáticos são grules(reescrita);

\begin{theorem}{grule select_2_1}
(x,y).1 = x
\end{theorem}
Comandos Especiais
O comando split serve para criar um
predicado do tipo IF/THEN/ELSE que
permite maiores reduções;
 O comando cases serve para dividir um
prova em mais de uma parte. Usa-se com
o comando next que passa para a
próxima parte da prova;
 O comando instantiate permite informar
ao Z-EVES sobre o valor de um objeto;
 O manual contém outros comandos.

Conclusão
Calcular a pré-condição de StDelete
diretamente, ou seja, try pre StDelete;
 Miscelânea de comandos: apply inPower,
split predicado, etc.
