补充资料：前后断言方法

前后断言方法
pre-and post-assertion method

q ianhou duanyan fangfa前后断言方法(，1卜邵目环以户理.犷山价n州如司) 在语句前后分别加上前提条件(即前断言)和结果断言(即后断言)，用程序设计逻辑证明程序正确性的方法。前提条件是该语句可执行的充分条件。结果断言指出语句执行中止后应具有的性质。前提条件又称前置断言，结果断言也称后置断言、后置条件等。 该证明方法源于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等。

说明：补充资料仅用于学习参考，请勿用于其它任何用途。