一种基于Coq的C++编译器变量作用域形式化方法

摘要

本发明公开了一种基于Coq的C++编译器变量作用域形式化方法，采用record数学模型形式化表结构，采用Inductive归纳定义形式化栈结构，采用match匹配形式化代码中引起分支的操作逻辑，采用Fixpoint递归函数形式化重复行为操作逻辑。现有技术中的FSPVM解释器在解释变量操作方法的时候，如果变量操作方法带有作用域特性，就会错误解释。采用本发明中的变量操作方法替代FSPVM解释器里的解释变量操作方法可以让新的FSPVM解释器能够解释带有作用域特性的代码。本发明使用了Record数学模型形式化字典数据结构，较使用Inductive归纳方法的传统形式化方式明显的提升了执行效率。