主函数
本模块只是对pl0程序编译器部分进行部分正确性验证，即合法的pl0程序符合pl0语言的语法规则、生成的中间代码结构正确、符号表能正确收集各种信息。（验证时间约 94sec）
[Back to Index]
验证特点：变量不变式，归纳谓词，逻辑函数，幽灵代码，宏定义
标注说明：main 函数验证的性质：源文件中的 pl0 程序符合 pl0 语法规则，且生成对应的中间代码结构正确。
程序样例
可验证文件：pl0_main_vf.c