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