Notación Z

Ejemplo de una especificación formal (en español) usando la notación Z, con cajas de esquemas nombradas, incluyendo declaraciones y predicados.

La notación Z es un lenguaje de especificación formal utilizado para describir y modelar sistemas informáticos. Está dirigido a la especificación clara de programas informáticos y sistemas informáticos 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 80. Mientras trabajaba en EDF (Électricité de France), trabajando con Bertrand Meyer, Abrial también trabajó en el desarrollo de 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. 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, habiendo llegado a Oxford en septiembre de 1979.

Abrial ha dicho que Z se llama así "¡Porque es el idioma definitivo!" 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.

En 1992, se estableció el Grupo de Usuarios Z (ZUG) para supervisar las actividades relacionadas con la notación Z, especialmente reuniones y conferencias.

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. Todas las expresiones en notación Z se escriben, evitando así algunas de las paradojas de la teoría de conjuntos ingenua. Z contiene un catálogo estandarizado (llamado el juego de herramientas matemáticas) de funciones y predicados matemáticos de uso común, definidos usando Z mismo. Se amplía con cuadros de esquema Z, que se pueden combinar utilizando sus propios operadores, basados en operadores lógicos estándar, y también mediante la inclusión de 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) 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. Este estándar y un corrigendum técnico están disponibles de forma gratuita en ISO:

• el estándar está disponible públicamente desde el sitio ISO ITTF de forma gratuita y, por separado, disponible para la compra del sitio ISO;
• el corrigendum técnico está disponible desde el sitio ISO de forma gratuita.

Premio

En 1992, el Laboratorio de Computación de la Universidad de Oxford recibió el premio Queen's Award for Technological Achievement por su desarrollo conjunto con IBM de la notación Z.