一种复杂同步语言程序的化简转化和自动验证方法

摘要

本发明提供了一种复杂同步语言程序的化简转化和自动验证方法，包括对复杂同步语言程序进行词法分析、语法分析后生成与源程序对应的抽象语法树。基于程序等价转化的思想，将复杂同步语言程序的抽象语法树进行化简并转化为简单同步语言程序的抽象语法树。遍历转化后的抽象语法树，得到一个与源程序功能等价并且只包含简单同步语言语法结构的程序。将该程序作为简单同步语言模型检测工具的输入，得到验证结果，从而实现对复杂同步语言程序的自动验证。