PM-06-Chap03-程序规范及其正确性证明概述.pptVIP

2005年3月3日星期四鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved*内容－Whereweare？程序规范、规范的描述断言与规范及{P}S{Q}程序正确性的概念程序正确性证明的过程2005年3月3日星期四鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved*3.2断言与规范1.断言断言就是关于事物性质的陈述。这个陈述可真可假。如“三是个质数”用断言作为程序的注解或作为正确性命题的一部分时，常用大括号括起来。例1:写一个计算商和余数的程序程序规范:“设被除数x1是个非负整数，除数x2是个正整数，计算x1除以x2的商y1和余数y2”又描述为:“初始条件:{x1=0ANDx20},计算满足{x1=x2*y1+y2and0=y2x2}的整数y1和y2”2005年3月3日星期四鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved*3.2断言与规范(续)一般地,一个程序规范可表示为由两个谓词构成的二元组（P,Q）。其中,P描述了所欲求解的问题必须满足的初始条件,它限定了输入参数的性质,称为初始断言或前置断言；Q描述了问题的最终解必须满足的性质,称为结果断言或后置断言。2005年3月3日星期四鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved*3.2断言与规范(续)程序断言是对程序的性质的陈述。最重要的一个程序断言为:{P}S{Q}。其中，（P，Q）是程序S的程序规范，S是一个程序（或语句）断言{P}S{Q}称为S关于（P，Q）的正确性断言。它的意义:“若S开始执行时P为真，则S的执行必终止且终止时Q为真”2005年3月3日星期四鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved*3.2断言与规范(续)例:求商余程序{x1=0andx20}Y2:=x1;y1:=0;{0=y2and0x2andx1=x2*y1+y2}Whiley2=x2dobegin{0=y2and0x2＝y2andx1=x2*y1+y2}y2:=y2-x2;y1:=y1+1;{0=y2and0x2andx1=x2*y1+y2}end;{x1=x2*y1+y2and0=y2x2}2005年3月3日星期四鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved*3.2断言与规范(续)问题：如何构造断言使他们能准确地反映不同位置上程序的性质？有了断言，如何证明他们的正确性？能否有准则，可以从规范（P，Q）构造出程序S，使{P}S{Q}为真。2005年3月3日星期四鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved*3.2断言与规范(续)2.程序断言的进一步说明说明:在给出规范描述（P，Q）时，必须指明哪些量是可变的，哪些是不可变的。如果是可变的，必要时对前者还需指明其变化方式。输入参数:在程序执行前从外部获得值，但在程序执行中，其值始终保持不变的变量。一般用以x开头的标识符表示。输出变量:其值随程序的执行而不断变化的变量。一般以y开头的变量，或不以x和u开头的变量标识。辅助变量:为了描述程序变量取值变化方式而因入的变量。这些变量不得在程序中出现，用以u开头的变量表示。2005年3月3日星期四鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved*3.2断言与规范(续)例1.编写一个程序Swap（y1,y2）,功能是把y1,y2两变量的值互换。其规范:({y1=u1∧y2=u2},{y1=u2∧y2=u1})鲍玉斌东大信息学院计算机软件所程序设计方法学AllRightsReserved第3章程序规范及其正确性证明概述*⑴Ｚ语言对大型系统的模块化能力不足。因为在Z语言中，目标软件系统的结构和特征都用模式来描述，随着系统的增大，模式也会越来越多，而Ｚ语言中没有更加有效的机制来管理这些模式，最终导致Ｚ规格说明难以阅读。⑵难以识别影响某一状态模式的所有操作模式。因为在Ｚ语言中，一个操作模式可能涉及多个状态模式，为了确定能影响特定状态模式的所有操作模式，就需要逐个检查全部操作模式的声明部分，这对于大型软件