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

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

作　　者：张杨[1] 段富[1] 

机构地区：[1]太原理工大学计算机科学与技术学院,山西太原030024

出　　处：《计算机工程与设计》2013年第7期2403-2407,共5页Computer Engineering and Design

基　　金：山西省自然科学基金项目(2008011039);山西省科技攻关基金项目(20080322008)

摘　　要：在编译器的构造中,常由于语义的二义性等问题导致不正确的目标程序。为解决此问题,提出了一种新型的语法及语义正确性验证方案,即建立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.

关 键 词：LR(k)文法 形式化描述 形式化验证 Z规格 语法 语义 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]