第7章程序验证 内容概述 程序逻辑：描述和论证程序行为的逻辑 Hoare逻辑 Dijkstra:最弱前条件演算 从程序到定理 -验证条件生成 从定理到证明 定理证明器 判定过程 循环不变式的推断 以George C.Necula教授的讲稿为主来介绍
第7章 程序验证 内容概述 • 程序逻辑：描述和论证程序行为的逻辑 – Hoare逻辑 – Dijkstra最弱前条件演算 • 从程序到定理 – 验证条件生成 • 从定理到证明 – 定理证明器 – 判定过程 • 循环不变式的推断 • 以George C. Necula教授的讲稿为主来介绍
程序逻辑 ·Hoare:逻辑 -良形公式(wel-formed formula)的形式为 {P}C{2 -C是程序片段 需要介绍编程语言 -P和O是断言 需要介绍断言及推理规则 -{P}C{Q}称为程序规范 需要介绍规范语言及推理规则 -Hoare?逻辑也称为语言的一种公理语义
程 序 逻 辑 • Hoare逻辑 – 良形公式（well-formed formula）的形式为 { P } C { Q } – C是程序片段 需要介绍编程语言 – P 和Q是断言 需要介绍断言及推理规则 – { P } C { Q }称为程序规范 需要介绍规范语言及推理规则 – Hoare逻辑也称为语言的一种公理语义
作为例子的核心编程语言 。语法 -整数表达式 E::=n x-EE+EE-EE*EE 布尔表达式 B::=true false !BBBBB E<E (B) 一命令 C::=x=E C;C if BC}else{C while B{C -例子 y=1;z=0;while Z!=x)z=z+1;y=y *Z
作为例子的核心编程语言 • 语法 – 整数表达式 E ::= n | x | −E | E + E | E − E | E E | ( E ) – 布尔表达式 B ::= true | false | !B | B & B | B || B | E < E | ( B ) – 命令 C ::= x = E | C ; C | if B { C } else { C } | while B { C } – 例子 y = 1; z = 0; while (z != x) { z = z +1; y = y z }
Hoare逻辑 断言语言 -用来描述程序变量满足的性质，如x==5,x+y<30 通常，断言P,O的语法同编程语言布尔表达式的 语法有些区别：如可以出现量词 ·Hoare逻辑的良形公式 -{P}C{2} -C是一段程序，P和O分别是C的前条件和后条件 -例如{x=5}x=x+1{x=6}
Hoare逻辑 • 断言语言 – 用来描述程序变量满足的性质，如x==5, x+y <30 – 通常，断言P, Q的语法同编程语言布尔表达式的 语法有些区别：如可以出现量词 • Hoare逻辑的良形公式 – { P } C { Q } – C是一段程序，P和Q分别是C的前条件和后条件 – 例如 { x == 5 } x = x + 1 { x == 6 }
Hoare?逻辑 ·Hoarei逻辑良形公式{P}C{Q}的解释 部分正确性 在满足P的任何状态下执行C,若C终止则结果状 态一定满足Q。记作⑦ par{p)C1O) 完全正确性 在满足P的任何状态下执行C,则C一定终止并且 结果状态一定满足Q。记作ot{P}C{2} 通常建议用部分正确性证明十终止性证明来得到 完全正确性证明
Hoare逻辑 • Hoare逻辑良形公式{ P } C { Q }的解释 – 部分正确性 在满足P的任何状态下执行C，若C终止则结果状 态一定满足Q。记作 par { P } C { Q } – 完全正确性 在满足P的任何状态下执行C，则C一定终止并且 结果状态一定满足Q。记作 tot { P } C { Q } – 通常建议用部分正确性证明＋终止性证明来得到 完全正确性证明