Hispanopedia Wiki
Articulo de referencia

notación Z

Un ejemplo de una especificación formal (en español) utilizando la notación Z, con cuadros de esquema con nombre, incluyendo declaraciones y predicados. La notación Z / ˈ z ɛ d ...

Hispanopedia WikiContenido en espanolLectura gratuita

Un ejemplo de una especificación formal (en español) utilizando la notación Z, con cuadros de esquema con nombre, 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 basados ​​en computadoras en general.

Historia

Jean-Raymond Abrial , el principal creador de la notación Z.

En 1974, Jean-Raymond Abrial [ 2 ] publicó "Semántica de datos". [ 3 ] Utilizó una notación que posteriormente se enseñaría en la Universidad de Grenoble hasta finales de la década de 1980.

Mientras trabajaba en EDF ( Électricité de France ), junto a Bertrand Meyer , Abrial también colaboró ​​en el desarrollo de Z. [ 4 ] Z fue propuesta originalmente por Abrial en 1977 con la ayuda de Steve Schuman y Bertrand Meyer . [ 5 ] La notación Z se utiliza en el libro Méthodes de programmation de 1980. [ 6 ]

Z se desarrolló aún más en el Grupo de Investigación de Programación de la Universidad de Oxford , donde Abrial trabajó a principios de la década de 1980 con investigadores como Bernard Sufrin e Ib Holm Sørensen (1949-2012), [ 7 ] habiendo llegado a Oxford en septiembre de 1979. [ 8 ] Sørensen recibió un doctorado de la Universidad de Oxford en 1981 por una investigación temprana basada en Z. [ 9 ] Impartió los primeros cursos de notación Z en Oxford [ 10 ] y estableció la serie de reuniones de usuarios de Z, inicialmente en Oxford. [ 11 ]

Ib Holm Sørensen dirigió el Proyecto de Procesamiento de Transacciones en la Universidad de Oxford desde su inicio en 1982 (posteriormente renombrado como "Proyecto CICS", [ 12 ] ), en colaboración con IBM Hursley . [ 13 ] El proyecto especificó formalmente partes del software de procesamiento de transacciones CICS de IBM utilizando la notación Z. Esto ganó un Premio de la Reina al Logro Tecnológico en 1992. [ 14 ] [ 15 ] Como parte del proyecto CICS, Sørensen extendió el Lenguaje de Comandos Protegidos de Edsger Dijkstra al permitir el uso de la notación de esquema Z como comandos abstractos. [ 16 ] Estas ideas fueron formalizadas posteriormente por Carroll Morgan en su cálculo de refinamiento . [ 16 ]

Carroll Morgan añadió los cuadros de esquema Z para la estructuración de especificaciones más extensas. [ 17 ] Ian Hayes editó el libro Specification Case Study de 1987 sobre el uso de Z (2.ª edición publicada en 1993), [ 18 ] con contribuciones de Morgan, Sørensen, Sufrin y otros. Mike Spivey produjo un estándar de facto para Z en forma de libro en 1989 (2.ª edición, 1992). [ 19 ]

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

Uso y notación

Z se basa 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 . [ 19 ] Todas las expresiones en notación Z están tipadas , evitando así algunas de las paradojas de la teoría ingenua 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 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. [ 17 ] Esto permite construir especificaciones Z en especificaciones grandes de manera conveniente.

Grupo de Usuarios Z

En 1985, Ib Sørensen impulsó una serie de reuniones de usuarios de Z, inicialmente en Rewley House en Oxford . [ 11 ] En 1992, se estableció el Grupo de Usuarios de Z (ZUG) en una de estas reuniones para supervisar las actividades relacionadas con la notación Z, especialmente reuniones y conferencias. [ 11 ] El ZUG continuó organizando talleres/reuniones regulares de usuarios de Z (ZUM). Posteriormente, cuando comenzaron a celebrarse fuera del Reino Unido, se las conoció como la Conferencia Internacional de Usuarios de Z. Más tarde, estas conferencias se combinaron para abarcar también el método B , pasando a llamarse Conferencia Internacional de Usuarios de B y Z (ZB).

Estándares

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

  • La norma está disponible públicamente [ 21 ] de forma gratuita en ISO ITTF y, por separado, está disponible para su compra [ 21 ] en el sitio de ISO;
  • La corrección técnica está disponible [ 22 ] gratuitamente en ISO.

Debido a que la notación Z utiliza muchos símbolos que no son ASCII , la especificación incluye sugerencias para representar los símbolos de la notación Z en ASCII y en LaTeX . También existen codificaciones Unicode para todos los símbolos Z estándar. [ 23 ]

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 )". [ 24 ]

Lecturas adicionales

  • Spivey, John Michael (1992). La notación Z: un manual de referencia . Serie internacional en ciencias de la computación (2.ª  ed.). Prentice Hall . Archivado del original el 8 de diciembre de 2019. Recuperado el 24 de marzo de 2020 .
  • Davies, Jim ; Woodcock, Jim (1996). Uso de Z: Especificación, refinamiento y prueba . Serie internacional en ciencias de la computación. Prentice Hall. ISBN 0-13-948472-8Archivado del original el 5 de abril de 2007. Consultado el 22 de marzo de 2006 .
  • Bowen, Jonathan (1996). Especificación y documentación formales mediante Z: Un estudio de caso . International Thomson Computer Press, International Thomson Publishing . ISBN 1-85032-230-9.
  • Jacky, Jonathan (1997). El método 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, la especificación formal de sistemas y Z. Oxford University Press . doi : 10.1093/oso/9780198538370.001.0001 . ISBN 978-0198538370.

Véase también

Referencias

  1. ↑ Bowen, Jonathan P. (2016). "La notación Z: ¿De dónde proviene la causa y hacia dónde se dirige?" (PDF) . Ingeniería de sistemas de software confiables . Notas de clase en ciencias de la computación . Vol. 9506. Springer . págs. 103–151 . doi : 10.1007/978-3-319-29628-9_3 . ISBN   978-3-319-29627-2.
  2. ↑ Bowen, Jonathan P. ; Habrias, Henri (abril–junio 2025). "Jean-Raymond Abrial: Una biografía científica de un pionero de los métodos formales". IEEE Annals of the History of Computing . 48 (2). IEEE Computer Society : 71– 80. arXiv : 2604.07353 . doi : 10.1109/MAHC.2026.3685515 .
  3. ↑ 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 , North-Holland , págs. 1–59 
  4. ↑ Hoare, Tony (2011). «Felicitaciones a Bertrand con motivo de su sexagésimo cumpleaños» (PDF) . En Nanz, Sebastian (ed.). El futuro de la ingeniería de software . Springer . pp. 183–184 . doi : 10.1007/978-3-642-15187-3 . ISBN  978-3-642-15187-3.
  5. ↑ Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980), "A Specification Language", en Macnaghten, AM; McKeag, RM (eds.), On the Construction of Programs , Cambridge University Press , ISBN 0-521-23090-X(describe una versión temprana del idioma).
  6. ↑ Meyer, Bertrand ; Baudoin, Claude (1980), Méthodes de programmation (en francés), Eyrolles
  7. ↑ Bowen, Jonathan (julio de 2022). "Ib Holm Sørensen: Diez años después" (PDF) . FACS FACTS ( 2022–2 ). BCS-FACS : 41–49 . Recuperado el 1 de junio de 2026 .
  8. ↑ Sufrin, Bernard (enero de 2026). "Recuerdos de Jean-Raymond Abrial en Oxford, los Alpes y París" (PDF) . FACS FACTS . 2026 (1). BCS : 66–78 .
  9. ↑ Sørensen, Ib Holm (1981). Temas en especificación y diseño de programas: especificación y diseño de sistemas distribuidos. Archivado el 31 de julio de 2022 en Wayback Machine (DPhil). Reino Unido: Wolfson College , Universidad de Oxford .
  10. ↑ Woodcock, Jim ; Davies, Jim (1996). «Agradecimientos». Uso de Z: Especificación, refinamiento y prueba . Serie internacional en ciencias de la computación. Prentice Hall . ISBN 0-13-948472-8.
  11. 1 2 3 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 . Recuperado el 3 de agosto de 2022 .  
  12. ↑ Fitzgerald, JS (octubre de 2006). Perspectivas sobre los métodos formales en los últimos 25 años . Serie de informes técnicos. Vol. CS-TR-983. Reino Unido: Universidad de Newcastle .
  13. ↑ Hayes, Ian (1993). «Prefacio a la primera edición». Estudios de caso de especificación. Serie internacional en ciencias de la computación (2.ª ed.). Prentice Hall. ISBN 978-0-13-832544-2.
  14. ↑ King, Steve (1993). "El uso de Z en la reestructuración de IBM CICS". En Hayes, Ian (ed.). Estudios de caso de especificación . Serie internacional en ciencias de la computación (2.ª ed.). Prentice Hall . págs. 202-213. ISBN 978-0-13-832544-2.
  15. ↑ "Prof Jim Woodcock, FREng" Archivado el 3 de octubre de 2022 en Wayback Machine . Reino Unido: Universidad de York .
  16. 1 2 Hayes, Ian J.; King, Steve (2021). "11.9 Influencia de la industria en la investigación". En Jones, Cliff B .; Misra, Jayadev (eds.). Teorías de la programación: La vida y obra de Tony Hoare . Association for Computing Machinery . págs. 266–267. ISBN 978-1-4503-8728-6.
  17. 1 2 Woodcock, JCP (enero de 1989). "Estructuración de especificaciones en Z" (PDF) . Software Engineering Journal . 4 (1). IEE : 51–66. doi : 10.1049/sej.1989.0007 .
  18. ↑ Hayes, Ian, ed. (1993). Specification Case Studies Archived 20 June 2015 at the Wayback Machine . International Series in Computer Science (2nd ed.). Prentice Hall . ISBN 978-0-13-832544-2.
  19. 1 2 Spivey, J. Michael (1992). La notación Z: un manual de referencia . Serie internacional en ciencias de la computación (2.ª ed.). Hemel Hempstead: Prentice Hall . ISBN  978-0139785290.
  20. ↑ 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 .
  21. 1 2 3 "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áginas.
  22. 1 2 "ISO/IEC 13568:2002/Cor.1:2007". Tecnología de la información — Z Notación de especificación formal — Sintaxis, sistema de tipos y semántica — Corrección técnica 1 (PDF) . ISO. 15 de julio de 2007. 12 págs.
  23. ↑ Korpela, Jukka K. "Unicode explicado: internacionalizar documentos, programas y sitios web" . unicode-search.net . Archivado del original el 24 de marzo de 2020. Consultado el 24 de marzo de 2020 .
  24. ↑ "Premio de la Reina a los Logros Tecnológicos 1992" . Laboratorio de Informática de la Universidad de Oxford . Archivado del original el 2 de diciembre de 2008. Consultado el 17 de octubre de 2021 .