Exemplos de especificacoes em Z

Em resposta a um visitante do blog, estou adicionando um exemplo de especificacoes em Z que usei durante minha experiencia com Z/Eves.

1. IBM CIC'S Browser Component


Este mecanização corresponde ao exemplo discutido no post

Technical Report No 257 by IBM (A specification, refinement and Verification Using Z Schema Calculus)

Abraco,
Diego Dias

Technical Report No 257 by IBM (A specification, refinement and Verification Using Z Schema Calculus)

The document made available on this post was recovered during the moving from Claremont Tower to the Urban Sciences Building while I was at Newcastle University. Leo Freitas, one of the co-authors of the paper "Mecanizando o componente de navegação do IBM’s CICS: um experimento do Grande Desafio" found a paper copy of this document and gave. It was part of my first foray into the mechanisation of formal theories using theorem provers, and since it is the basis for the paper mentioned above, and it is unrestricted, I decided to make it available!

A specification, refinement and Verification Using Z Schema Calculus

Enjoy it!