Notación Z

La notación Z / ˈ z ɛ d / es un lenguaje de especificación formal utilizado para describir y modelar sistemas informáticos. ^[1] Su objetivo es la especificación clara de programas informáticos y sistemas informáticos en general.

Historia

En 1974, Jean-Raymond Abrial publicó "Data Semantics". ^[2] Utilizó una notación que luego se enseñaría en la Universidad de Grenoble hasta fines de la década de 1980. Mientras estaba en EDF ( Électricité de France ), trabajando con Bertrand Meyer , Abrial también trabajó en el desarrollo de Z. ^[3] La notación Z se utiliza en el libro de 1980 Méthodes de programmation . ^[4]

Z fue propuesto originalmente por Abrial en 1977 con la ayuda de Steve Schuman y Bertrand Meyer . ^[5] Fue desarrollado aún más en el Grupo de Investigación de Programación de la Universidad de Oxford , donde Abrial trabajó a principios de los años 1980, habiendo llegado a Oxford en septiembre de 1979.

Abrial ha dicho que Z se llama así "¡porque es el lenguaje definitivo!" ^[6] aunque el nombre " Zermelo " también se asocia con la notación Z a través de su uso de la teoría de conjuntos de Zermelo-Fraenkel .

En 1992, se creó el Grupo de Usuarios Z (ZUG) para supervisar las actividades relacionadas con la notación Z, especialmente reuniones y conferencias. ^[7]

Uso y notación

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 . ^[8] Todas las expresiones en notación Z están tipificadas , evitando así algunas de las paradojas de la teoría de conjuntos ingenua . Z contiene un catálogo estandarizado (llamado el kit de herramientas matemáticas ) de funciones y predicados matemáticos de uso común, definidos utilizando el propio Z. Se amplía con cajas de esquema Z , que se pueden combinar utilizando sus propios operadores, basados en operadores lógicos estándar, y también incluyendo esquemas dentro de otros esquemas. Esto permite que las especificaciones Z se conviertan en especificaciones grandes de una manera conveniente.

Debido a que la notación Z (al igual que el lenguaje APL , mucho antes) utiliza 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 existen codificaciones Unicode para todos los símbolos Z estándar. ^[9]

Normas

La ISO completó un esfuerzo de estandarización Z en 2002. Esta norma ^[10] y una corrección técnica ^[11] están disponibles gratuitamente en la ISO:

la norma está disponible públicamente ^[10] en el sitio ITTF de ISO de forma gratuita y, por separado, está disponible para su compra ^[10] en el sitio de ISO;
El corrigendum técnico está disponible ^[11] en el sitio ISO de forma gratuita.

Otorgar

En 1992, el Laboratorio de Computación de la Universidad de Oxford e IBM recibieron conjuntamente el Premio de la Reina al Logro Tecnológico "por el desarrollo de... la notación Z y su aplicación en el producto IBM Customer Information Control System ( CICS )". ^[12]

Véase también

Grupo de usuarios Z (ZUG)
Proyecto Community Z Tools (CZT)
Otros métodos formales (y lenguajes que utilizan especificaciones formales ):
- 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 objetos para la notación Z
- Alloy , un lenguaje de especificación inspirado en la notación Z y que implementa los principios del Lenguaje de Restricción de Objetos (OCL).
- Verus, una herramienta propietaria creada por Compion, Champaign, Illinois (posteriormente adquirida por Motorola), para su uso en el proyecto UNIX seguro de múltiples niveles iniciado por su división Addamax.
Fastest , una herramienta de prueba basada en modelos para la notación Z.
Lenguaje de modelado unificado , una herramienta de modelado de diseño de sistemas de software de Object Management Group

Referencias

^ Bowen, Jonathan P. (2016). "La notación Z: ¿de dónde viene la causa y hacia dónde va?" (PDF) . Ingeniería de sistemas de software confiables . Apuntes de clase en informática . Vol. 9506. Springer . págs. 103–151. doi :10.1007/978-3-319-29628-9_3. ISBN 978-3-319-29627-2.
^ Abrial, Jean-Raymond (1974), "Semántica de datos", en Klimbie, JW; Koffeman, KL (eds.), Actas de la Conferencia de trabajo de la IFIP sobre gestión de bases de datos , Holanda Septentrional , págs. 1–59
^ Hoare, Tony (2010). Saludos a Bertrand con motivo de su sexagésimo cumpleaños (PDF) . Springer . p. 183. ISBN 978-3-642-15187-3. {{cite book}}: |work=ignorado ( ayuda )
^ Meyer, Bertrand ; Baudoin, Claude (1980), Méthodes de programmation (en francés), Eyrolles
^ Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980), "Un lenguaje de especificación", en Macnaghten, AM; McKeag, RM (eds.), Sobre la construcción de programas , Cambridge University Press , ISBN 0-521-23090-X(describe la versión inicial del lenguaje).
^ Hoogeboom, Hendrik Jan. "Métodos formales en ingeniería de software" (PDF) . Países Bajos: Universidad de Leiden . Consultado el 14 de abril de 2017 .
^ Bowen, Jonathan (julio de 2022). "El grupo de usuarios Z: treinta años después" (PDF) . FACS FACTS . N.º 2022–2. BCS-FACS . págs. 50–56 . Consultado el 3 de agosto de 2022 .
^ Spivey, J. Michael (1992). La notación Z: un manual de referencia . International Series in Computer Science (2.ª ed.). Hemel Hempstead: Prentice Hall . ISBN 978-0139785290.
^ Korpela, Jukka K. "Unicode Explained: Internationalize Documents, Programs, and Web Sites" (Explicación de Unicode: internacionalizar documentos, programas y sitios web). unicode-search.net . Consultado el 24 de marzo de 2020 .
^ abc "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 ) . ISO. 1 de julio de 2002. 196 págs.
^ ab "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 — Corrigendum técnico 1 (PDF) . ISO. 15 de julio de 2007. 12 págs.
^ "Premio de la Reina al Logro Tecnológico 1992". Laboratorio de Computación de la Universidad de Oxford . Archivado desde el original el 2 de diciembre de 2008. Consultado el 17 de octubre de 2021 .

Lectura adicional

Spivey, John Michael (1992). La notación Z: un manual de referencia. International Series in Computer Science (2.ª ed.). Prentice Hall .
Davies, Jim ; Woodcock, Jim (1996). Uso de Z: especificación, refinamiento y demostración. 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). El camino de Z: programación práctica con métodos formales. Cambridge University Press . ISBN 0-521-55976-6.
Ince, DC (1993). Introducción a las matemáticas discretas, especificación formal del sistema y Z. Oxford University Press . doi :10.1093/oso/9780198538370.001.0001. ISBN 9780198538370.

[1] Bowen, Jonathan P. (2016). "La notación Z: ¿de dónde viene la causa y hacia dónde va?" (PDF) . Ingeniería de sistemas de software confiables . Apuntes de clase en informática . Vol. 9506. Springer . págs. 103–151. doi :10.1007/978-3-319-29628-9_3. ISBN 978-3-319-29627-2.

[2] Abrial, Jean-Raymond (1974), "Semántica de datos", en Klimbie, JW; Koffeman, KL (eds.), Actas de la Conferencia de trabajo de la IFIP sobre gestión de bases de datos , Holanda Septentrional , págs. 1–59

[3] Hoare, Tony (2010). Saludos a Bertrand con motivo de su sexagésimo cumpleaños (PDF) . Springer . p. 183. ISBN 978-3-642-15187-3. {{cite book}}: |work=ignorado ( ayuda )

[4] Meyer, Bertrand ; Baudoin, Claude (1980), Méthodes de programmation (en francés), Eyrolles

[5] Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980), "Un lenguaje de especificación", en Macnaghten, AM; McKeag, RM (eds.), Sobre la construcción de programas , Cambridge University Press , ISBN 0-521-23090-X(describe la versión inicial del lenguaje).

[6] Hoogeboom, Hendrik Jan. "Métodos formales en ingeniería de software" (PDF) . Países Bajos: Universidad de Leiden . Consultado el 14 de abril de 2017 .

[zug22-7] Bowen, Jonathan (julio de 2022). "El grupo de usuarios Z: treinta años después" (PDF) . FACS FACTS . N.º 2022–2. BCS-FACS . págs. 50–56 . Consultado el 3 de agosto de 2022 .

[8] Spivey, J. Michael (1992). La notación Z: un manual de referencia . International Series in Computer Science (2.ª ed.). Hemel Hempstead: Prentice Hall . ISBN 978-0139785290.

[9] Korpela, Jukka K. "Unicode Explained: Internationalize Documents, Programs, and Web Sites" (Explicación de Unicode: internacionalizar documentos, programas y sitios web). unicode-search.net . Consultado el 24 de marzo de 2020 .

[Standard-10] "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 ) . ISO. 1 de julio de 2002. 196 págs.

[Corrigendum-11] "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 — Corrigendum técnico 1 (PDF) . ISO. 15 de julio de 2007. 12 págs.

[12] "Premio de la Reina al Logro Tecnológico 1992". Laboratorio de Computación de la Universidad de Oxford . Archivado desde el original el 2 de diciembre de 2008. Consultado el 17 de octubre de 2021 .