A Scanner and Parser for Z Specifications

Maria Ulfah Siregar, John Derrick


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.


Z2SAL; Scanner; Parser; JFlex; BYACC/J

Full Text:



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.

DOI: http://dx.doi.org/10.14421/ijid.2018.07104


  • There are currently no refbacks.

Copyright (c) 2018 IJID (International Journal on Informatics for Development)

Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.


ISSN: 2252-7834 (print) | 2549-7448 (online)

International Journal on Informatics for Development

Office : Informatics Dept. Faculty of Science and Technology,

State Islamic University (UIN) Sunan Kalijaga,


Marsda Adisucipto Street, Yogyakarta

Phone +62-274 519739 Fax. +62-274 540971

Email : ijid@uin-suka.ac.id

Creative Commons License

All publications

by International Journal on Informatics for Development are licensed under a

Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License