基本知识 ,谓词逻辑 程序设计中用到谓词逻辑的知识 -谓词：结果类型为bo0l的函数 bool even(int m){/用编程语言写的谓词，与数理 if(m/2*2=m)return true;/逻辑中的有区别 else return false; -if(even(x)&even(y))... 一<、<=、=、！=…等关系算符都是谓词
• 谓词逻辑 程序设计中用到谓词逻辑的知识 – 谓词：结果类型为bool的函数 bool even(int m) { //用编程语言写的谓词，与数理 if (m/2 * 2 == m) return true; //逻辑中的有区别 else return false; } – if(even(x) && even(y)) … – <、<=、==、!= …等关系算符都是谓词 基 本 知 识 12
基本知识 ·谓词逻辑 -合式公式 (1)谓词集合 、 函数集合 (包括常量) (2)基于来定义项集 t:xcft,...,t) (f∈ 例如a+5<b-3中的a+5和b-3 3)归纳地定义基于（，) 的合式公式 φ：=Pt1,2,,tnl中|中V中|中∧中| p→中1x中13xφ1（φ） (P∈ -增加的规则 全称量词断言和存在量词断言的证明规则等
• 谓词逻辑 – 合式公式 (1) 谓词集合 、函数集合 （包括常量） (2) 基于 来定义项集 t ::= x | c | f(t, …, t) ( f ) 例如 a + 5 < b – 3中的a + 5和b – 3 (3) 归纳地定义基于（ , ）的合式公式 ::= P(t1 , t2 , …, tn ) | | | | | x | x | ( ) ( P ) – 增加的规则 全称量词断言和存在量词断言的证明规则等 基 本 知 识 13
Hoare逻辑 ·程序逻辑 -对程序进行推理的逻辑 -Hoare逻辑是一种程序逻辑 介绍面向非常简单的编程语言（只有赋值语句、 顺序语句、条件语句和循环语句)的Hoare逻辑 推理规则 14
Hoare 逻 辑 • 程序逻辑 – 对程序进行推理的逻辑 – Hoare逻辑是一种程序逻辑 – 介绍面向非常简单的编程语言（只有赋值语句、 顺序语句、条件语句和循环语句）的Hoare逻辑 推理规则 14
Hoare逻辑 ·合式公式(wel-formed formula) 语法形式：{PS{O},称为Hoare三元式 (1)S是代码段，遵循相应编程语言的语法 (2)P和O是关于程序状态（变量到值的映射）的 断言，分别称为S的前断言和后断言，断言是谓词 逻辑的合式公式 (3)例：{x=1∧y<5}x=x+1{x=2Λy<5} {P,S{Q}的含义：在满足P的状态下执行S,若执 行终止，则终止状态满足Q 例：{x=1∧y<5}x=x+1{x=2∧y<5}成立 {x>1∧y<5}x=x+1{x>0Λy<5}也成立
Hoare 逻 辑 • 合式公式（well-formed formula） – 语法形式：{P} S {Q}，称为Hoare三元式 (1) S是代码段，遵循相应编程语言的语法 (2) P和Q是关于程序状态（变量到值的映射）的 断言，分别称为S的前断言和后断言，断言是谓词 逻辑的合式公式 (3) 例： {x == 1 y < 5} x = x +1 {x == 2 y < 5} – {P} S {Q}的含义：在满足P的状态下执行S ，若执 行终止，则终止状态满足Q 例：{x == 1 y < 5} x = x +1 {x == 2 y < 5}成立 {x > 1 y < 5} x = x +1 {x > 0 y < 5}也成立15
Hoare逻辑 ·赋值公理 形式：{QEx}x=E{2公 QE/x]表示Q中出现的变量x用表达式E代换 -例：{x+1>6}x=x+1{x>6}是赋值公理的实例 -特点：x+1>6(即x>5)是语句x=x+1和后断 言x>6的最弱前断言 (1)x>5.1和x>7都可作为前断言，因都强于x>5 x>5.1→x>5并且x>7→x>5 (2)若x>4.9作为前断言，则三元式不成立，因为 x>4.9→x>5不成立 16
Hoare 逻 辑 • 赋值公理 – 形式：{Q[E/x]} x = E {Q} Q[E/x]表示Q中出现的变量x用表达式E代换 – 例: {x +1 > 6} x = x +1 {x > 6} 是赋值公理的实例 – 特点： x +1 > 6 （即x > 5）是语句x = x+1和后断 言x > 6 的最弱前断言 (1) x > 5.1和x > 7都可作为前断言，因都强于x > 5 x > 5.1 x > 5 并且x > 7 x > 5 (2) 若x > 4.9作为前断言，则三元式不成立，因为 x > 4.9 x > 5不成立 16