基本知识 程序：在数组a中快速查找某个值 101521283237 44 49 53 57 6267717783 int am] Vn:[0..m-2].an]a n+1] ·怎样进行测试 -对数组a的长度m(m>0) 的各种情况都要测试吗？ -对a中出现的各个元素都需要测试吗？ -对a中不出现的元素要测多少种情况？
基 本 知 识 • 程序：在数组a中快速查找某个值 int a[m] n:[0..m−2].a[n] < a[n+1] • 怎样进行测试 – 对数组a的长度m (m>0) 的各种情况都要测试吗？ – 对a中出现的各个元素都需要测试吗？ – 对a中不出现的元素要测多少种情况？ 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 7
基本知识 程序测试与程序验证 测试能发现程序有错；一般而言，硬测试不能保证 程序无错 程序验证：用数学的方法来证明程序的性质，提 高软件可信程度 演绎验证：指用逻辑推理的方法来证明程序具备 所期望的性质 就所期望的性质而言，演绎验证可保证程序无错 程序逻辑：对程序进行推理的逻辑 Q
基 本 知 识 • 程序测试与程序验证 – 测试能发现程序有错；一般而言，测试不能保证 程序无错 – 程序验证：用数学的方法来证明程序的性质，提 高软件可信程度 – 演绎验证：指用逻辑推理的方法来证明程序具备 所期望的性质 就所期望的性质而言，演绎验证可保证程序无错 – 程序逻辑：对程序进行推理的逻辑 8
基本知识 命题逻辑 程序设计中用到命题逻辑的知识 if(0<=m&&m<100). ●0<=m和m<100都是命题逻辑的原子命题 ·&&是命题逻辑的二元运算符（下面用入而非&&） -if(0≤m0<n). ·是命题逻辑的二元运算符（下面用v而不是） -n=0;while(!n>=100){.;n=n+1;} 。!是命题逻辑的一元运算符（下面用一而不是！）
基 本 知 识 • 命题逻辑 程序设计中用到命题逻辑的知识 – if (0 <= m && m <100) … • 0 <= m和m <100都是命题逻辑的原子命题 • &&是命题逻辑的二元运算符(下面用而非&&) – if (0 < m || 0 < n) … • ||是命题逻辑的二元运算符（下面用而不是 ||） – n = 0; while(! n >= 100) { …; n = n + 1;} • !是命题逻辑的一元运算符（下面用而不是 !） 9
基本知识 ·命题逻辑 -合式公式(wel-formed formula) 的归纳定义 中：=pl中1pv中|中入中1中→中1（φ） (1)p代表原子命题，例如x>3,a5]=10.5 原子命题具体形式与讨论的问题领域有关 (2)中代表一般命题，“：=”右部用“|”分隔的 各部分代表命题的构成形式，如0<=x人x<100 (3)入，V,一和→代表合取、析取、非和蕴涵运算， 在确定了它们的运算优先关系后，很多情况下括 号可以省略，如pV(q1入q2)可简化为pVq1入q2 备注：蕴涵采用→而不是→，→用于描述函数类型
基 本 知 识 • 命题逻辑 – 合式公式（well-formed formula）的归纳定义 ::= p | | | | | ( ) (1) p代表原子命题，例如 x > 3, a[5] == 10.5 原子命题具体形式与讨论的问题领域有关 (2) 代表一般命题，“::=”右部用“| ”分隔的 各部分代表命题的构成形式，如 0<= x x <100 (3) , , 和代表合取、析取、非和蕴涵运算， 在确定了它们的运算优先关系后，很多情况下括 号可以省略，如p (q1 q2 )可简化为p q1 q2 备注：蕴涵采用而不是→， →用于描述函数类型 10
基本知识 命题逻辑 一推理规则 例：有关合取“入”运算的推理规则 (ne1) φ入 (Ae2) “人i”表示合取引入规则(i:introduction) “人e”表示合取消去规则 (e:elimination) 对和一等也都有各自的推理规则
基 本 知 识 • 命题逻辑 – 推理规则 例：有关合取“”运算的推理规则 ( i) (e1 ) (e2 ) “ i”表示合取引入规则（i: introduction） “ e”表示合取消去规则（e: elimination） 对和等也都有各自的推理规则 11