Application of classical compilation techniques for syntactic and semantic analysis of specification written in Object Z

TL;DR

This paper explores how classical compilation techniques can be adapted to analyze Object Z specifications, addressing the challenges of parsing formal languages by combining compilation expertise with formal specification understanding.

Contribution

It introduces tools for analyzing Object Z specifications, identifies common semantic constraints, and proposes a compilation-based approach for building an Object Z parser.

Findings

Tools for analyzing Object Z and Z specifications are presented.

Common semantic constraints in Object Z are identified.

A compilation-based approach for Object Z parser construction is proposed.

Abstract

Building a parser for a formal specification language such as Object Z is not an easy task. Indeed, it requires a double competence both in the compilation field than in the field of formal specification. In this paper, we first present some tools for analyzing specifications written in Z and Object Z by showing the characteristics of each. Then, we identify some common semantic constraints in Object Z. Finally, we propose an approach for building a parser for Object Z based on the conventional techniques of compilation.