Lenguaje Z

En el mismo se definen las variables: contactos (como el conjunto de nombres cuyos cumpleaños están agendados – subconjunto de todos los nombres - ) y cumple como una función parcial con dominio en el conjunto NOMBRE e imagen en el conjunto FECHA; en la siguiente parte del esquema se define una condición o invariante del sistema, que en este caso indica que el conjunto contactos es igual al dominio de la función cumple.

Los siguientes esquemas definen las operaciones que se realizan sobre el sistema: El esquema AgregarCumple especifica la operación de agregar un nuevo cumpleaños, la letra griega delta delante del nombre del esquema principal, indica que luego de esta operación se producirá un cambio de estado, luego se declaran dos variables: nombre?

NO deben pertenecer al conjunto contactos y que el estado inmediato posterior del conjunto cumple (cumple') es igual al estado anterior unión la upla conformada por el nombre y la fecha ingresadas.

), en este caso la letra griega theta delante del nombre del esquema principal, denota que esta operación no producirá un cambio de estados.

Finalmente el esquema Recordatorio especifica la operación que dada una fecha, el sistema nos devuelve el conjunto de los cumpleaños que ocurren en la misma, como puede verse tampoco modifica el estado del sistema y la condición indica que la variable de salida tarjetas!