一种基于规则的语言的公理语义  

Axiomatic semantics of rule-based language

作　　者：魏振春[1] 韩江洪[1] 陆阳[1] 刘小平[1] 

机构地区：[1]合肥工业大学计算机与信息学院

出　　处：《计算机工程与应用》2008年第20期86-88,共3页Computer Engineering and Applications

基　　金：国家教育部博士点基金(the Fund for the Doctoral Program of the Ministry of Education of China under Grant No.20050359004);国家教育部新世纪优秀人才计划项目(the New Century Excellent Talent Foundation from MOE of China under Grant No.NCET-04-050562);安徽省科技公关计划项目(the Key Technologies R&D Program of Anhui Province, China under Grant No.06012069B)

摘　　要：为了准确描述离散事件控制系统对象之间的逻辑关系和编写控制程序,提出了一种基于规则的语言——逻辑规则描述语言(LRDL)。用EBNF给出了LRDL的语法定义,基于Hoare逻辑的公理系统,形式化地给出并证明了LRDL的公理语义,为用LRDL编写的程序的正确性证明提供了理论依据。In order to exactly describe logic relations among objects of discrete event control systems and write programs,a rulebased language,Logic Rule Description Language （LRDL） is put forward.Formal syntax of LRDL is defined by EBNF.Axiomatic semantics of LRDL is presented and proved formally based on axiomatic system of Hoare logic,which offers theoretical basis for the proof of the correctness of programs written with LRDL.

关 键 词：规则 逻辑规则描述语言 公理语义 HOARE逻辑 形式语法 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]