Home // ICSEA 2011, The Sixth International Conference on Software Engineering Advances // View article

Formal Parsing Analysis of Context-Free Grammar using Left Most Derivations

Authors:
Khalid A. Buragga
Nazir Ahmad Zafar

Keywords: parsing analysis; context-free language; formal specification; Z notation; verification.

Abstract:
Formal approaches are useful to verify the properties of software and hardware systems. Formal verification of a software system targets the source program where semantics of a language has more meanings than its syntax. Therefore, program verification does not give guarantee the generated executable code is correct as described in the source program. This is because the compiler may lead to an incorrect target program due to bugs in the compiler itself. It means verification of compiler is important than verification of a source program to be compiled. In this paper, context-free grammar is linked with Z notation to be useful in the verification of a part of compiler. At first, we have defined grammar, then, language derivation procedure is described using the left most derivations. In the next, verification of a given language is described by recursive procedures. The ambiguity of a language is checked as a part of the parsing analysis. The formal specification is analyzed and validated using Z/Eves tool. Formal proofs of the models are presented using powerful techniques, that is, reduction and rewriting of the Z/Eves.

Pages: 251 to 256

Copyright: Copyright (c) IARIA, 2011

Publication date: October 23, 2011

Published in: conference

ISSN: 2308-4235

ISBN: 978-1-61208-165-6

Location: Barcelona, Spain

Dates: from October 23, 2011 to October 29, 2011