程序验证(十二):完全正确性

Tattoo

发布日期: 2020-07-03 14:32:32 浏览量: 24
评分:
star star star star star star star star star star
*转载请注明来自write-bug.com

版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。
原文链接:https://blog.csdn.net/swy_swy_swy/article/details/106844776

一、完全正确性

完全正确性(total correctness),写作:

[P]c[Q][P]c[Q]

意思是:

  • 如果我们从一个满足PP的环境开始执行cc

  • 那么cc一定终止

  • 且它的最终的环境满足QQ

二、良基关系(Well-Founded Relations)

集合SS上的一个二元关系\prec是一个良基关系,当且仅当:

  • SS中不存在无限序列s1,s2,s3,..s_1,s_2,s_3,..,使得对于所有i>0i > 0都有si+1sis_{i+1}\prec s_i

  • 也就是说,SS中每个下降序列都是有限的

2.1 词法意义上的良基关系

给定集合S1,..,SnS_1,.. ,S_n和关系1,..,n\prec_1 ,.. ,\prec_n ,令S1×..×S_1\times .. \times

定义关系\prec

(s1,..,sn)(t1,..,tn)i=1n(siitij=1i1sj=tj)(s_1 ,.. ,s_n)\prec (t_1 ,.. ,t_n)\Leftrightarrow \bigvee ^n_{i=1} (s_i\prec_i t_i\wedge\bigwedge ^{i-1}_{j=1} s_j=t_j)

解释一下,(s1,..,sn)(t1,..,tn)(s_1 ,.. ,s_n)\prec (t_1 ,.. ,t_n)当且仅当:

  • 在某一位置iisiitis_i\prec_i t_i

  • 而对于所有之前的位置jjsj=tjs_j=t_j

2.2 证明完全正确性

为了证明程序终止,我们需要:

  • 在程序的状态上构造一个良基关系\prec

  • 证明每一个基础路径的的输出状态都“小于”输入状态

如果满足以上两点,那么程序一定终止,否则就存在一个程序状态的无限序列,这可以被映射到\prec上的一个无限下降序列。

与以上两步相对应,我们需要:

  • 找到一个函数δ\delta将程序状态映射到一个带有已知良基关系\prec的集合SS

  • 证明δ\delta在每一个基础路径上依据\prec都是下降的

函数δ\delta被称为秩函数(ranking function)。

2.3 对于秩函数的注释

我们用带有\downarrow的代码注释秩函数,需要在函数的循环头位置注释。

2.4 vc

vcvc即为:

Pwlp(c1;..;cn,δ(x)δ(x))[x/x]P\to wlp(c_1; .. ;c_n,\delta (x)\prec \delta (x'))[x/x']

计算的时候用xx^{\prime}代表开始时xx的值,计算完毕后再换回来。

上传的附件

发送私信

人生最好的三个词:久别重逢,失而复得,虚惊一场

48
文章数
33
评论数
最近文章
eject