数理逻辑ch4

1第四章程序验证前述模型的检测主要是对通讯系统最为适用，特点是：1）有限状态；2）没有复杂数据无法操作类似整数、表或树等变量（实现难度指运行时间及复杂系数等）对于无限状态空间，本章提出程序验证方法2与模型检测方法相比，程序验证方法属于1）基于证明的方法采用一种证明演算构造系统满足所需性质的一个证明。（类同谓词演算）系统描述为一组逻辑公式г，而规范是另一个公式Ф，通过找到г├Ф的证明来验证系统满足性质这样验证性质就避免了①②③无限的具体的个体例如：①穷举验证②程序中的无限多个交互值验证③无限多个模型验证32）基于半自动的验证(人的因素+机器因素)需要人工编制一些启发式规则3）基于面向性质的验证验证程序的性质，不是检测程序的规范如：顺序性这个性质设：n为开始t为就绪c为运行它的性质是n→t→c……44）基于应用领域的验证这里应用领域是顺序变换程序①程序获得一个输入②经过运算③产生一个正确（希望）的输出④终止5）基于开发前/后的验证如：任何一个工程的建设之前都要通过论证，是否可行，而且这样的论证是经过多次交换而得到的结果，避免需求错误开发小程序片段代码的过程中用本方法进行验证，避免功能性错误5§4.1为什么要规范和验证编码计算机科学中验证论据包括1）有效地形成文档：①是程序规范的重要组成部分②程序文档化的过程可以提出/解决问题2）缩短市场化时间：在计划阶段，通过形式规范对软件进行验证，可清除大多数错误，清晰系统结构，大大缩短软件开发市场化时间63）重析经适当的规范和验证的软件更容易复用，如：移植，再开发等4）认证审计通过证明程序满足其规范，最终确保软件产品的安全性，正确性。7§4.2软件验证的一种框架（惯例）编制一个系统首先要了解这个系统的功能、用途等，然后进行设计到完成这个系统。这个过程为：接受系统了解系统功能设计系统形式规范编码实现84.2软件验证的一种框架（模式）项目（来源客户）→软件公司→根据实际进行非形式描述→得出初步方案→比较与用户要求（希望）→得出形式化→实现→验证满足条件后→交付。那么具体产生软件的一个框架是：1）将应用领域中要求的非形式描述R，转化成（某种语言编写的）某种符号逻辑中等价公式ФR2）根据用户提供的要求（希望）如：数据，环境等，编写一个能实现ФR的程序P3）证明程序P满足公式ФR9Note：实际中也要经常在编制过程中修改R；Note：寻求R的合适形式化ФR过程是难点（要细心）；Note：最后任务验证P满足ФR。例如：编程序容易，但要构造一个合理的算法是难点，而这个算法要对用户要求是适合的，并证明算法是收敛的而不是发散的同时也要验证程序的可靠性。4.2软件验证的一种框架（模式）10§4.2.1一种核心程序设计语言接下来我们就用实际编码来介绍程序验证理论。对象：命令型编程语言的典型核心语言语言包括对整数值和布尔值变量的赋值if语句，while语句顺序合成。语言不包含：对象过程，线程递归数据结构114.2.1一种核心程序设计语言语法论域核心语言是由整数表达式，布尔表达式和命令组成，而把命令视为程序。核心语言有三类语法论域：1）整数表达式，由变量x，y，z…数字0，1，2…-1，-2…2）运算符，由+，-，*，÷3）命令121）整数表达式的形式定义：E：：=n∣x∣（-E）∣（E+E）∣（E-E）∣（E*E）（4-1）优先级1）-负数2）*，÷3）+，-134.2.1一种核心程序设计语言例如：核心语言的合法的整数表达式：5X4+（x-3）（x×y）+4x+（x×（y-（8+z）））142）布尔表达式（if、while语句中的条件）的形式定义：B：：=true∣false∣（！B）∣（B&B）∣（B║B）∣（EE）（4-2）Note：其中：！表示┐&表示∧║表示∨True表示TFalse表示FNote：！（E1==E2）可以写成E1！=E2153）命令的形式定义C::=x=E∣C;C∣ifB{C}else{C}∣whileB{C}x=E:当前状态下计算整数表达式E的值，然后用该计算的结果复写储存在x中的当前值C;C：命令C1和C2的顺序合成。开始在当前储存状态下执行C1。若执行终止，则在执行C1的结果后的储存状态下执行C2，否则C1的执行不终止，运行C1,C2也不终止。163）命令的形式定义C::=x=E∣C;C∣ifB{C}else{C}∣whileB{C}ifB{C}else{C}在当前存储状态下计算布尔表达式B。若结果为真，则执行C1；若B计算为假，则执行C2。whileB{C}1.在当前存储状态下计算布尔表达式B的值2.若B计算为假，则命令终止3.否则执行C。若该执行终止，则用已更新的存储状态下重新计算的B值再次从步骤(1)开始173）命令的形式定义C::=x=E∣C;C∣ifB{C}else{C}∣whileB{C}例如：while（z=0）例如if（a-1==0）{{y=1；}z=z+1；elsey=y+z+2；{y=a；}}其中：{}同C语言一样其含义同C语言一样18举例：用核心语言编写n！程序因为自然n的阶乘n！归纳定义为（由数学知）0！=1（n+1）！=（n+1）*n！（4-4）用核心语言编写为：y=1；z=0；while（z！=x）{z=z+1；y=y*z；}Note：这虽然是一个很简单的程序P，但要验证它确实能做到，接下来我们就验证它。19§4.2.2霍尔三元组我们知道用核心语言（由4-3）式生成的程序，计算n！时过程为：开始时在一个机器“状态”下运行做一些计算后可能终止（停止）输出结束时通常是另一个“状态”结束20机器的状态可以表示为程序中所使用的变量值的向量。即：d=d1，d2……dn（其中di表示某一个值）这样一来就会有一个问题要解决：即：对程序P需求的形式规范ФR用什么样的语法？其中：P表示编制的代码程序（代码编程者）Ф:表示公式ФR:表示形式描述R:表示非形式描述（用户的要求，或项目指标及参数）21例：计算数y，其平方小于输入x（用户要求R）1.一个合适的规范y*yx（设计者找到的公式）2.若输入x是-4时3.因为没有一个数的平方小于负数（问题出现）4.结果不可能对所有的可能输入都能编出程序（找客户修订）5.若输入x是正数，计算一个平方数小于x的数y（修订后要求）22结论：不仅考虑程序运行后的状态还要考虑程序运行前的状态这样我们给出一个规范（霍尔三元组）即：断言三元组（|Ф|）P（|ψ|）初始程序结果含义为：若程序P在一个满足Ф的状态下运行，则执行P的结果状态满足ψ。23例如上例：计算平方小于x的数y的程序P的规范形式为：（∣x0∣）P（∣y*yx∣）含义为：若在满足x0的状态下运行P，则结果状态将是y*yx。Note：若x≤0时怎么办，因为客户没要求，即使x≤0时是“垃圾”也满足规范。通过上述我们给出霍尔三元组的定义24定义：1）规范的（∣Ф∣）P（∣ψ∣）称为霍尔三元组。规范指：给出条件能够找出合适的逻辑公式例如：计算数y，其平方小于输入x（给出条件）y*yx（找到了合适的规范）2）在（∣Ф∣）P（∣ψ∣）中Ф:为P的前置条件ψ:为P的后置条件253）核心程序（验证语言）的一个存储或状态是将每个变量x指派为一个整数L（x）的函数L。例如：L（x）=就绪，L（y）=运行，L（z）=开始，每个状态的函数为L，（类同数学的f（x）中的f）4）①对于带有函数符号-（负，一元的），②对于带有函数符号+，-（二元的），③对于带有谓词符号，=的逻辑公式，我们说状态L满足Ф或者L是一个Ф状态写作L╞Ф，当且仅当M╞lФ成立。5）要求|Φ|和|Ψ|中的量词只约束未出现在程序P中的变量26例如：对满足L（x）=-2L（y）=5L（z）=-1的任意状态L，关系①L╞┐（x+yz）成立，因为x+y计算为-2+5=3，Z计算为L（z）=-1而3不是严格小于-1。故成立27例如：对满足L（x）=-2L（y）=5L（z）=-1的任意状态L，关系②L╞y-x*zz不成立即：5-（-2）*（1-）=3而3不是严格小于-1。故②不成立28例如：对满足L（x）=-2L（y）=5L（z）=-1③L╞∀u（yu→y*zu*z）不成立因为当u=7时L╞yu成立，但L╞y*zu*z不成立总结：不对开始状态做任何约束，我们希望无论程序从什么状态开始，结果状态都应满足ψ，为此前置条件设为T（永真）29霍尔三元组规范的程序不唯一例如：计算y，其平方小于输入x程序1：y=0；程序2：y=0；while（y*yx）{y=y+1；}y=y-1；修正点Note：若x=22时，程序1输出0，程序2输出4，都是规范的。30§4.2.3部分正确性和完全正确性霍尔三元组的含义：“若程序P在满足Ф的状态下运行，则执行P的结果满足ψ”但没提到如果P不终止，我们会得到什么结论有两种方法来处理：①部分正确性证明（不要求程序终止）②完全正确性证明（要求程序终止）31部分正确性证明定义如果对满足Ф的所有状态L（x），只要P实际终止，执行P后结果状态就满足后置条件ψ，我们称三元组（∣Ф∣）P（∣ψ∣）在部分正确意义下满足。此时关系╞Par（∣Ф∣）（∣ψ∣）成立。我们称╞Par为部分正确性满足关系。特别地，任何不终止的程序都满足其规范，例如：whileture{x=0；}无休止地循环。32例：计算平方小于x（∣x0∣）P（∣y*yx∣）说明x0的状态下运行程序P结果状态是y*yx即╞Par部分正确性满足。也就是说仅当程序P对一个满足Ф的输入终止时，我们才坚持ψ在结果状态下为真。33完全正确性证明定义我们说三元组（∣Ф∣）P（∣ψ∣）在完全正确意义下满足，如果满足前置条件Ф的所有状态下执行程序P，P肯定终止，而且结果状态满足后置条件ψ。我们说关系╞tot（∣Ф∣）P（∣ψ∣）成立，并称╞tot为完全正确性关系。不终止的程序都不满足其规范Note：本章以部分正确性证明为主。下面给出证明规范的典型例子34例1：设succ为P是程序a=x+1；if（a-1==0）{y=1；}else{y=a；}因为succ在部分正确性的意义下满足规范╞Par（∣T∣）succ（∣y=x+1∣）因为a=x+1，y=a，所以y=x+1又因若将x视为输入，y视为输出，则succ计算后继35例2：如计算n的阶乘n：（设程序为fac1）y=1；z=0；while（z！=x）{z=z+1；y=y*z；}该程序只有x最初为非负时该程序才终止|=tot(|x≧0|Fac1|Ψ|)成立|=tot(|T|Fac1|Ψ|)不可证|=par(|x≧0|Fac1|Ψ|)可证|=par(|T|Fac1|Ψ|)可证36根据例子给出如下定义：定义：①若三元组（∣Ф∣）P（∣ψ∣）的部分正确性可用部分正确性演算所证明，则称矢列├Par（∣Ф∣）P（∣ψ∣）是有效的。②若三元组（∣Ф∣）P（∣ψ∣）的完全正确性可用完全正确性演算所证明，则称矢列├tot（∣Ф∣）P（∣ψ∣）是有效的。37形式的给出合理性，对所有Ф，P，ψ而言（也可以理解为定理）①只要├Par（∣Ф∣）P（∣ψ∣）有效则╞Par（∣Ф∣）P（∣ψ∣）成立②同理只要├tot（∣Ф∣）P（∣ψ∣）有效则╞tot（∣Ф∣）P（∣ψ∣）成立合理性比完备性更容易证明§4.2.4程序变量和逻辑变量（对核心语言）定义：将待验证程序中的变量称为程序变量例上例中的（∣x≥0∣）fac1（∣y=x！∣）中的x，yNote：程序变量也可以出现在规范的前置条件和后置条件中下面给出例子：Fac1Fac2Sumy=0；y=1z=0；z=0；while（x！=0）while（x0）while（z！=x）{y=y*x；{z=z+x；{z=z+1；x=x-1；x=x-1；}}