第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 } – 通常建议用部分正确性证明＋终止性证明来得到 完全正确性证明
Hoare逻辑 ●例1Succ ●例2Fac1 {} {x>=0} a=x+1; y=1; if(a-1=0){ Z=0; y=1; while (Z!=x){ else Z=Z+1; y=a; y=y*Z巧 {y=x+1} {y=x!
Hoare逻辑 • 例1 Succ • 例2 Fac1 { } { x >= 0 } a = x + 1; y = 1; if (a -1 == 0 ) { z = 0; y = 1; while ( z != x ) { } else { z = z + 1; y = a; y = y z; } } { y == x + 1 } { y == x ! }
Hoare逻辑 ●例2Fac1 ●例3Fac2 {x>=0} x是辅助的逻辑变量 y=1; {x>=0入x=X0} z=0; y=1; while (Z!=x){ while (x!=0){ z=Z+1; y=y*x; y=y*Z到 x=x-1; {y=x!} {y==xo!}
Hoare逻辑 • 例2 Fac1 • 例3 Fac2 { x >= 0 } x0是辅助的逻辑变量 y = 1; { x >= 0 x == x0 } z = 0; y = 1; while ( z != x ) { while ( x != 0 ) { z = z + 1; y = y x; y = y z; x = x − 1; } } { y == x ! } { y == x0 ! }
Hoare逻辑 ·部分正确性的证明规则 赋值公理 {Q[Elx]x={2) 赋值公理的实例 -{2=2}x=2{x=2} -{2==4}X=2{x=4} -{2=y}x=2{x=y} -{2>0}x=2{x>0》 -{x+1+5=y}x=x+1{x+5==y} {x+1>0人y>0}X=x+1{x>0Λy>0
Hoare逻辑 • 部分正确性的证明规则 – 赋值公理 赋值公理的实例 – { 2 == 2 } x = 2 { x == 2 } – { 2 == 4 } x = 2 { x == 4 } – { 2 == y } x = 2 { x == y } – { 2 > 0 } x = 2 { x > 0 } – { x + 1 + 5 == y } x = x + 1 { x + 5 ==y } – { x + 1 > 0 y > 0 } x = x + 1 { x > 0 y > 0 } { Q[E/x] } x = E { Q }
Hoare逻辑 ·部分正确性的证明规则 -赋值公理 {2IE]}x=E{2 -复合规则 AP}CIRY {R}C2{2} {P}C1;C2{2} -条件规则 {PAB}C1{2}{P∧B}C2{2} {P}if B{C1}else {C2) -循环规则 {I∧B}C{I} {I}while B{C}{∧-By
Hoare逻辑 • 部分正确性的证明规则 – 赋值公理 – 复合规则 – 条件规则 – 循环规则 { Q[E/x] } x = E { Q } { P } C1 { R } { R } C2 { Q } { P } C1 ; C2 { Q } { P B } C1 { Q } { P B } C2 { Q } { P } if B {C1 } else {C2} { Q } { I B } C { I } { I } while B {C } {I B}
Hoare逻辑 ·部分正确性的证明规则 -推论规则 ARP→P{P}C{2} AR2→2 {P}C{2} ARP'→P表示P→P在谓词逻辑的自然演绎演 算中可以证明
Hoare逻辑 • 部分正确性的证明规则 – 推论规则 AR P P 表示P P在谓词逻辑的自然演绎演 算中可以证明 AR P P { P } C { Q } AR Q Q { P } C { Q }
