Teoremas de equivalência

Sejam P e Q schemas equivalentes. Para mostrar a equivalência entre estes schemas usando Z/Eves deve ser provado o predicado:

P \iff Q

Uma forma tipica de mostrar esta equivalência é dividi-la em duas partes:

1. P \implies Q
2. Q \implies P

Para transformar o predicado P \iff Q nos predicados 1 e 2, o usuário pode entrar com os seguintes comandos de prova:

slip P
rewrite
cases
rewrite

Neste ponto o predicado 1 foi obtido.

next
split Q
rewrite

Neste ponto o predicado 2 foi obtido.

Agora, é somente provar os predicados. Para alternar entre eles utiliza-se o comando next.

Mecanizando o componente de navegação do IBMs CICS

O site do MEFES (Métodos Formais em Engenharia de Software) está hospedado em https://wiki.dcc.ufba.br/MEFES/. Neste endereço está disponível para download o artigo "Mecanizando o componente de navegação do IBMs CICS: um experimento do Grande Desafio". O artigo foi publicado na IX ERBASE e foi premiado com o terceiro lugar no Workshop de Trabalhos de Iniciação Científica e de Graduação (WTICG). A ERBASE é um evento regional promovido anualmente pela Sociedade Brasileira de Computação.

Como citar:

DIAS, D. M. ; Robson Silva ; Leo Freitas ; Adolfo Duran . Mecanizando o componente de navegação do IBMs CICS: um experimento do Grande Desafio. In: IX Escola Regional de Computação Bahia - Alagoas - Sergipe, 2009, Ilheus. Anais da IX ERBASE, 2009.