第5章 类型和效果系统 5.2理论上的性质 操作语义：无环境的自然语义 一语义的正确性 用类型系统得出某表达式的类型是，则该表达 式在操作语义下求得的值的类型也是x 程序分析的解的存在性 1、定义标注完全格 2、再定义标注类型的完全格 3、擦掉标注后是同样定型断言的加标注定型断 言集合构成一个Moore family第5章 类型和效果系统 5.2 理论上的性质 – 操作语义：无环境的自然语义 – 语义的正确性 用类型系统得出某表达式的类型是，则该表达 式在操作语义下求得的值的类型也是 – 程序分析的解的存在性 1、定义标注完全格 2、再定义标注类型的完全格 3、擦掉标注后是同样定型断言的加标注定型断 言集合构成一个Moore family