Application of classical compilation techniques for syntactic and semantic analysis of specification written in Object Z
This work addresses the difficulty of parsing Object Z for researchers and practitioners in formal methods, but it appears incremental as it applies existing compilation techniques to a specific domain.
The paper tackled the challenge of building a parser for the formal specification language Object Z by identifying its characteristics and semantic constraints, and proposed an approach based on conventional compilation techniques.
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.