La notación Z / z ɛ d / es un formal de lenguaje de especificación se usa para describir y modelado de sistemas de computación. Está dirigido a la especificación clara de programas de computadora y sistemas basados en computadora en general.
Historia [ editar ]
En 1974, Jean-Raymond Abrial publicó "Data Semantics". [1] Usó una notación que luego se enseñaría en la Universidad de Grenoble hasta finales de la década de 1980. Mientras estaba en EDF ( Électricité de France ), Abrial escribió notas internas sobre Z. [ cita requerida ] La notación Z se usa en el libro de 1980 Méthodes de programmation . [2]
Z fue propuesto originalmente por Abrial en 1977 con la ayuda de Steve Schuman y Bertrand Meyer . [3] Se desarrolló más a fondo en el Grupo de Investigación de Programación en la Universidad de Oxford , donde Abrial trabajó a principios de 1980, después de haber llegado a Oxford en septiembre de 1979.
Abrial ha dicho que Z se llama así "¡Porque es el lenguaje supremo!" [4] aunque el nombre " Zermelo " también está asociado con la notación Z mediante el uso de la teoría de conjuntos de Zermelo-Fraenkel .
Uso y notación [ editar ]
Z se basa en la notación matemática estándar utilizada en la teoría de conjuntos axiomáticos , el cálculo lambda y la lógica de predicados de primer orden . Todas las expresiones en notación Z están escritas , evitando así algunas de las paradojas de la teoría de conjuntos ingenua . Z contiene un catálogo estandarizado (llamado kit de herramientas matemáticas ) de funciones y predicados matemáticos de uso común, definidos utilizando el propio Z.
Debido a que la notación Z (al igual que el lenguaje APL , mucho antes) usa muchos símbolos que no son ASCII , la especificación incluye sugerencias para representar los símbolos de notación Z en ASCII y en LaTeX . También hay codificaciones Unicode para todos los símbolos Z estándar. [5]
Estándares [ editar ]
ISO completó un esfuerzo de estandarización Z en 2002. Esta norma [6] y una corrección técnica [7] están disponibles en ISO free:
- la norma está disponible públicamente [6] en el sitio de la ITTF de ISO de forma gratuita y, por separado, está disponible para su compra [6] en el sitio de ISO;
- la corrección técnica está disponible [7] en el sitio de ISO de forma gratuita.
Ver también [ editar ]
- Grupo de usuarios Z (ZUG)
- Proyecto Community Z Tools (CZT)
- Otros métodos formales (y lenguajes que utilizan especificaciones formales ):
- FDM (Metodología de desarrollo formal), que gira en torno a los sub-lenguajes de especificación Ina Jo e Ina Flo, bastante populares en las décadas de 1980 y 1990
- VDM-SL , la principal alternativa a Z
- Método B , desarrollado por Jean-Raymond Abrial (creador de la notación Z)
- Z ++ y Object-Z : extensiones de objeto para la notación Z
- Alloy , un lenguaje de especificación inspirado en la notación Z e implementando los principios del Object Constraint Language (OCL).
- Verus, una herramienta patentada construida por Compion, Champaign, Illinois (luego comprada por Motorola), para su uso en el proyecto UNIX seguro multinivel iniciado por su división Addamax.
- Fastest es una herramienta de prueba basada en modelos para la notación Z.
Referencias [ editar ]
- ^ Abrial, Jean-Raymond (1974), "Semántica de datos", en Klimbie, JW; Koffeman, KL (eds.), Actas de la Conferencia de trabajo de IFIP sobre gestión de bases de datos , Holanda Septentrional , págs. 1-59
- ^ Meyer, Bertrand ; Baudoin, Claude (1980), Méthodes de programmation (en francés), Eyrolles
- ^ Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980), "A Specification Language", en Macnaghten, AM; McKeag, RM (eds.), Sobre la construcción de programas , Cambridge University Press , ISBN 0-521-23090-X (describe la primera versión del idioma).
- ^ Hoogeboom, Hendrik Jan. "Métodos formales en ingeniería de software" (PDF) . Holanda: Universidad de Leiden . Consultado el 14 de abril de 2017 .
- ^ Korpela, Jukka K. "Explicación de Unicode: internacionalizar documentos, programas y sitios Web" . unicode-search.net . Consultado el 24 de marzo de 2020 .
- ^ a b c "ISO / IEC 13568: 2002" . Tecnología de la información - Notación de especificación formal Z - Sintaxis, sistema de tipos y semántica ( PDF comprimido ) . YO ASI. 1 de julio de 2002. 196 págs.
- ^ a b "ISO / IEC 13568: 2002 / Cor.1: 2007". Tecnología de la información - Notación de especificación formal Z - Sintaxis, sistema de tipos y semántica - Corrección técnica 1 (PDF) . YO ASI. 15 de julio de 2007. 12 págs.
Lectura adicional [ editar ]
- Spivey, John Michael (1992). La notación Z: un manual de referencia . Serie Internacional en Ciencias de la Computación (2ª ed.). Prentice Hall .
- Davies, Jim ; Woodcock, Jim (1996). Usando Z: Especificación, Refinamiento y Prueba . Serie Internacional en Ciencias de la Computación. Prentice Hall. ISBN 0-13-948472-8.
- Bowen, Jonathan (1996). Especificación formal y documentación utilizando Z: un enfoque de estudio de caso . International Thomson Computer Press, International Thomson Publishing . ISBN 1-85032-230-9.
- Jacky, Jonathan (1997). The Way of Z: Programación práctica con métodos formales . Prensa de la Universidad de Cambridge . ISBN 0-521-55976-6.