Recursive Schema Definitions in Object-Z

Unlike Z, Object-Z allows schemas to be defined recursively. This enables mutual and self recursive structures, commonly occurring in object-oriented programs, to be readily specified. In this paper, we provide a fixed point interpretation of such definitions. In addition, we provide simple guidelines for producing non-recursive schema definitions which are semantically identical to recursive ones.

• Type: Conference
• Year: 2000
• Where: ZUM
• Authors: Graeme Smith
• Keywords: Formal Methods, Non-recursive Schema Definitions, Object-Z Allows Schemas, Recursive Structures, ZUM 2000