Lenguaje Z
Es un lenguaje formal utilizado en ingeniería del software para la especificación formal de un sistema de cómputo, como una fase previa al desarrollo del código de programa para el mismo en un lenguaje de programación.
Se basa en la teoría de conjuntos, el cálculo lambda y la lógica de primer orden, se definen construcciones denominadas esquemas para describir el espacio de estados del sistema y las operaciones que sobre el mismo se efectúan. En los esquemas se declaran variables y predicados que afectan los valores de las variables declaradas.
El lenguaje Z logró el estándar ISO en el 2002.
CARACTERÍSTICAS
Z es un lenguaje de matriz.
Z es una máquina de lenguaje de programación independiente, lo …ver más…
El lenguaje de esquemas puede ser usado para describir el estado de un sistema y las formas en el cual dicho estado puede cambiar. Además puede ser usado para describir propiedades del sistema y para razonar acerca de posibles refinamientos de un diseño.
Un rasgo característico de Z es el uso de tipos. Cada objeto en el lenguaje matemático tiene un único tipo, representado como un conjunto maximal en la especificación actual. Además de proveer un útil eslabón con la práctica de programación, esta noción de tipos significa que un algoritmo puede ser escrito para controlar el tipo de cada objeto en la especificación; existen varias herramientas de chequeo de tipos que apoyan el uso práctico de Z.
Un tercer aspecto es el uso del lenguaje natural. Usamos matemáticas para exponer el problema, para descubrir soluciones y para probar que el diseño elegido cumple con la especificación. Usamos lenguaje natural para relacionar las matemáticas con los objetos del mundo real; habitualmente este trabajo se consigue parcialmente mediante el nombrado juicioso de las variables pero el comentado adicional es vital. Una especificación bien escrita debería ser perfectamente obvia al lector.
Un cuarto aspecto es refinamiento. Se puede desarrollar un sistema construyendo un modelo de un diseño, usando tipos de datos matemáticos simples para identificar el comportamiento deseado. Luego podemos refinar esta descripción construyendo otro