错误诊断处理
为简单起见，pl0程序编译器部分的验证也只限于合法的pl0程序。如果pl0程序不合法（存在语法或语义错误），程序直接退出。
该模块包括两个函数：函数error打印错误信息；函数test在程序不合法时退出程序。（验证时间约 36sec）
[Back to Index]
验证特点：变量不变式，宏定义
标注说明：1. error函数主要功能是输出错误信息，验证的性质都是平凡的。
2. test函数协议包含两个命名行为：sym在集合s1中、sym不在集合s1中。
程序样例
可验证文件：pl0_error_vf.c