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!