基于Z规格的LR(k)形式化分析及验证

Formal analysis and verification of LR(k) based on Z

在编译器的构造中,常由于语义的二义性等问题导致不正确的目标程序。为解决此问题,提出了一种新型的语法及语义正确性验证方案,即建立LR(k)文法和Z规格说明的联系,以此构造LR(k)文法的形式化描述及其形式化验证。实验结果表明,该方案能有效描述并检测LR(k)文法分析器中的语法错误及语义二义性,有助于提高分析器的有效性。

During the construction of the compiler, complier may generate an incorrect source program due to bugs, such as amBiguity of semantic, in itself. So, a new approach of verification of correctness of semantic and syntax is presented, which links context-flee grammar and Z specification to construct formal specification and formal verification of LR （k）. The experiment demonstrates that the approach tests the ambiguity of semantic and syntax error of LR （k） to improve the validity of the compiler efficiently.