程序验证(五):一阶理论的过程

Tattoo

发布日期: 2020-06-30 11:37:13 浏览量: 68
评分:
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/106622963

主要讨论TET_E的量词自由片段以及TAT_A

一、等价理论的判定

1.1 等价及未解释函数理论(Theory of Equality and Uninterpreted Functions)

除=外的谓词实际上使我们的讨论不必要地复杂化,去除这些累赘谓词的方法如下:

  • 对每个谓词pp,引入一个新的(fresh)函数符号fpf_p

  • 引入一个新的常量\bullet

  • 将每个谓词实例p(t1,..,tn)p(t_1 ,.., t_n)替换为fp(t1,..,tn)=f_p(t_1 ,.., t_n)=\bullet,这样就得到了等价及未解释函数理论(EUF):

    • EUF中唯一的谓词就是=
    • 所有的公理都是相等或不等

转化方法举例:

x=y(p(x)p(y))x=y\to (p(x)\leftrightarrow p(y))

转化为:

x=y((fp(x)=)(fp(y)=))x=y\to ((f_p (x)=\bullet)\leftrightarrow (f_p (y)=\bullet))

p(x)q(x,y)q(y,z)¬q(x,z)p(x)\wedge q(x,y)\wedge q(y,z)\to \neg q(x,z)

转化为:

(fp(x)=fq(x,y)=fq(y,z)=)fq(x,z)(f_p(x)=\bullet \wedge f_q(x,y)=\bullet \wedge f_q(y,z)=\bullet) \to f_q(x,z)\ne \bullet

1.2 一些概念

1.2.1 关系(relation)

给定SS上的二元关系RRs1,s2S\forall s_1,s_2\in S,或者s1Rs2s_1Rs_2或者¬(s1Rs2)\neg (s_1Rs_2)

一个二元关系RR若满足以下三个性质,即为一个等价关系(equivalence relation):

  • 自反性xS.sRs\forall x\in S.sRs

  • 对称性s1,s2S.s1Rs2s2Rs1\forall s_1,s_2\in S.s_1Rs_2\to s_2Rs_1

  • 传递性s1,s2,s3S.s1Rs2s2Rs3s1Rs3\forall s_1,s_2,s_3\in S.s_1Rs_2 \wedge s_2Rs_3 \to s_1Rs_3

一个二元关系RR是同余关系(congruence relation),如果它除以上三个性质外,还满足函数同余性:

s,tSn.(i=1nsiRti)f(s)Rf(t)\forall s,t \in S^n .(\bigwedge ^n_{i=1} s_iRt_i)\to f(s)Rf(t)

1.2.2 类(class)

RRSS上的一个等价关系,则sSs\in SRR下的等价类(equivalence class)为:

[s]R{sS:sRs}[s] _R \equiv \{s'\in S:sRs'\}

SS中的每个元素都属于RR的一个等价类。如果RR是同余关系,那么[s]R[s]_Rss的同余类。

举例:Consider the relation 2\equiv _2 over ZZ, where a2ba\equiv _2 b iff (a mod 2)=(b mod 2)(a \space mod \space 2)=(b \space mod \space 2). The equivalence class of 4 under 2\equiv_2 is:

[4]2={nZ:(nmod2)=0}={nZ:n is even}[4]_{\equiv_2} = \{n\in Z: (n mod 2)=0\}=\{n\in Z : n~is~even\}

1.2.3 分割(partition)

SS的一个分割PP是一个SS的子集的集合,满足:

  • total(SPS)=S(\bigcup _{S^{\prime} \in P} S^{\prime} )=S

  • disjointS1,S2P.S1S2S1S2=\forall S_1, S_2 \in P.S_1\ne S_2\to S_1 \cap S_2 = \varnothing

等价关系RR 产生了SS的一个分割,叫做SS除以RR的商,也就是:

S/R={[s]R:sS}S/R = \{[s]_R : s\in S\}

例如,商Z/2Z /\equiv_2即为这个分割:

{{nZ: n is odd},{nZ: n is even}}\{\{n\in Z :~n~is~odd\},\{n\in Z:~n~is~even\}\}

1.2.4 关系的精化(refinement)

给定SS上两个关系R1R_1R2R_2,我们说R1R_1精化了R2R_2,写作R1R2R_1 \prec R_2,如果满足条件:

s1,s2S.s1R1s2s1R2s2\forall s_1, s_2\in S.s_1R_1s_2 \to s_1R_2s_2

我们可以把二元关系RR视为一个对(pair)的集合R^\hat{R},也就是:

s1,s2S, if s1Rs2, then (s1,s2)R^\forall s_1,s_2 \in S,~if~s_1Rs_2,~then~(s_1,s_2)\in \hat{R}

于是我们知道R1R2R_1 \prec R_2当且仅当R^1R^2\hat{R}_1 \subseteq \hat{R}_2

举例:

R1:{sR1s:sS}R_1:\{sR_1s:s\in S\}

R2:{s1R2s2:s1,s2S}R_2:\{s_1R_2s_2:s_1,s_2\in S\}

那么

R1R2R_1 \prec R_2

1.2.5 等价闭包(equivalence closure)

一个SS上的关系RR的等价闭包RER^E是这样的一个等价关系,满足:

  • 其中RR精化RER^ERRER\prec R^E

  • 对于其他满足RRR\prec R^{\prime}的等价关系RR^{\prime},或者R=RER^{\prime}=R^E或者RERR^E \prec R^{\prime} 。也就是说,RER^E是包含RRR的最小的等价关系。

与之相似,RR的同余闭包(congruence closure)RCR^C是包含RR的最小同余关系。

等价闭包的构造的一个例子:

有一个论域S={a,b,c,d}S=\lbrace a,b,c,d \rbrace,一个关系RR满足:

aRb,bRc,dRdaRb,bRc,dRd

为了构造RER^E,根据定义逐步构造:

最后

RE={(a,b),(b,a),(a,a),(b,b),(b,c),(c,a),(c,b),(c,c),(d,d)}R^E = \{(a,b),(b,a),(a,a),(b,b),(b,c),(c,a),(c,b),(c,c),(d,d)\}

1.3 等价理论的判定

TET_E的量词自由片段是可判定的

1.3.1 核心逻辑

给定一个TET_E-公式FF

F:(s1=t1)..(sm=tm)(sm+1tm+1)..(sntn)F:(s_1 = t_1)\wedge .. \wedge (s_m = t_m)\wedge(s_{m+1}\ne t_{m+1})\wedge .. \wedge (s_n \ne t_n)

FFTET_E-可满足的,当且仅当存在一个同余关系\sim,使得:

  • 对每个i{1,..,m}i\in \lbrace 1,.. ,m \rbrace, sitis_i \sim t_i

  • 对每个i{m+1,..,n}i\in \lbrace m+1,.. ,n \rbrace, sitis_i \sim t_i

这样一个同余关系定义了FFTET_E-解释(D,I)(D,I)

  • 其中DD\sim的同余类构成

  • 其中III将DD的元素赋值给FF的子项(subterm)来满足\sim

  • 其中II赋值了=,一个与\sim相似的关系

我们把(D,I)F(D,I)\models F简记为F\sim \models F

1.3.2 同余闭包算法

SFS_FFF的子项,\simSFS_F上的关系,那么该算法如下:

  • 在子项集合SFS_F上构造{s1=t1,..,s+m=tm}\lbrace s_1=t_1,.. ,s+m=t_m \rbrace的同余闭包~

  • 如果对于任何i{m+1,..,n}i\in \lbrace m+1,.. ,n \rbracesitis_i \sim t_i,那么返回unsatunsat

  • 否则,返回satsat

第一步中,构造同余闭包的方法如下:

  • 从“最好”的同余关系开始0={{s}:sSF}\sim 0 = \lbrace \lbrace s \rbrace :s\in S_F \rbrace,这里SFS_F每个子项都在它本身构成的同余类里

  • 对于每个i{1,..,m}i\in \lbrace 1,.. , m \rbrace,通过把si=tis_i = t_i加入i1\sim _{i-1}构造i\sim _i

    • 将同余类[si]i1[s_i]_{\sim _{i-1}}[ti]i1[t_i]_{\sim _{i-1}}merge起来

    • 将任何通过以上步骤产生的新的同余关系传递下去

举例:判断以下公式的可满足性

F:f(a,b)=af(f(a,b),b)aF: f(a,b) = a\wedge f(f(a,b),b)\ne a

建立子项集合SFS_F

SF={a,b,f(a,b),f(f(a,b),b)}S_F = \{a,b,f(a,b),f(f(a,b),b)\}

构造SFS_F上的“最好”的闭包关系:

{{a},{b},{f(a,b)},{f(f(a,b),b)}}\{\{a\},\{b\},\{f(a,b)\},\{f(f(a,b),b)\}\}

对于每个i{1,..,m}i\in \lbrace 1,.. ,m \rbrace,将同余类[si]i1[s_i]_{\sim _{i-1}}[ti]i1[t_i]_{\sim_{i-1}}merge起来,这里由f(a,b)=af(a,b)=a得到:

{{a,f(a,b)},{b},{f(f(a,b),b)}}\{\{a,f(a,b)\},\{b\},\{f(f(a,b),b)\}\}

每次merge之后,使用公理以推进,由f(a,b)a,bbf(a,b)\sim a,b\sim b,有f(f(a,b),b)f(a,b)f(f(a,b),b)\sim f(a,b),从而:

{{a,f(a,b),f(f(a,b),b)},{b}}\{\{a,f(a,b),f(f(a,b),b)\},\{b\}\}

这也就是SFS_F的同余闭包。

FFTET_E-不可满足的,因为f(f(a,b),b)af(f(a,b),b)\sim aFF声称f(f(a,b),b)af(f(a,b),b)\ne a

判断以下公式的可满足性

F:f(f(f(a)))=af(f(f(f(f(a)))))=af(a)aF:f(f(f(a)))=a\wedge f(f(f(f(f(a)))))=a\wedge f(a)\ne a

建立子项集合SFS_F

SF={a,f(a),f2(a),f3(a),f4(a),f5(a)}S_F = \{a,f(a),f^2(a),f^3(a),f^4(a),f^5(a)\}

构造SFS_F 上的初始同余关系:

{{a},{f(a)},{f2(a)},{f3(a)},{f4(a)},{f5(a)}}\{\{a\},\{f(a)\},\{f^2(a)\},\{f^3(a)\},\{f^4(a)\},\{f^5(a)\}\}

f3(a)=af^3(a) = a,合并{f3(a)}\lbrace f^3(a) \rbrace{a}\lbrace a \rbrace

{{a,f3(a)},{f(a)},{f2(a)},{f4(a)},{f5(a)}}\{\{a,f^3(a)\},\{f(a)\},\{f^2(a)\},\{f^4(a)\},\{f^5(a)\}\}

f3(a)af^3(a)\sim a,推导出f4(a)f(a)f^4(a)\sim f(a)

{{a,f3(a)},{f(a),f4(a)},{f2(a)},{f5(a)}}\{\{a,f^3(a)\},\{f(a),f^4(a)\},\{f^2(a)\},\{f^5(a)\}\}

f4(a)f(a)f^4(a)\sim f(a),推导出f5(a)f2(a)f^5(a)\sim f^2(a)

{{a,f3(a)},{f(a),f4(a)},{f2(a),f5(a)}}\{\{a,f^3(a)\},\{f(a),f^4(a)\},\{f^2(a),f^5(a)\}\}

f5(a)=af^5(a)=a,合并{f2(a),f5(a)}\lbrace f^2(a),f^5(a) \rbrace

{{a,f2(a),f3(a),f5(a)},{f(a),f4(a)}}\{\{a,f^2(a),f^3(a),f^5(a)\},\{f(a),f^4(a)\}\}

f3(a)f2(a)f^3(a)\sim f^2(a),推导出f4(a)f3(a)f^4(a)\sim f^3(a)

{{a,f(a),f2(a),f3(a),f4(a),f5(a)}}\{\{a,f(a),f^2(a),f^3(a),f^4(a),f^5(a)\}\}

这就是SFS_F的同余闭包。

FF声称f(a)af(a)\ne a,而f(a)af(a)\sim a,所以unsatunsat

实现同余闭包算法的底层算法:并查集

1.3.3 性质

  • 可靠性与完备性:如果同余闭包算法返回satsat那么量词自由的FF就是TEsatT_E-sat

  • 复杂度:O(e2)O(e^2)(参见并查集算法)

二、数组的判定理论

2.1 核心逻辑

TAT_A可满足性判定归约为TET_E可满足性判定。

如果一个ΣZ\Sigma_Z-公式FF不包含任何写项:

  • 将每个数组变量aa与一个新的(fresh)函数符号faf_a关联起来

  • 将每个读项a[i]a[i]替换为fa(i)f_a(i)判断并返回得到的公式的TET_E可满足性;否则,取一个项aiv[j]a\langle i\triangleleft v\rangle [j],并分为两种情况:

    • F[aiv[j]]F[a\langle i\triangleleft v\rangle [j]]替换为F1:F[v]i=jF_1:F[v]\wedge i=j

    • F[aiv[j]]F[a\langle i\triangleleft v\rangle [j]]替换为F2:F[a[j]]ijF_2:F[a[j]]\wedge i\ne j

  • 递归地对F1F_1F2F_2做以上处理。只要有一个分支是satsat,那么返回satsat

  • 否则,返回unsatunsat

举例:判断以下公式的可满足性

F:i1=ji1i2a[j]=v1ai1v1i2v2[j]a[j]F:i_1 = j\wedge i_1\ne i_2 \wedge a[j]=v_1 \wedge a\langle i_1 \triangleleft v_1 \rangle \langle i_2 \triangleleft v_2 \rangle [j]\ne a[j]

FF本身知,i2ji_2 \ne j

F2:i1=ji1i2a[j]=v1ai1v1[j]a[j]i2jF_2:i_1=j\wedge i_1\ne i_2\wedge a[j] = v_1\wedge a\langle i_1\triangleleft v_1\rangle [j]\ne a[j]\wedge i_2\ne j

其中有一个写项,所以分为两种情况:

F3:i1=ji1i2a[j]=v1v1a[j]i2ji1=jF_3:i_1 =j\wedge i_1\ne i_2 \wedge a[j]=v_1 \wedge v_1\ne a[j]\wedge i_2\ne j\wedge i_1 =j

F4:i1=ji1i2a[j]=v1a[j]a[j]i2ji1jF_4:i_1=j\wedge i_1\ne i_2\wedge a[j]=v_1 \wedge a[j]\ne a[j]\wedge i_2\ne j\wedge i_1\ne j

二者都是不可满足的。

所有的分支都是unsatunsat,所以得出结论:FFTAT_A-不可满足的。

2.2 性质

  • 可靠性与完备性:给定一个ΣA\Sigma_A公式FF,以上判定算法返回satsat当且仅当FFTAT_A-可满足的,否则,它返回unsatunsat

  • 复杂度:这是一个NP完全问题

上传的附件

发送私信

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

79
文章数
34
评论数
eject