De Wikipedia, la enciclopedia libre
Saltar a navegación Saltar a búsqueda
Un ejemplo de una especificación formal (en español) usando la notación Z.

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 ]

  1. ^ 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
  2. ^ Meyer, Bertrand ; Baudoin, Claude (1980), Méthodes de programmation (en francés), Eyrolles
  3. ^ 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).
  4. ^ Hoogeboom, Hendrik Jan. "Métodos formales en ingeniería de software" (PDF) . Holanda: Universidad de Leiden . Consultado el 14 de abril de 2017 .
  5. ^ Korpela, Jukka K. "Explicación de Unicode: internacionalizar documentos, programas y sitios Web" . unicode-search.net . Consultado el 24 de marzo de 2020 .
  6. ^ 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.
  7. ^ 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.