A Scanner and Parser for Z Specifications



How to Cite

Siregar, M. U., & Derrick, J. (2018). A Scanner and Parser for Z Specifications. IJID (International Journal on Informatics for Development), 7(1), 14–20. https://doi.org/10.14421/ijid.2018.07104


Coding either a scanner or a parser from beginning has many disadvantages such as tedious, could raise many errors, needs much times and effort, etc. All of these could result less scanner or parser. This paper describes our research on implementing a scanner and parsers for Z specifications. Rather to code them from scratch, we use tools that have specialities on creating such tasks. These tools generate several Java files which can be integrated with a main program in Java. Our research produces a scanner and parser for Z specifications. These tools may benefit Z specifications to be studied further.



G. Klein, “JFlex – The Fast Scanner for Java,” Accessed from http://www.jflex.de/index.html, 2015.

T. Hurka, “BYACC/J,” Accessed from http://byaccj.sourceforge.net, 2008.

A. J. D. Reis, “Compiler Construction Using Jva, JavaCC, and YACC,” Wiley-IEEE Press, 2012.

G. Smith and L. Wildman, “Model Checking Z Specifications Using SAL,” in ZB 2005: Formal Specifications and Devvelopment in Z and B, Springer, 2005, pp. 85–103.

J. Derrick, S. North, and A. J. H. Simons, “Z2SAL: A Translation-based Model Checker for Z,” Formal Aspect of Computing, Springer, 2011, pp. 43--71.

J. Derrick, S. North, and A. J. H. Simons, “Issues in Implementing a Model for Z,” Formal Methods and Software Engineering, Springer, 2006, pp. 678--696.

A. J. H. Simons, “The Z2SAL User Guide,” Accessed from http://staffwww.dcs.shef.ac.uk/people/A.Simons/z2sal/userguide.html, 2012.

M. U. Siregar, “Support for Model Checking Z Specifications,” A PhD Thesis of the University of Sheffield, Accessed from etheses.whiterose.ac.uk/17776/1/thesis_acp12mus_rev.pdf, 2017.

J. M. Spivey, “The Z Notation,”Prentice-Hall: New York, 1989.

J. R. Levine, T. Mason, and D. Brown, “Lex & YACC,” O’Reilly & Associates, Inc., 1992.

Creative Commons License
IJID (International Journal on Informatics for Development) is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License