Notación Z - Z notation

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

En 1974, Jean-Raymond Abrial publicó "Data Semantics". Usó una notación que luego se enseñaría en la Universidad de Grenoble hasta finales de los años ochenta. Mientras estaba en EDF ( Électricité de France ), Abrial escribió notas internas sobre Z. La notación Z se usa en el libro de 1980 Méthodes de programmation .

Z fue propuesto originalmente por Abrial en 1977 con la ayuda de Steve Schuman y Bertrand Meyer . Fue desarrollado aún más 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!" aunque el nombre " Zermelo " también se asocia con la notación Z mediante el 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 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.

Estándares

ISO completó un esfuerzo de estandarización Z en 2002. Esta norma y una corrección técnica están disponibles en ISO free:

  • el estándar está disponible públicamente en el sitio de ISO ITTF de forma gratuita y, por separado, está disponible para su compra en el sitio de ISO;
  • la corrección técnica está disponible gratuitamente en el sitio de ISO.

Otorgar

En 1992, “ Su Majestad la Reina [se mostró] gratamente complacida de aprobar la recomendación del Primer Ministro de que el Premio de la Reina por Logros Tecnológicos debería ser otorgado este año al Laboratorio de Computación de la Universidad de Oxford . Oxford University Computing Laboratory [ganado] el premio conjuntamente con IBM Reino Unido Laboratories Limited para el desarrollo de un método de programación basado en elemental teoría de conjuntos y la lógica conocida como la notación Z , y su aplicación en el IBM Information Control System (CICS) de los clientes de productos . "

Ver también

  • 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

Otras lecturas