stringtranslate.com

notación Z

Un ejemplo de especificación formal usando 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] Está dirigido a la especificación clara de programas informáticos y sistemas informáticos en general.

Historia

En 1974, Jean-Raymond Abrial publicó "Semántica de datos". [2] Utilizó una notación que luego se enseñaría en la Universidad de Grenoble hasta finales de los años 1980. Mientras estuvo 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 Méthodes de programmation de 1980 . [4]

Z fue propuesto originalmente por Abrial en 1977 con la ayuda de Steve Schuman y Bertrand Meyer . [5] Se desarrolló aún más en el Grupo de Investigación en Programación de la Universidad de Oxford , donde Abrial trabajó a principios de la década 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 definitivo!" [6] 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 .

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ática , 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 ingenua teoría de conjuntos . Z contiene un catálogo estandarizado (llamado kit de herramientas matemáticas ) de funciones y predicados matemáticos de uso común, definidos usando el propio Z. Se complementa con cuadros 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 manera conveniente.

Debido a que la notación Z (al igual que el lenguaje APL , mucho antes) utiliza muchos símbolos no ASCII , la especificación incluye sugerencias para representar los símbolos de notación Z en ASCII y LaTeX . También existen codificaciones Unicode para todos los símbolos Z estándar. [9]

Estándares

ISO completó un esfuerzo de estandarización Z en 2002. Esta norma [10] y un corrigendum técnico [11] están disponibles en 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]

Ver también

Referencias

  1. ^ Bowen, Jonathan P. (2016). "La notación Z: ¿De dónde viene la causa y hacia dónde va el curso?" (PDF) . Ingeniería de sistemas de software confiables . Apuntes de conferencias sobre informática . vol. 9506. Saltador . 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 del 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) . Saltador . pag. 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 anterior del idioma).
  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) . HECHOS FACS . Núm. 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 . Serie Internacional de Ciencias de la Computación (2ª ed.). Hemel Hempstead: Prentice Hall . ISBN 978-0139785290.
  9. ^ Korpela, Jukka K. "Explicación de Unicode: internacionalización de documentos, programas y sitios web". Unicode-search.net . Consultado el 24 de marzo de 2020 .
  10. ^ a b "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.
  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 - Corrección técnica 1 (PDF) . YO ASI. 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 .

Otras lecturas