Verification of Identifier and Reserved word of Lexical Analyzer Using Z Notation

Abstract

In this paper, we formalize the lexical analysis into a Z specification for verifying it in Z tool. Lexical analyzer is described as automata, further, we write the specification of it using an integration of automata and Z. This gives formal approach which can leads to its correctness. In this paper, we present the development and verification of a generic and simple lexical analyzer which is obtained from the integration of automata and Z-notations.