符号表管理
本模块有2个函数：函数enter用于向符号表添加新的符号，并确定标识符的有关属性。函数position用于查找符号表，并返回相关表索引。（验证时间约 102sec）
[Back to Index]
验证特点：变量不变式，宏定义，带命名行为的函数协议
标注说明：1. enter函数验证的性质：根据形参的取值(constant、variable和proc)，符号表收集不同的信息。
2. position函数验证的性质：当函数返回值大于0时，该返回值是形参id1在符号表中条目的索引；当函数返回值等于0时，形参id1在符号表中无相应条目。
程序样例
可验证文件：pl0_table_vf.c