Design and construction of an error-free compiler is a difficult and challenging process. The main functionality of a compiler is to translate a source code to an executable machine code correctly and efficiently. In formal verification of software, semantics of a language has more meanings than the syntax. It means source program verification does not give guarantee the generated code is correct. This is because the compiler may lead to an incorrect target program due to bugs in itself. It means verification of a compiler is much more important than verification of a source program. In this paper, we present a new approach by linking context-free grammar and Z notation to construct LR(K) parser. This has several advantages because correctness of the compiler depends on describing rules that must be written in formal languages. First, we have defined grammar then language derivation procedure is given using right-most derivations. Verification of a given language is done by recursive procedures based on the words. Ambiguity of a language is checked and verified. The specification is analyzed and validated using Z/Eves tool. Formal proofs are presented using powerful techniques of reduction and rewriting available in Z/Eves.
C. J. Burgess, “The Role of Formal Methods in Software Engineering Education and Industry,” Technical Report, University of Bristol, Bristol, 1995.
K. A. Buragga and N. A. Zafar, “Formal Parsing Analysis of Context-Free Grammar Using Left Most Derivations,” International Conference on Software Engineering Advances, 2011.
N. A. Zafar, S. A. Khan and B. Kamran, “Formal Procedure of Deriving Language from Context-Free Grammar,” International Conference on Intelligence and Information Technology, Vol. 1, 2010, pp. 533-536.
N. A. Zafar and B. Kamran, “Formal Construction of Possible Operators on Context-Free Grammar,” International Conference on Intelligence and Information Technology, 2010.
H. Beek, A. Fantechi, S. Gnesi and F. Mazzanti, “State/ Event-Based Software Model Checking,” Integrated Formal Methods, Springer, Berlin, 2004, pp. 128-147.
O. Hasan and S. Tahar, “Verification of Probabilistic Properties in the HOL Theorem Prover,” Integrated Formal Methods, Springer, Berlin, 2007, pp. 333-352.
F. Gervais, M. Frappier and R. Laleau, “Synthesizing B Specifications from EB3 Attribute Definitions,” Integrated Formal Methods, Springer, Berlin, 2005, pp. 207-226. doi:10.1007/11589976_13
K. Araki, A. Galloway, and K. Taguchi, “Integrated Formal Methods,” Proceedings of the 1st International Conference on Integrated Formal Methods, Springer, Berlin, 1999.
B. Akbarpour, S. Tahar and A. Dekdouk, “Formalization of Cadence SPW Fixed-Point Arithmetic in HOL,” Integrated Formal Methods, Springer, Berlin, 2002, pp. 185-204.
J. Derrick and G. Smith, “Structural Refinement of Object-Z/CSP Specifications,” The Institute of Finance Management, Springer, Berlin, 2000, pp. 194-213.
T. B. Raymond, “Integrating Formal Methods by Unifying Abstractions,” Springer, Berlin, 2004, pp. 441-460.
J. S. Dong, R. Duke and P. Hao, “Integrating Object-Z with Timed Automata,” 2005, pp. 488-497.
J. S. Dong, et al., “Timed Patterns: TCOZ to Timed Automata,” The 6th International Conference on Formal Engineering Methods, 2004, pp. 483-498.
R. L. Constable, et al., “Formalizing Automata II: Decidable Properties,” Technical Report, Cornell University, Cornell, 1997.
R. L. Constable, et al., “Constructively Formalizing Automata Theory,” Foundations of Computing Series, MIT Press, Cambridge, 2000.
M. Heiner and M. Heisel, “Modeling Safety Critical Systems with Z and Petri Nets,” International Conference on Computer Safety, Reliability and Security, Springer, Berlin, 1999, pp. 361-374. doi:10.1007/3-540-48249-0_31
H. Leading and J. Souquieres, “Integration of UML and B Specification Techniques: Systematic Transformation from OCL Expressions into B,” Asia-Pacific Software Engineering Conference, 2002, pp. 495-504.
H. Leading and J. Souquieres, “Integration of UML Views Using B Notation,” Proceedings of Workshop on Integration and Transformation of UML Models, 2002.
W. Wechler, “The Concept of Fuzziness in Automata and Language Theory,” Akademic-Verlag, Berlin, 1978.
N. M. John and S. M. Davender, “Fuzzy Automata and Languages: Theory and Applications,” ?Chapman & Hall, London, 2002.
M. Ito, “Algebraic Theory of Automata and Languages,” World Scientific Publishing Co., Singapore, 2004. doi:10.1142/9789812562685
M. Brendan and J. S. Dong, “Blending Object-Z and Timed CSP: An Introduction to TCOZ,” 20th International Conference on Software Engineering, IEEE Computer Society, Kyoto, 1998.
J. M. Spivey, “The Z Notation: A Reference Manual,” Printice-Hall, Austin, 1989.
J. M. Wing, “A Specifier, Introduction to Formal Methods,” IEEE Computer, Vol. 23, No. 9, 1990, pp. 8-24. doi:10.1109/2.58215
C. Lindig, “Random Testing of C Calling Conventions,” ACM, 2005.
J. A. Anderson, “Automata Theory with Modern Applications,” Cambridge University Press, Cambridge, 2006. doi:10.1017/CBO9780511607202
H. C. Young, J. Moscola and J. W. Lockwood, “Context-Free Grammar Based Token Tagger in Reconfigurable Devices,” Proceedings of International Conference of Data Engineering, 2005, p. 78.
M. V. D. Brand, A. Sellink and C. Verhoef, “Generation of Components for Software Renovation Factories from Context-Free Grammars,” Counselors of Real Estate, 2001, pp. 144-153.
M. Balakrishna, D. Moldovan and E. K. Cave, “Automatic Creation and Tuning of Context-Free Grammars for Interactive Voice Response Systems,” IEEE NLP-KE, 2005, pp. 158-163.
L. Pedersen and H. Reza, “A Formal Specification of a Programming Language: Design of Pit,” 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2008, pp. 111-118.
D. P. Tuan, “Computing with Words in Formal Methods,” Technical Report, University of Canberra, Canberra, 2000.
S. A. Vilkomir and J. P. Bowen, “Formalization of Software Testing Criterion,” South Bank University, London, 2001.
A. Hall, “Correctness by Construction: Integrating Formality into a Commercial Development Process,” Praxis Critical Systems Limited, Springer, Berlin, Vol. 2391, 2002, pp. 139-157.
B. A. L. Gwandu and D. J. Creasey, “Importance of Formal Specification in the Design of Hardware Systems,” Birmingham University, Birmingham, 1994.
D. K. Kaynar and N. Lynchn, “The Theory of Timed I/O Automata,” Morgan & Claypool Publishers, 2006.
D. Jackson, I. Schechter and I. Shlyakhter, “Alcoa: The Alloy Constraint Analyzer,” Proceedings of the 22nd International Conference of Software Engineering, 2000, pp. 730-733.
D. Aspinall and L. Beringer, “Optimisation Validation,” Electronic Notes in Theoretical Computer Science, Vol. 176, No. 3, 2007, pp. 37-59. doi:10.1016/j.entcs.2006.06.017
S. Briaisa and U. Nestmannb, “A Formal Semantics for Protocol Narrations,” Theoretical Computer Science, Vol. 389, No. 3, 2007, pp. 484-511.
L. Freitas, J. Woodcock and Y. Zhang, “Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository,” Science of Computer Programming, Vol. 74, No. 4, 2009, pp. 197-218. doi:10.1016/j.scico.2008.09.012