Syntactic Constructs

Abstract

An Object-Z specification, like a Z specification, comprises a list of formal paragraphs — type definitions, axiomatic definitions, global predicates, schema definitions and class definitions — interleaved with informal explanatory text and diagrams. As in Z, line breaks in axiomatic definitions and schema definitions, including those that occur within class definitions, are interpreted as semicolons — that is, as declaration or predicate separators — except when such an interpretation is syntactically invalid, in which case they are, as in other parts of the specification, ignored.