stringtranslate.com

Notación Z

Un ejemplo de una especificación formal (en español) utilizando la notación Z, con cuadros de esquema nombrados, incluyendo declaraciones y predicados

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:

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

Referencias

  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 .
  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 .
  10. ^ 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.
  11. ^ 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.
  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 .

Lectura adicional