Z notation
 |
 |
A notação Z (pronunciada zɛd), nomeada dos Axiomas de Zermelo-Fränkel, é uma linguagem de especificação formal usada para descrever e modelar sistemas computacionais. É direcionado à especificação direta de programas de computador e na formulação de testes sobre o comportamento específico do programa.[1]
Z foi originalmente proposta por Jean-Raymond Abrial em 1977 com a ajuda de Steve Schuman e Bertrand Meyer. Z foi mais desenvolvida no Programming Research Group (Grupo de Pesquisa de Programação) em Oxford University (Universidade de Oxford), onde Abrial trabalhou no começo dos anos 80.
Z é baseada na notação matemática padrão usada no axioma da teoria dos conjuntos, cálculos lambda, e lógica predicada de primeira ordem. Todas as expressões na notação Z são tipadas, conseqüentemente desviando alguns dos paradoxos da Teoria Ingênua dos Conjuntos. Z contém um catálogo padronizado (chamado de caixa de ferramentas matemáticas) de funções matemáticas mais freqüentemente usadas e predicados.
Apesar da notação Z usar muitos símbolos não-ASCII, a especificação inclui sugestões para renderizar os símbolos da notação Z em ASCII e em Látex. Uma fonte ttf de Z também está disponível para download.
Padronização A ISO completou a padronização de Z em 2002. Esta padronização pode ser obtida diretamente da ISO.
Ver também
[editar | editar código-fonte]Referências
- ↑ «Z notation». Biblioteca Nacional da Alemanha (em alemão). Consultado em 26 de agosto de 2020
Bibliografia
[editar | editar código-fonte]- J. Michael Spivey (1992). The Z Notation: a reference manual 2nd edition ed. [S.l.]: Prentice Hall International Series in Computer Science. Consultado em 1 de julho de 2008. Arquivado do original em 9 de outubro de 2008
- Jim Davies and Jim Woodcock (1996). Using Z: Specification, Refinement and Proof. [S.l.]: Prentice Hall International Series in Computer Science. ISBN 0-13-948472-8. Consultado em 1 de julho de 2008. Arquivado do original em 27 de junho de 2009
- Jonathan Bowen (1996). Formal Specification and Documentation using Z: A Case Study Approach. [S.l.]: International Thomson Computer Press. ISBN 1-85032-230-9. Consultado em 1 de julho de 2008. Arquivado do original em 9 de abril de 2010
- Jonathan Jacky (1997). The Way of Z: Practical Programming with Formal Methods. [S.l.]: Cambridge University Press. ISBN 0-521-55976-6
Ligações externas
[editar | editar código-fonte]- «The World Wide Web Virtual Library: The Z notation». , por Jonathan Bowen
- «Community Z Tools (CZT) project»
- «Specification proposals by Ian Toyn»
- «ZETA open-source system for development software specifications in Z»
- «HOL-Z open-source proof environment for Z in Isabelle/HOL»
- «Mike Spivey's Fuzz Type-Checker for Z»
- «Z/Eves — A proof checker for the Z notation». (site em alemão mas todos os manuais são em inglês)
