|
Object-ZObject-Z es una extensión orientada a objetos de la notación Z y fue desarrollado en la Universidad de Queensland en Australia. Notación Z es un idioma para la especificación formal de sistemas informáticos. Diferencias entre Z y Object-ZObject-Z añade a Z formas de expresar conceptos del paradigma orientado a objetos, sobre todo clases, polimorfismo y herencia. Eso permite la formalización de sistemas que consisten de un conjunto de objetos que comunican entre sí. Object-Z introduce además interfaces de los clases, quiere decir formas de utilizar las clases desde afuera. Eso está realizado con listas de visibilidad (visibility lists) que determinan cuales de las variables o esquemas se pueden acceder desde afuera. En Z se asume que todos los esquemas se pueden acceder desde afuera así que no se pueden describir métodos que solo sirven para otros métodos dentro de la clase. Z permite definir cuales de los esquemas describen métodos que cambian el estado del sistema y cuales no lo cambian (por ejemplo porque solo retornan una variable) con los símbolos Δ y Ξ. Para un esquema que cambia el estado hay que definir el valor posterior para todas las variables del sistema. Esto fue cambiado en Object-Z. Ahí se puede definir para cada esquema cuales variables cambia. Un esquema que no cambia ningún variable corresponde a los esquemas 'Ξ' de Z. Eso es una gran ventaja en clases complejas con esquemas que cambian pocas variables. Esos esquemas son más simples en Object-Z que en Z. Enlaces externos
|
