前后断言方法

pre-and post-assertion method

前后断言方法是在语句前后分别加上前提条件(即前断言)和结果断言(即后断言)，用程序设计逻辑证明程序正确性的方法。前提条件是该语句可执行的充分条件。 结果断言指出语句执行中止后应具有的性质。前提 条件又称前置断言，结果断言也称后置断言、后置条 件等。 该证明方法源于R.Floycl，他在1967年提出在 流程图的联线上加上断言使得程序到达该处时断言 为真。后经C.A.R.HOare发展成型，成为程序设计 逻辑的主要部分。 前后断言的主要形式有两种: (l)Q{引R刻画语句S的部分正确性。意 指:若前提条件Q满足，且S执行终止，则S终止 时结果断言R成立。 (2){Q}S{R}刻画语句S的完全正确性。意 指:若前提条件Q满足，则S执行终止，且S终止 时结果断言R成立。 将Q{S}R或{Q}S{R}的整体作为一个谓词 公式，若该公式永真，则S相对于前提条件Q和结 果断言R分别是部分正确或完全正确的。为证明 复合语句Q{51;52}R的部分正确性，可在S，;52 之间插入断言Q‘使得Q{S;}Q‘和Q‘{52}R都永 真。也可以插人多个断言Ql，QZ，Q3等，使它们之 间是蕴涵关系，用以反映证明思路。对其它语句构 造可采用类似的方法。对于循环语句，除给出前后 断言外，还须在循环中加入循环不变式，要求每次循 环到达该处时不变式都成立。用前后断言可表示 语句的公理语义。利用这些语义规则可帮助我们 在程序正确性证明过程中确定该擂人何种断言， 以达到引导证明的目的(参见最弱前里条件方法)。 前后断言方法，特别是结合最弱前置条件方法现 已广泛用于规约语言及其支撑系统，如VDM，Lareh 等。