Object-Z

Object-Z is an object-oriented extension of the Z specification language, developed in the early 1990s to address Z's inability to describe systems in terms of classes, objects, inheritance, and polymorphism. Where Z schemas describe abstract states and operations, Object-Z adds object-oriented structuring: classes encapsulate state and behavior, objects are instances of classes, and inheritance allows specifications to be refined and reused through specialization.

The semantics of Object-Z preserve the set-theoretic foundations of Z while extending the schema calculus with object identity, class hierarchies, and operation dispatch. A class in Object-Z is essentially a template that defines a state schema (the attributes) and a collection of operation schemas (the methods). Object identities are modeled as references to state bindings, and the history of an object is the sequence of states it passes through as its operations are invoked.

Object-Z was an important step in the evolution of formal methods toward the design paradigms that dominated 1990s software engineering. However, it suffered from the same adoption barriers as Z itself — mathematical notation, limited tool support — and was eventually overtaken by less formal but more accessible approaches such as UML and design-by-contract. The question Object-Z raises is whether formal methods failed to adopt object-orientation, or whether object-orientation failed to earn the rigor that formal methods demanded.