公理语义 一个语言的每个语法成分的含义定义为公理和演绎规则， 用于推导出该成分执行的效果。 公理语义概念是随着程序正确性的证明而发展的。当正 确性证明能构造时表明程序执行它的规格说明所描述 的计算。在一个证明中，每一个语句之前之后都有一 个逻辑表达式对程序的变量进行约束，以此说明这个语 句的含义。 般的记号{P}S{Q} 如果在语句$执行前P为真，则在语句S执行并终止后Q为 真。 公理语义 一个语言的每个语法成分的含义定义为公理和演绎规则， 用于推导出该成分执行的效果。 公理语义概念是随着程序正确性的证明而发展的。当正 确性证明能构造时表明程序执行它的规格说明所描述 的计算。在一个证明中，每一个语句之前之后都有一 个逻辑表达式对程序的变量进行约束,以此说明这个语 句的含义。 一般的记号 {P} S {Q} 如果在语句S执行前P为真，则在语句S执行并终止后Q为 真