前后置断言方法 ·霍尔逻辑的核心思想 {Pre,C,Post) 口用于从逻辑上证明C的正确性 口Pre:前置断言，用于验证C执行的充分条件 口Post:后置断言，用于“检验”C执行后的效果(ifC终止) 口后置断言中的a' "C执行前后变量的变化如何在denotation上予以区别：'符号前后置断言方法 ◼ 霍尔逻辑的核心思想 ❑ {Pre, C, Post} ❑ 用于从逻辑上证明C的正确性 ❑ Pre：前置断言，用于验证C执行的充分条件 ❑ Post：后置断言，用于“检验”C执行后的效果(if C终止) ❑ 后置断言中的a’ ◼ C 执行前后变量的变化如何在denotation上予以区别：’符号