Abstract
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.
References
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.
IJID (International Journal on Informatics for Development) is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License