RETE网络中的优化编译模式及其PVS形式验证  

Optimizing Compiler Schemas in RETE Network and their Formal Verification with PVS

作　　者：刘晓建[1] 陈平[1] 

机构地区：[1]西安电子科技大学软件工程研究所,西安710071

出　　处：《计算机科学》2003年第6期168-171,共4页Computer Science

基　　金："十五"国防预先研究项目基金"可信软件工程技术"(413150501)

摘　　要：In the compilation of rule program to the intermediate code--RETE network,optimizing compilation is an important comptler schema,and is a necessary step in the compiler verification. In this paper,we discuss optimization schemas in rule program compilation,and prove the semantic equivalence theorems of these schemas. Firstly,the structure of RETE network and Its PVS specification are represented. Secondly,three kinds of optimization schemas are listed. Then algorithms evaluating semantics of target RETE network are given. Finally,we prove the semantic equivalence theorems with theorem prover PVS (Prototype Verification System).In the compilation of rule program to the intermediate code-RETE network, optimizing compilation is an important compiler schema,and is a necessary step in the compiler verification. In this paper,we discuss optimization schemas in rule program compilation, and prove the semantic equivalence theorems of these schemas. Firstly, the structure of RETE network and its PVS specification are represented. Secondly,three kinds of optimization schemas are listed. Then algorithms evaluating semantics of target RETE network are given. Finally,we prove the semantic e-quivalence theorems with theorem prover PVS (Prototype Verification System).

关 键 词：RETE网络 优化编译模式 PVS 形式验证 编译器 程序设计语言 

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