Notación Z
La notación Z ( notación Z en inglés , pronunciada /zɛd/) es un lenguaje de especificación formal utilizado para describir y modelar programas y su verificación formal .
Propuesto por Jean -Raymond Abrial en 1977, Steve Schuman y Bertrand Meyer participaron en el desarrollo [1 ] .
Basado en la notación matemática estándar utilizada en la teoría axiomática de conjuntos , el cálculo lambda y la lógica de predicados de primer orden . Se eligen expresiones válidas en notación Z para evitar las paradojas de la teoría axiomática de conjuntos . También contiene un catálogo estandarizado de predicados y funciones matemáticas de uso frecuente.
Aunque la notación usa muchos caracteres fuera del conjunto ASCII , la especificación permite que las expresiones se escriban completamente en ASCII oa través de LaTeX , hay una fuente especializada para admitirlo (fuente Z ttf) [2] .
En 2002, la Organización Internacional de Normalización completó el proceso de estandarización de la notación Z [3] .
Hay una extensión orientada a objetos Object-Z [4] .
Notas
- ↑ Jean-Raymond Abrial, Stephen A. Schuman y Bertrand Meyer: A Specification Language , en On the Construction of Programs , Cambridge University Press, eds. A.M. Macnaghten y R.M. McKeag, 1980 (describe la primera versión del lenguaje). ISBN 0-521-23090-X
- ↑ GoldenWeb.it - Descarga gratuita de fuentes True Type - Zed.ttf . Consultado el 7 de noviembre de 2008. Archivado desde el original el 13 de noviembre de 2007.
- ↑ Tecnología de la información - Notación de especificación formal Z - Sintaxis, sistema de tipos y semántica . — ISO/CEI 13568:2002 . - 2002. - Pág. 196.
- ↑ Duke, R. y Rose, G. (2000). Especificación formal orientada a objetos usando object-z. Pilares de la Computación. Macmillan.
Literatura
- J. Michael Spivey. La notación Z: un manual de referencia (neopr.) . — 2ª edición. - Prentice Hall International Series in Computer Science, 1992. Archivado el 9 de octubre de 2008 en Wayback Machine .
- Jim Davies y Jim Woodcock. Usando Z : especificación, refinamiento y prueba . - Serie Internacional Prentice Hall en Informática, 1996. - ISBN 0-13-948472-8 . Archivado el 27 de junio de 2009 en Wayback Machine .
- Jonathan Bowen. Especificación formal y documentación utilizando Z: un enfoque de estudio de caso . - International Thomson Computer Press, 1996. - ISBN 1-85032-230-9 . Archivado el 9 de abril de 2010 en Wayback Machine .
- Jonathan Jacky. El Camino de Z : Programación Práctica con Métodos Formales . - Prensa de la Universidad de Cambridge , 1997. - ISBN 0-521-55976-6 .
 En catálogos bibliográficos |
|---|