Tattoo的文章

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


    版权声明:本文为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][P]c[Q]意思是:

    如果我们从一个满足PPP的环境开始执行ccc
    那么ccc一定终止
    且它的最终的环境满足QQQ

    二、良基关系(Well-Founded Relations)集合SSS上的一个二元关系≺\prec≺是一个良基关系,当且仅当:

    在SSS中不存在无限序列s1,s2,s3,..s_1,s_2,s_3,..s​1​​,s​2​​,s​3​​,..,使得对于所有i>0i > 0i>0都有si+1≺sis_{i+1}\prec s_is​i+1​​≺s​i​​
    也就是说,SSS中每个下降序列都是有限的

    2.1 词法意义上的良基关系给定集合S1,..,SnS_1,.. ,S_nS​1​​,..,S​n​​和关系≺1,..,≺n\prec_1 ,.. ,\prec_n≺​1​​,..,≺​n​​ ,令S1×..×S_1\times .. \timesS​1​​×..×
    定义关系≺\prec≺:
    (s1,..,sn)≺(t1,..,tn)⇔⋁i=1n(si≺iti∧⋀j=1i−1sj=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)(s​1​​,..,s​n​​)≺(t​1​​,..,t​n​​)⇔⋁​i=1​n​​(s​i​​≺​i​​t​i​​∧⋀​j=1​i−1​​s​j​​=t​j​​)解释一下,(s1,..,sn)≺(t1,..,tn)(s_1 ,.. ,s_n)\prec (t_1 ,.. ,t_n)(s​1​​,..,s​n​​)≺(t​1​​,..,t​n​​)当且仅当:

    在某一位置iii,si≺itis_i\prec_i t_is​i​​≺​i​​t​i​​
    而对于所有之前的位置jjj,sj=tjs_j=t_js​j​​=t​j​​

    2.2 证明完全正确性为了证明程序终止,我们需要:

    在程序的状态上构造一个良基关系≺\prec≺
    证明每一个基础路径的的输出状态都“小于”输入状态

    如果满足以上两点,那么程序一定终止,否则就存在一个程序状态的无限序列,这可以被映射到≺\prec≺上的一个无限下降序列。
    与以上两步相对应,我们需要:

    找到一个函数δ\deltaδ将程序状态映射到一个带有已知良基关系≺\prec≺的集合SSS
    证明δ\deltaδ在每一个基础路径上依据≺\prec≺都是下降的

    函数δ\deltaδ被称为秩函数(ranking function)。
    2.3 对于秩函数的注释我们用带有↓\downarrow↓的代码注释秩函数,需要在函数的循环头位置注释。
    2.4 vcvcvcvc即为:
    P→wlp(c1;..;cn,δ(x)≺δ(x′))[x/x′]P\to wlp(c_1; .. ;c_n,\delta (x)\prec \delta (x'))[x/x']P→wlp(c​1​​;..;c​n​​,δ(x)≺δ(x​′​​))[x/x​′​​]计算的时候用x′x^{\prime}x​′​​代表开始时xxx的值,计算完毕后再换回来。
    0  留言 2020-07-03 14:32:32
  • 程序验证(十一):演绎验证(下)


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

    一、新特征引入向Imp语言引入新的特征:

    断言注释(assertion annotation)
    过程(procedure)

    1.1 断言断言注释具有以下形式:
    {P}\{P\}{P}从语义上说,它们与运行时断言(runtime assertion)一样(比如c里面的assert)。如果当前环境使得断言表达式为假,程序停止执行。
    1.2 程序举个例子:

    这个过程就是一个带有注释的过程:

    前置条件由requires注释
    后置条件由ensures注释
    前置条件与后置条件中的自由变量可以是形式参数
    后置条件也可以包括特殊的变量rvrvrv,代表返回值(return value)

    二、部分正确性的证明一个程序(program)是部分正确的,如果对于它的每个过程(procedure)PPP都有:

    只要PPP的前置条件在过程的入口处被满足
    那么PPP的后置条件一定在过程的出口处被满足

    我们从基本思路:

    使用注释(annotation)把程序分为更简单的几部分
    独立地为每个部分生成vcvcvc,假定每个注释都成立
    根据每个部分的正确性,推出整体的正确性

    2.1 基本路径(Basic Paths)一个基本路径是一系列指令,满足:

    开始于一个过程的前置条件或循环不变量
    终止于一个循环不变量,一个断言或一个过程的后置条件
    不穿过循环:循环不变量只在路径的开头或结尾出现

    2.2 假设(assume)语句assume b的意思:

    只有当b在当前环境下为真,路径的剩余部分才可以执行
    当讨论剩余的路径时,我们可以假定b成立

    2.3 路径分割每一个assume,都引入两个分支,一个假定bbb成立,一个假定¬b\neg b¬b成立,所以在之前的例子里,有更多的基本路径。
    如何计算基本路径有多少呢?当我们计算基础路径的数量时,我们遵循深度优先的习惯。
    当遇到一个assume时:

    先假定它成立,然后生成相应的路径
    再假定它不成立,重复

    2.4 过程调用(Procedure Call)可以把过程调用替换为后置条件断言,需要引入另一个基础路径以确保前置条件成立,将前置条件与后置条件中的形式参数换为在调用中真正出现的参数。
    综上,过程调用的步骤为:
    1.给定一个过程fff具有以下原型:

    2.当fff在上下文w:=f(e1,..,en)w:=f(e_1 ,.. ,e_n)w:=f(e​1​​,..,e​n​​)中被调用时,用断言{P[e1,..,en]}\lbrace P[e_1,.. ,e_n] \rbrace{P[e​1​​,..,e​n​​]}表示调用上下文
    3.在穿过调用的路径中

    创建新的变量vvv来存放返回值
    将调用替换为后置条件的假定:


    三、vc生成当我们列举基础路径时,我们实际上得到了vcvcvc。
    注意,由于基础路径不穿过循环,所以我们只需要为三种命令生成vcvcvc:

    赋值:见上文
    序列:见上文
    assume:


    举例:
    0  留言 2020-07-03 10:12:16
  • 程序验证(十):演绎验证(上)


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

    一、基础路径(Basic Approach)给定一个程序ccc,由以下specification注解:
    {P}c{Q}\{P\}c\{Q\}{P}c{Q}为了证明这个三元组,我们构造一个验证条件(verification condition, VC)的集合:

    每个VC都是某个理论的一阶公式
    如果所有的VC都是永真的,那么{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace{P}c{Q}就是永真的

    二、谓词转换器给定一个断言QQQ和一个程序ccc,一个谓词转换器(predicate transformer)是一个函数,输出另一个断言。
    最弱前置条件(weakest precondition)谓词转换器产生一个wp(c,Q)wp(c,Q)wp(c,Q),使得:

    对于[wp(c,Q)]c[Q][wp(c,Q)]c[Q][wp(c,Q)]c[Q]是永真的,且
    对于任何满足[P]c[Q][P]c[Q][P]c[Q]的PPP,P⇒wp(c,Q)P\Rightarrow wp(c,Q)P⇒wp(c,Q),也就是说,wp(c,Q)wp(c,Q)wp(c,Q)是这种断言中最弱的

    广义最弱前置条件(weakest liberal precondition)谓词转换器产生一个wlp(c,Q)wlp(c,Q)wlp(c,Q),使得:

    对于wlp(c,Q)cQ{wlp(c,Q)}c{Q}wlp(c,Q)cQ是永真的,且
    对于wlp(c,Q)wlp(c,Q)wlp(c,Q)是这种断言中最弱的

    wlpwlpwlp为我们提供了一种逆向的思路,这也符合我们的直觉。
    三、wlp的定义我们用霍尔三元组来定义wlpwlpwlp:
    wlp(y:=x+1,(∀x.x<z→x<y)→x+1≤y)=?wlp(y:=x+1, (\forall x.x < z \to x < y) \to x+1\le y)=?wlp(y:=x+1,(∀x.x<z→x<y)→x+1≤y)=?注意,答案并不是:
    (∀x.x<z→x<x+1)→x+1≤x+1(\forall x.x < z\to x < x+1) \to x+1 \le x+1(∀x.x<z→x<x+1)→x+1≤x+1因为当我们用x+1x+1x+1替换yyy以处理:
    (∀x.x<z→x<y)(\forall x.x < z\to x < y)(∀x.x<z→x<y)时,变量xxx是被捕获的(captured)
    3.1 捕获避免代入(capture-avoiding substitution)当我们扩展P[a/x]P[a/x]P[a/x]时,我们需要:

    只代入xxx的自由形式(free occurence)
    将aaa中不自由的变量重命名以避免捕获

    3.2 数组赋值规则数组赋值的霍尔规则可以表示为:
    AsgnArr {Q[x⟨a1◃a2⟩/x]}x[a1]:=a2{Q}AsgnArr~\frac{}{\{Q[x\langle a_1\triangleleft a_2\rangle /x]\}x[a_1]:=a_2\{Q\}}AsgnArr ​{Q[x⟨a​1​​◃a​2​​⟩/x]}x[a​1​​]:=a​2​​{Q}​​​​相应的转换器即为:
    wlp(x[a1]:=a2,Q)=Q[x⟨a1◃a2⟩/x]wlp (x[a_1]:=a_2,Q)=Q[x\langle a_1\triangleleft a_2\rangle /x]wlp(x[a​1​​]:=a​2​​,Q)=Q[x⟨a​1​​◃a​2​​⟩/x]举例:计算
    wlp(b[i]:=5,b[i]=5)wlp(b[i]:=5,b[i]=5)wlp(b[i]:=5,b[i]=5)wlp(b[i]:=5,b[i]=5)=(b⟨◃5⟩[i]=5)=(5=5)=truewlp(b[i]:=5,b[i]=5)=(b\langle\triangleleft 5\rangle [i]=5)=(5=5)=truewlp(b[i]:=5,b[i]=5)=(b⟨◃5⟩[i]=5)=(5=5)=true计算
    wlp(b[n]:=x,∀i.1≤i<n→b[i]≤b[i+1])wlp(b[n]:=x,\forall i.1\le i < n\to b[i]\le b[i+1])wlp(b[n]:=x,∀i.1≤i<n→b[i]≤b[i+1])进行代入
    wlp(b[n]:=x,∀i.1≤i<n→b[i]≤b[i+1])=∀i.1≤i<n→(b⟨◃x⟩)[i]≤(b⟨n◃x⟩)[i+1]=(b⟨n◃x⟩)[n−1]≤(b⟨n◃x⟩)[n]∧∀i.1≤i<n−1→(b⟨n◃x⟩)[i]≤(b⟨n◃x⟩)[i+1]wlp(b[n]:=x,\forall i.1\le i < n\to b[i]\le b[i+1])=\forall i.1\le i < n\to (b\langle\triangleleft x\rangle)[i]\le (b\langle n\triangleleft x\rangle)[i+1]=(b\langle n\triangleleft x\rangle)[n-1]\le (b\langle n\triangleleft x\rangle)[n]\wedge \forall i.1\le i < n-1\to (b\langle n\triangleleft x\rangle)[i]\le (b\langle n\triangleleft x\rangle)[i+1]wlp(b[n]:=x,∀i.1≤i<n→b[i]≤b[i+1])=∀i.1≤i<n→(b⟨◃x⟩)[i]≤(b⟨n◃x⟩)[i+1]=(b⟨n◃x⟩)[n−1]≤(b⟨n◃x⟩)[n]∧∀i.1≤i<n−1→(b⟨n◃x⟩)[i]≤(b⟨n◃x⟩)[i+1]3.3 序列(sequencing)依据霍尔规则:
    Seq {P}c1{P′}{P′}c2{Q}{P}c1;c2{Q}Seq~\frac{\{P\}c_1\{P'\}\qquad\{P'\}c_2\{Q\}}{\{P\}c_1;c_2\{Q\}}Seq ​{P}c​1​​;c​2​​{Q}​​{P}c​1​​{P​′​​}{P​′​​}c​2​​{Q}​​相应的谓词转换器即为:
    wlp(c1;c2,Q)=wlp(c1,wlp(c2,Q))wlp(c_1;c_2,Q)=wlp(c_1,wlp(c_2,Q))wlp(c​1​​;c​2​​,Q)=wlp(c​1​​,wlp(c​2​​,Q))3.4 条件依据霍尔规则:

    相应的转换器即为:

    3.5 while循环依据等价关系:

    相应的wlpwlpwlp即为,此处略,最后转了个圈又回来了。
    3.6 近似最弱前置条件一般来说,我们无法总是算出循环的wlpwlpwlp,比如上面的情况。但是,我们可以借助于循环不变式来近似它。
    下面,我们使用这种方式表示循环:
    while b do{I}cwhile~b~do\{I\}cwhile b do{I}c这里III是由程序员提供的循环不变量。
    最为直观的想法是令:
    wlp(while b do{I}c,Q)=Iwlp(while~b~do\{I\}c,Q)=Iwlp(while b do{I}c,Q)=I但此时III可能不是最弱的前置条件。
    如果我们草率地认为:
    wlp(while b do{I}c,Q)=Iwlp(while~b~do\{I\}c,Q)=Iwlp(while b do{I}c,Q)=I我们漏了两件事情:

    没有检查I∧¬bI\wedge\neg bI∧¬b得到QQQ
    我们不知道III是否真的是一个循环不变式

    所以我们需要构造一个额外的验证条件(verification condition)的集合:

    为了在执行循环后确保QQQ能够实现,需要满足两个条件:

    一是vc(while b doIc,Q)vc(while~b~do{I}c,Q)vc(while b doIc,Q)中的每一个公式都是永真的
    二是wlp(while b doIc,Q)=Iwlp(while~b~do{I}c,Q)=Iwlp(while b doIc,Q)=I一定是永真的

    3.7 构造vcwhile是唯一一个引入额外条件的命令,但是其他的声明可能也包含循环,所以:
    vc(x:=a,Q)=∅vc(x:=a,Q)=\varnothingvc(x:=a,Q)=∅vc(c1;c2,Q)=vc(c1,wlp(c2,Q))∪vc(c2,Q)vc(c_1;c_2,Q)=vc(c_1,wlp(c_2,Q))\cup vc(c_2,Q)vc(c​1​​;c​2​​,Q)=vc(c​1​​,wlp(c​2​​,Q))∪vc(c​2​​,Q)vc(if b then c1 else c2,Q)=vc(c1,Q)∪vc(c2,Q)vc(if~b~then~c_1~else~c_2,Q)=vc(c_1,Q)\cup vc(c_2,Q)vc(if b then c​1​​ else c​2​​,Q)=vc(c​1​​,Q)∪vc(c​2​​,Q)3.8 综合综上,我们得到验证:
    {P}c{Q}\{P\}c\{Q\}{P}c{Q}的通用方法:

    计算P′=wlp(c,Q)P^{\prime}=wlp(c,Q)P​′​​=wlp(c,Q)
    计算vc(c,Q)vc(c,Q)vc(c,Q)
    检查P→P′P\to P^{\prime}P→P​′​​ 的永真性
    检查每个F∈vc(c,Q)F\in vc(c,Q)F∈vc(c,Q)的永真性

    若3,4检验均通过,那么{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace{P}c{Q}是永真的,但反之不一定成立,因为循环不变式可能不是最弱的前置条件。
    0  留言 2020-07-02 19:18:16
  • 程序验证(九):程序正确性规范


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

    什么是程序的正确性?应当在指定的前提下,进行预定的行为,达到指定的结果。
    一、部分正确性(Partial Correctness)部分正确性指的是一个程序的停止行为。
    我们将部分正确性用霍尔三元组(Hoare triples)表达:
    {P}c{Q}\{P\}c\{Q\}{P}c{Q}
    其中ccc是一个程序
    其中PPP和QQQ是一阶逻辑的断言(assertion)
    其中P,QP, QP,Q的自由变量可以在程序的变量中随意选择
    其中PPP是先验条件(precondition),QQQ是后验条件(postcondition)

    上述{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace{P}c{Q}的含义:

    在一个满足PPP的环境中开始执行ccc
    如果ccc终止,那么它的最终环境将满足QQQ

    注意,部分正确性没有排除以下两点:

    程序执行不终止
    程序没有从PPP开始执行

    二、完全正确性(Total Correctness)部分正确性没有要求终止,完全正确性是一个更强的声明,写作:
    [P]c[Q][P]c[Q][P]c[Q]
    如果我们从一个满足PPP的环境开始执行ccc
    那么ccc一定终止,而且它最终的环境满足QQQ

    三、断言给定三元组:
    {P}c{Q}\{P\}c\{Q\}{P}c{Q}公式PPP与QQQ是一阶断言。
    对于Imp,有用的理论是TZ∪TAT_Z\cup T_AT​Z​​∪T​A​​。PPP或QQQ中的变量包括程序变量、量词变量、其他逻辑变量,即
    vars(Q)=pvars(Q)∪qvars(Q)∪lvars(Q)vars(Q)=pvars(Q)\cup qvars(Q)\cup lvars(Q)vars(Q)=pvars(Q)∪qvars(Q)∪lvars(Q)3.1 断言的语义由于lvars(Q)lvars(Q)lvars(Q)的存在,我们不能仅依据环境σ\sigmaσ来判断QQQ的值,所以,令α\alphaα为lvars(Q)lvars(Q)lvars(Q)的变量的一个赋值,那么:

    断言的可满足性与永真性:

    如果对于所有σ\sigmaσ,σ⊨Q\sigma\models Qσ⊨Q,那么我们写作⊨Q\models Q⊨Q。
    3.2 部分正确性的语义我们说{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace{P}c{Q}在σ\sigmaσ中在α\alphaα下永真,写作σ⊨α{P}c{Q}\sigma\models_{\alpha} \lbrace P \rbrace c \lbrace Q \rbraceσ⊨​α​​{P}c{Q},如果:
    ∀σ′.(σ⊨αP∧⟨c,σ⟩⇓σ′)→σ′⊨αQ\forall \sigma^{\prime}.(\sigma\models_{\alpha}P\wedge \langle c,\sigma\rangle\Downarrow\sigma^{\prime})\to\sigma^{\prime}\models_{\alpha}Q∀σ​′​​.(σ⊨​α​​P∧⟨c,σ⟩⇓σ​′​​)→σ​′​​⊨​α​​Q也就是说:

    只要σ\sigmaσ在α\alphaα下满足PPP
    而且ccc在σ\sigmaσ中执行得到σ′\sigma^{\prime}σ​′​​
    那么σ′\sigma^{\prime}σ​′​​ 在α\alphaα下满足QQQ

    我们说{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace{P}c{Q}是永真的,写作⊨{P}c{Q}\models \lbrace P \rbrace c \lbrace Q \rbrace⊨{P}c{Q},如果:
    ∀σ,α.σ⊨α{P}c{Q}\forall \sigma,\alpha.\sigma\models_{\alpha} \{P\}c\{Q\}∀σ,α.σ⊨​α​​{P}c{Q}也就是:
    ∀σ,σ′,α.(σ⊨αP∧⟨c,σ⟩⇓σ′)→σ′⊨αQ\forall \sigma,\sigma',\alpha. (\sigma\models_{\alpha}P\wedge\langle c,\sigma\rangle\Downarrow\sigma') \to \sigma'\models_{\alpha} Q∀σ,σ​′​​,α.(σ⊨​α​​P∧⟨c,σ⟩⇓σ​′​​)→σ​′​​⊨​α​​Q四、三元组的证明(verify)我们将引入一种逻辑,该逻辑能从已知的三元组推出新的三元组,这种逻辑叫做霍尔逻辑(Hoare logic)。
    引入规则的形式为:
    ⊢{P}c{Q}\vdash \{P\}c\{Q\}⊢{P}c{Q}4.1 跳过与赋值(skip&assignment)Skip {P}skip{P}Skip~\frac{}{\{P\} skip \{P\}}Skip ​{P}skip{P}​​​​Asgn {Q[a/x]}x:=a{Q}Asgn~ \frac{}{\{Q[a/x]\}x:=a\{Q\}}Asgn ​{Q[a/x]}x:=a{Q}​​​​其中Q[a/x]Q[a/x]Q[a/x]:在QQQ中把所有xxx换成aaa,举个例子:
    (5+x)[(x+1)/x]=5+(x+1)(5+x)[(x+1)/x]=5+(x+1)(5+x)[(x+1)/x]=5+(x+1)4.2 逻辑的加强与削弱注意,我们不能证明一个很显而易见的东西:
    ⊢{y=0}x:=1{x=1}\vdash\{y=0\}x:=1\{x=1\}⊢{y=0}x:=1{x=1}但我们可以证明:
    ⊢{1=1}x:=1{x=1}\vdash\{1=1\}x:=1\{x=1\}⊢{1=1}x:=1{x=1}于是引入前提加强(precondition strengthening):
    Pre ⊢{P′}c{Q}P⇒P′{P}c{Q}Pre~\frac{\vdash\{P'\}c\{Q\}\qquad P\Rightarrow P'}{\{P\}c\{Q\}}Pre ​{P}c{Q}​​⊢{P​′​​}c{Q}P⇒P​′​​​​例如:
    Pre Asgn ⊢{1=1}x:=1{x=1}y=0⇒1=1{y=0}x:=1{x=1}Pre~\frac{Asgn~\frac{}{\vdash\{1=1\}x:=1\{x=1\}}\qquad y=0\Rightarrow 1=1}{\{y=0\}x:=1\{x=1\}}Pre ​{y=0}x:=1{x=1}​​Asgn ​⊢{1=1}x:=1{x=1}​​​​y=0⇒1=1​​与之相似,引入一削弱后验条件的规则:
    Post ⊢{P}c{Q′}Q′⇒Q{P}c{Q}Post~\frac{\vdash\{P\}c\{Q'\}\qquad Q'\Rightarrow Q}{\{P\}c\{Q\}}Post ​{P}c{Q}​​⊢{P}c{Q​′​​}Q​′​​⇒Q​​在二者的基础上,引入序列规则(consequence rule):
    Conseq P⇒P′⊢{P′}c{Q′}Q′⇒Q{P}c{Q}Conseq~\frac{P\Rightarrow P'\qquad\vdash \{P'\}c\{Q'\}\qquad Q'\Rightarrow Q}{\{P\}c\{Q\}}Conseq ​{P}c{Q}​​P⇒P​′​​⊢{P​′​​}c{Q​′​​}Q​′​​⇒Q​​4.3 组合(composition)Seq {P}c1{P′}{P′}c2{Q}{P}c1;c2{Q}Seq~\frac{\{P\}c_1\{P'\}\qquad \{P'\}c_2\{Q\}}{\{P\}c_1;c_2\{Q\}}Seq ​{P}c​1​​;c​2​​{Q}​​{P}c​1​​{P​′​​}{P​′​​}c​2​​{Q}​​举例:使用霍尔逻辑证明swap函数
    {x=x′∧y=y′}t:=x;x:=y;y:=t{y=x′∧x=y′}\{x=x'\wedge y=y'\}t:=x;x:=y;y:=t\{y=x'\wedge x=y'\}{x=x​′​​∧y=y​′​​}t:=x;x:=y;y:=t{y=x​′​​∧x=y​′​​}1.由Asgn:
    {x=x′∧y=y′}t:=x{t=x′∧y=y′}\{x=x'\wedge y=y'\}t:=x\{t=x'\wedge y=y'\}{x=x​′​​∧y=y​′​​}t:=x{t=x​′​​∧y=y​′​​}2.由Asgn:
    {t=x′∧y=y′}x:=y{t=x′∧x=y′}\{t=x'\wedge y=y'\}x:=y\{t=x'\wedge x=y'\}{t=x​′​​∧y=y​′​​}x:=y{t=x​′​​∧x=y​′​​}3.由Asgn:
    {t=x′∧x=y′}y:=t{y=x′∧x=y′}\{t=x'\wedge x=y'\}y:=t\{y=x'\wedge x=y'\}{t=x​′​​∧x=y​′​​}y:=t{y=x​′​​∧x=y​′​​}4.由1,2,Seq:
    {x=x′∧y=y′}t:=x;x:=y{t=x′∧x=y′}\{x=x'\wedge y=y'\}t:=x;x:=y\{t=x'\wedge x=y'\}{x=x​′​​∧y=y​′​​}t:=x;x:=y{t=x​′​​∧x=y​′​​}5.最后,由3,4,Seq:
    Q.E.DQ.E.DQ.E.D4.4 条件(conditional)If {P∧b}c1{Q}{P∧¬b}c2{Q}{P}if b then c1 else c2{Q}If~\frac{\{P\wedge b\}c_1\{Q\}\qquad \{P\wedge \neg b\}c_2\{Q\}}{\{P\} if~b~then~c_1~else~c_2\{Q\}}If ​{P}if b then c​1​​ else c​2​​{Q}​​{P∧b}c​1​​{Q}{P∧¬b}c​2​​{Q}​​
    在true分支:如果bbb成立,我们需要证明{P∧b}c1Q\lbrace P\wedge b \rbrace c_1{Q}{P∧b}c​1​​Q
    在false分支:如果¬b\neg b¬b成立,我们需要证明{P∧¬b}c2{Q}\lbrace P\wedge\neg b \rbrace c_2 \lbrace Q \rbrace{P∧¬b}c​2​​{Q}

    4.5 while循环(loop)While {P∧b}c{P}{P}while b do c{P∧¬b}While~\frac{\{P\wedge b\}c\{P\}}{\{P\} while~b~do~c\{P\wedge\neg b\}}While ​{P}while b do c{P∧¬b}​​{P∧b}c{P}​​其中,PPP是循环不变量(loop invariant):

    在进入循环前成立,并且在每次迭代后保持不变
    这由前提{P∧b}c{P}\lbrace P\wedge b \rbrace c \lbrace P \rbrace{P∧b}c{P}所确定

    为了使用While,需要先证明PPP是不变量。
    五、可靠性与完备性
    之前的规则对于部分正确性都是可靠的
    对于Imp,是不完备的,因为可以归约为TPAT_{PA}T​PA​​
    0  留言 2020-07-02 09:43:51
  • 程序验证(八):形式语义


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

    一、语义描述方法
    操作语义:用抽象机描述程序执行引起的状态改变,关心状态改变是怎样产生的,与语言的实现关系紧密
    指称语义:使程序执行的效果对应数学对象,只关心程序执行的效果,不关心其是怎样产生的
    公理语义:将程序的语义性质表示为命题,采用数理逻辑的方法研究

    二、引入玩具语言Imp2.1 语法范畴
    数字集NumNumNum,用nnn表示数字
    变元集VarVarVar,用xxx表示变元
    算术表达式集AexpAexpAexp,用aaa表示算术表达式
    布尔表达式集BexpBexpBexp,用bbb表示布尔表达式
    语句集ComComCom,用ccc表示语句

    2.2 语法a∈AExp::=n∈Z∣x∈Var∣a1+a2∣a1∗a2∣a1−a2a\in AExp::=n\in Z |x\in Var|a_1+a_2|a_1*a_2|a_1-a_2a∈AExp::=n∈Z∣x∈Var∣a​1​​+a​2​​∣a​1​​∗a​2​​∣a​1​​−a​2​​b∈BExp::=true∣false∣a1=a2∣a1≤a2∣¬b∣b1∧b2b\in BExp::=true|false|a_1=a_2|a_1\le a_2|\neg b|b_1\wedge b_2b∈BExp::=true∣false∣a​1​​=a​2​​∣a​1​​≤a​2​​∣¬b∣b​1​​∧b​2​​c∈Com::=skip∣x:=a∣c1;c2∣if b then c1 else c2∣while b do cc\in Com::=skip|x:=a|c_1;c_2|if~b~then~c_1~else~c_2|while~b~do~cc∈Com::=skip∣x:=a∣c​1​​;c​2​​∣if b then c​1​​ else c​2​​∣while b do c三、表达式语义3.1 表达式的语义采用二进制
    n::=0∣1∣n0∣n1n::=0|1|n0|n1n::=0∣1∣n0∣n1语义函数N:Num→ZN: Num \to ZN:Num→Z
    N[0]=0N[0]=0N[0]=0
    N[1]=1N[1]=1N[1]=1
    N[n0]=2∗N[0]N[n0]=2*N[0]N[n0]=2∗N[0]
    N[n1]=2∗N[n]+1N[n1]=2*N[n]+1N[n1]=2∗N[n]+1
    3.2 状态环境是从变元集到整数集的函数
    Env=Var→ZEnv=Var \to ZEnv=Var→Z
    如σ=[x↦5,y↦7,z↦0]\sigma = [x \mapsto 5,y \mapsto 7,z \mapsto 0]σ=[x↦5,y↦7,z↦0],即σx=5,σy=7,σz=0\sigma x=5,\sigma y=7,\sigma z=0σx=5,σy=7,σz=0
    设σ′=σ[x↦7]\sigma^{\prime} =\sigma [x\mapsto 7]σ​′​​=σ[x↦7],则σ′x=7\sigma^{\prime} x=7σ​′​​x=7,对于不同于xxx的变元yyy,yσ′y=σyy\sigma^{\prime} y=\sigma yyσ​′​​y=σy

    状态是一个二元组⟨c,σ⟩\langle c,\sigma\rangle⟨c,σ⟩,其中σ\sigmaσ是当前变量的赋值,ccc为下一条被执行的语句。
    3.3 算术表达式的语义语义函数A:Aexp→(Env→Z)A: Aexp\to (Env\to Z)A:Aexp→(Env→Z):

    A[n]σ=N[n]A[n]\sigma = N[n]A[n]σ=N[n]
    A[x]σ=σxA[x]\sigma = \sigma xA[x]σ=σx
    A[a1+a2]σ=A[a1]σ+A[a2]σA[a_1+a_2]\sigma = A[a_1]\sigma +A[a_2]\sigmaA[a​1​​+a​2​​]σ=A[a​1​​]σ+A[a​2​​]σ
    A[a1a2]σ=A[a1]σA[a2]σA[a_1a_2]\sigma = A[a_1]\sigma A[a_2]\sigmaA[a​1​​a​2​​]σ=A[a​1​​]σA[a​2​​]σ
    A[a1−a2]σ=A[a1]σ−A[a2]σA[a_1-a_2]\sigma = A[a_1]\sigma -A[a_2]\sigmaA[a​1​​−a​2​​]σ=A[a​1​​]σ−A[a​2​​]σ

    3.4 布尔表达式的语义语义函数B:Bexp→(Env→T)B:Bexp\to (Env\to T)B:Bexp→(Env→T):
    B[true]σ=trueB[true]\sigma = trueB[true]σ=true
    B[false]σ=falseB[false]\sigma = falseB[false]σ=false
    B[a1=a2]σ=A[a1]σ=A[a2]σB[a_1=a_2]\sigma = A[a_1]\sigma = A[a_2]\sigmaB[a​1​​=a​2​​]σ=A[a​1​​]σ=A[a​2​​]σ
    B[a1≤a2]σ=A[a1]σ≤A[a2]σB[a_1\le a_2]\sigma = A[a_1]\sigma\le A[a_2]\sigmaB[a​1​​≤a​2​​]σ=A[a​1​​]σ≤A[a​2​​]σ
    B[¬b]σ=¬B[b]σB[\neg b]\sigma = \neg B[b]\sigmaB[¬b]σ=¬B[b]σ
    B[b1∧b2]σ=B[b1]σ∧B[b2]σB[b_1\wedge b_2]\sigma = B[b_1]\sigma\wedge B[b_2]\sigmaB[b​1​​∧b​2​​]σ=B[b​1​​]σ∧B[b​2​​]σ
    3.5 举例在环境σ=[x↦1,y↦3]\sigma = [x\mapsto 1,y\mapsto 3]σ=[x↦1,y↦3]下计算表达式(x+2)∗y(x+2)*y(x+2)∗y的值
    A[(x+2)∗y]σ=A[(x+2)]σ∗A[y]σ=(A[x]σ+A[2]σ)∗A[y]σ=(1+2)∗3=9A[(x+2)*y]\sigma =A[(x+2)]\sigma * A[y]\sigma = (A[x]\sigma +A[2]\sigma) * A[y]\sigma =(1+2)* 3 = 9A[(x+2)∗y]σ=A[(x+2)]σ∗A[y]σ=(A[x]σ+A[2]σ)∗A[y]σ=(1+2)∗3=93.6 代入用算术表达式a0a_0a​0​​替换算术表达式aaa中变元yyy的所有出现得到的算术表达式记为a[y↦a0]a[y\mapsto a_0]a[y↦a​0​​]:
    A[a[y↦a0]]σ=A[a](σ[y↦A[a0]σ])A[a[y\mapsto a_0]]\sigma = A[a](\sigma [y\mapsto A[a_0]\sigma ])A[a[y↦a​0​​]]σ=A[a](σ[y↦A[a​0​​]σ])用算术表达式a0a_0a​0​​替换布尔表达式bbb中变元yyy的所有出现得到的布尔表达式记为b[y↦a0]b[y\mapsto a_0]b[y↦a​0​​]:
    B[b[y↦a0]]σ=B[b](σ[y↦A[a0]σ])B[b[y\mapsto a_0]]\sigma = B[b](\sigma [y\mapsto A[a_0]\sigma])B[b[y↦a​0​​]]σ=B[b](σ[y↦A[a​0​​]σ])四、操作语义4.1 概念包括以下两种:

    结构操作语义(小步操作语义):描述执行语句的各步计算如何发生
    自然语义(大步操作语义):描述如何得到语句执行终止的最终状态

    4.2 结构操作语义结构操作语义强调计算的具体步骤,基于状态之间的迁移关系→\to→来定义,即
    ⟨c,σ⟩→⟨c′,σ′⟩\langle c,\sigma\rangle\to\langle c',\sigma'\rangle⟨c,σ⟩→⟨c​′​​,σ​′​​⟩意义:语句ccc从环境σ\sigmaσ执行到中途,这时环境为σ′\sigma^{\prime}σ​′​​,待执行的语句为c′c^{\prime}c​′​​。
    反复应用上面的迁移关系,直至程序终止状态⟨skip,σ⟩\langle skip, \sigma \rangle⟨skip,σ⟩。
    若无状态⟨c′,σ′⟩\langle c^{\prime}, \sigma^{\prime} \rangle⟨c​′​​,σ​′​​⟩使得⟨c,σ⟩→⟨c′,σ′⟩\langle c,\sigma \rangle \to\langle c^{\prime},\sigma^{\prime} \rangle⟨c,σ⟩→⟨c​′​​,σ​′​​⟩,则称⟨c,σ⟩\langle c,\sigma\rangle⟨c,σ⟩是呆滞的(stuck)。
    4.2.1 Imp的结构操作语义Asgn:⟨x:=a,σ⟩→⟨skip,σ[x↦A[a]σ]⟩Asgn:\frac{}{\langle x:=a,\sigma\rangle\to\langle skip,\sigma [x\mapsto A[a]\sigma]\rangle}Asgn:​⟨x:=a,σ⟩→⟨skip,σ[x↦A[a]σ]⟩​​​​Skip:no ruleSkip:no~ruleSkip:no ruleSeq1:⟨c1,σ⟩→⟨c1′,σ1′⟩⟨c1;c2,σ⟩→⟨c1′;c2,σ′⟩Seq1:\frac{\langle c_1,\sigma\rangle\to\langle c'_1,\sigma'_1\rangle}{\langle c_1;c_2,\sigma\rangle\to\langle c'_1;c_2,\sigma'\rangle}Seq1:​⟨c​1​​;c​2​​,σ⟩→⟨c​1​′​​;c​2​​,σ​′​​⟩​​⟨c​1​​,σ⟩→⟨c​1​′​​,σ​1​′​​⟩​​Seq2:⟨skip;c,σ⟩→⟨c,σ⟩Seq2:\frac{}{\langle skip;c,\sigma\rangle\to\langle c,\sigma\rangle}Seq2:​⟨skip;c,σ⟩→⟨c,σ⟩​​​​IfTrue:⟨if b then c1 else c2,σ⟩→⟨c1,σ⟩IfTrue:\frac{}{\langle if~b~then~c_1~else~c_2,\sigma\rangle\to\langle c_1,\sigma\rangle}IfTrue:​⟨if b then c​1​​ else c​2​​,σ⟩→⟨c​1​​,σ⟩​​​​IfFalse:⟨if b then c1 else c2,σ⟩→⟨c2,σ⟩IfFalse:\frac{}{\langle if~b~then~c_1~else~c_2,\sigma\rangle\to \langle c_2,\sigma\rangle}IfFalse:​⟨if b then c​1​​ else c​2​​,σ⟩→⟨c​2​​,σ⟩​​​​While:⟨while b do c,σ⟩→⟨if b then(c;while b do c)else skip,σWhile:\frac{}{\langle while~b~do~c,\sigma\rangle\to\langle if~b~then(c;while~b~do~c)else~skip,\sigma}While:​⟨while b do c,σ⟩→⟨if b then(c;while b do c)else skip,σ​​​​4.2.2 推导序列语句ccc从环境σ\sigmaσ开始的推导序列有以下两种形式(记γ0=⟨c,σ⟩\gamma_0=\langle c,\sigma\rangleγ​0​​=⟨c,σ⟩):

    有限状态序列γ0,γ1,..,γk\gamma0,\gamma_1,..,\gamma_kγ0,γ​1​​,..,γ​k​​,其中γ0→γ1,..,γ\gamma_0\to \gamma_1,..,\gammaγ​0​​→γ​1​​,..,γ{k-1}\to \gamma_k可以推导得出。γk\gamma_kγ​k​​的形式为⟨skip,σ′⟩\langle skip,\sigma^{\prime} \rangle⟨skip,σ​′​​⟩或者γk\gamma_kγ​k​​是呆滞的
    无限状态序列γ0,γ1,..\gamma_0,\gamma_1,..γ​0​​,γ​1​​,..,其中γ0→γ1\gamma_0\to \gamma_1γ​0​​→γ​1​​,γ1→γ2\gamma_1\to\gamma_2γ​1​​→γ​2​​等可以推导得到
    将γ0→γ1→..→γk\gamma_0\to \gamma_1\to .. \to\gamma_kγ​0​​→γ​1​​→..→γ​k​​简记为γ0→∗γk\gamma_0 \to ^{*}\gamma_kγ​0​​→​∗​​γ​k​​

    4.2.3 确定性结构操作语义具有确定性:对于任意语句ccc,从任意环境σ\sigmaσ出发,只要⟨c,σ⟩→⟨c′,σ′⟩\langle c,\sigma\rangle\to\langle c^{\prime},\sigma^{\prime}\rangle⟨c,σ⟩→⟨c​′​​,σ​′​​⟩且⟨c,σ⟩→⟨c′′,σ′′⟩\langle c,\sigma\rangle\to\langle c^{\prime\prime},\sigma^{\prime\prime}\rangle⟨c,σ⟩→⟨c​′′​​,σ​′′​​⟩,就有σ′=σ′′\sigma^{\prime}=\sigma^{\prime\prime}σ​′​​=σ​′′​​
    4.2.4 终止和循环
    若存在从状态⟨c,σ⟩\langle c,\sigma\rangle⟨c,σ⟩开始的有限推导序列,则称语句ccc从环境σ\sigmaσ执行是终止的
    若存在从状态⟨c,σ⟩\langle c,\sigma\rangle⟨c,σ⟩开始的无限推导序列,则称语句ccc从环境σ\sigmaσ执行是循环的
    若语句ccc从每个环境执行都是终止的,则称语句ccc总是终止的
    若语句ccc从每个环境执行都是循环的,则称语句ccc总是循环的

    4.2.5 语义等价如果对于任意状态σ\sigmaσ,满足下列条件:

    对于任意终止或呆滞格局⟨c′,σ′⟩\langle c^{\prime},\sigma^{\prime}\rangle⟨c​′​​,σ​′​​⟩,⟨c1,σ⟩→∗⟨c′,σ′⟩\langle c_1,\sigma\rangle \to^{*} \langle c^{\prime},\sigma^{\prime}\rangle⟨c​1​​,σ⟩→​∗​​⟨c​′​​,σ​′​​⟩,当且仅当⟨c2,σ⟩→∗⟨c′,σ′⟩\langle c_2,\sigma\rangle \to^{*} \langle c^{\prime},\sigma^{\prime}\rangle⟨c​2​​,σ⟩→​∗​​⟨c​′​​,σ​′​​⟩
    存在从⟨c1,σ⟩\langle c_1,\sigma\rangle⟨c​1​​,σ⟩开始的无限推导序列当且仅当存在从⟨c2,σ⟩\langle c_2,\sigma\rangle⟨c​2​​,σ⟩开始的无限推导序列,则称语句c1c_1c​1​​和c2c_2c​2​​是语义等价的,如语句c1;(c2;c3)c_1;(c_2;c_3)c​1​​;(c​2​​;c​3​​)和语句(c1;c2);c3(c_1;c_2);c_3(c​1​​;c​2​​);c​3​​是语义等价的

    4.2.6 语义函数可将语句ccc的意义概括为从EnvEnvEnv到EnvEnvEnv的部分函数:
    SSOS:Cmd→(Env↪Env)S_{SOS} : Cmd\to(Env\hookrightarrow Env)S​SOS​​:Cmd→(Env↪Env)定义

    例如,SSOS[while true do skip]σ=undefS_{SOS}[while \space true \space do \space skip]\sigma = undefS​SOS​​[while true do skip]σ=undef
    4.3 自然语义自然语义关心语句执行对环境的改变。
    从环境σ\sigmaσ执行语句ccc将终止于环境σ′\sigma^{\prime}σ​′​​:
    ⟨c,σ⟩⇓σ′\langle c,\sigma\rangle\Downarrow \sigma^{\prime}⟨c,σ⟩⇓σ​′​​规则的一般形式:

    4.3.1 Imp的自然语义
    每个规则有若干前提和一个结论。称有0个前提的规则为公理,如BigAsgn, BigSkip, BigWhileFalse是公理。
    当使用公理和规则得出⟨c,σ⟩⇓σ′\langle c,\sigma\rangle\Downarrow \sigma^{\prime}⟨c,σ⟩⇓σ​′​​时,就得到一推导树,树根是⟨c,σ⟩⇓σ′\langle c,\sigma\rangle\Downarrow \sigma^{\prime}⟨c,σ⟩⇓σ​′​​,树叶是公理,每个分支点是某规则的结论,而它的儿子是该规则的前提。
    4.3.2 终止和循环
    若存在环境σ′\sigma^{\prime}σ​′​​使得⟨c,σ⟩⇓σ′\langle c,\sigma\rangle\Downarrow\sigma^{\prime}⟨c,σ⟩⇓σ​′​​,则称语句ccc从环境σ\sigmaσ执行是终止的
    若不存在环境σ′\sigma^{\prime}σ​′​​使得⟨c,σ⟩⇓σ′\langle c,\sigma\rangle\Downarrow \sigma^{\prime}⟨c,σ⟩⇓σ​′​​,则称语句ccc从环境σ\sigmaσ执行是循环的
    若语句ccc从每个环境执行都是终止的,则称语句ccc总是终止的
    若语句ccc从每个环境执行都是循环的,则称语句ccc总是循环的

    4.3.3 语义等价如果对于任意环境σ\sigmaσ和σ′\sigma^{\prime}σ​′​​:
    ⟨c0,σ⟩⇓σ′⇔⟨c1,σ⟩⇓σ′\langle c_0,\sigma\rangle\Downarrow\sigma^{\prime} \Leftrightarrow \langle c_1,\sigma\rangle\Downarrow \sigma^{\prime}⟨c​0​​,σ⟩⇓σ​′​​⇔⟨c​1​​,σ⟩⇓σ​′​​则称语句c0c_0c​0​​和c1c_1c​1​​是语义等价的。
    4.3.4 确定性自然语义具有确定性:对于任意语句ccc,和任意环境σ1,σ2,σ\sigma_1,\sigma_2,\sigmaσ​1​​,σ​2​​,σ,只要⟨c,σ⟩⇓σ1\langle c,\sigma \rangle\Downarrow \sigma_1⟨c,σ⟩⇓σ​1​​且⟨c,σ⟩⇓σ2\langle c,\sigma\rangle\Downarrow \sigma_2⟨c,σ⟩⇓σ​2​​,就有σ1=σ2\sigma_1=\sigma_2σ​1​​=σ​2​​,即
    ∀σ,σ1,σ2,c.(⟨c,σ⟩⇓σ1∧⟨c,σ⟩⇓σ2)→(σ1=σ2)\forall \sigma,\sigma_1,\sigma_2,c.(\langle c,\sigma\rangle\Downarrow\sigma_1\wedge\langle c,\sigma\rangle\Downarrow\sigma_2)\to (\sigma_1 =\sigma_2)∀σ,σ​1​​,σ​2​​,c.(⟨c,σ⟩⇓σ​1​​∧⟨c,σ⟩⇓σ​2​​)→(σ​1​​=σ​2​​)4.3.5 语义函数可将语句ccc的意义概括为从FnvFnvFnv到EnvEnvEnv的部分函数:
    Sns:Cmd→(Env↪Env)S_{ns}: Cmd\to (Env\hookrightarrow Env)S​ns​​:Cmd→(Env↪Env)定义

    4.4 两种语义的对比
    对于语言Imp的每个语句ccc,任意环境σ\sigmaσ和σ′\sigma^{\prime}σ​′​​,若⟨c,σ⟩⇓σ′\langle c,\sigma\rangle\Downarrow \sigma^{\prime}⟨c,σ⟩⇓σ​′​​,则⟨c,σ⟩→∗⟨skip,σ′⟩\langle c,\sigma\rangle\to^{*}\langle skip,\sigma^{\prime} \rangle⟨c,σ⟩→​∗​​⟨skip,σ​′​​⟩
    对于语言Imp的每个语句ccc,任意环境σ\sigmaσ和σ′\sigma^{\prime}σ​′​​ ,若⟨c,σ⟩→k⟨skip,σ′⟩\langle c,\sigma\rangle\to^k\langle skip,\sigma^{\prime}\rangle⟨c,σ⟩→​k​​⟨skip,σ​′​​⟩,则⟨c,σ⟩⇓σ′\langle c,\sigma\rangle\Downarrow\sigma^{\prime}⟨c,σ⟩⇓σ​′​​
    对于语言Imp的每个语句ccc,Sns[c]=SSOS[c]S_{ns}[c]=S_{SOS}[c]S​ns​​[c]=S​SOS​​[c]
    0  留言 2020-07-01 11:58:25
  • 程序验证(七):可满足性模理论(Satisfiability Modulo Theories)


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

    一、SMTSatisfiability Modulo Theories(SMT)是以下情况的公式的判定问题:

    一些一阶理论的复合
    具有任意的布尔结构

    二、DPLL(T): DPLL Modulo Theories这是现代SMT求解器的基础技术。
    将SMT问题分解为可以高效求解的子问题:

    使用SAT求解技术来处理布尔结构(宏观)
    使用专门的理论求解器(theory solver)来判定背景理论的可满足性(微观)

    三、布尔结构通过TTT-公式的语义,我们递归定义公式FFF的布尔结构:

    这里PiP_iP​i​​是布尔变量。
    举例:考虑以下公式
    F:g(a)=c∧(f(g(a))≠f(c)∨g(a)=d)∧c≠dF:g(a)=c\wedge (f(g(a))\ne f(c)\vee g(a)=d)\wedge c\ne dF:g(a)=c∧(f(g(a))≠f(c)∨g(a)=d)∧c≠dFFF的布尔抽象:
    B(F)=B(g(a)=c)∧(B(f(g(a))≠f(c))∨B(g(a)=d))∧B(c≠d)=P1∧(¬P2∨P3)∧¬P4B(F)=B(g(a)=c)\wedge (B(f(g(a))\ne f(c))\vee B(g(a)=d))\wedge B(c\ne d)=P_1 \wedge (\neg P_2\vee P_3)\wedge \neg P_4B(F)=B(g(a)=c)∧(B(f(g(a))≠f(c))∨B(g(a)=d))∧B(c≠d)=P​1​​∧(¬P​2​​∨P​3​​)∧¬P​4​​我们也可以定义B−1B^{-1}B​−1​​,比如B−1(P1∧P3∧P4)B^{-1}(P_1 \wedge P_3 \wedge P_4)B​−1​​(P​1​​∧P​3​​∧P​4​​)就是g(a)=c∧g(a)=d∧c=dg(a)=c\wedge g(a)=d\wedge c=dg(a)=c∧g(a)=d∧c=d
    3.1 布尔抽象为什么称为抽象?因为它实际上是一个过度简化。几个事实:

    如果FFF是satsatsat,那么B(F)B(F)B(F)总是satsatsat
    如果B(F)B(F)B(F)是satsatsat,那么FFF一定是satsatsat吗?不是
    如果FFF是unsatunsatunsat,那么B(F)B(F)B(F)一定是unsatunsatunsat吗?不是
    如果B(F)B(F)B(F)是unsatunsatunsat,那么FFF呢?是

    3.2 T与SAT求解器的结合3.2.1 基本算法
    构造FB:=B(F)F_B:=B(F)F​B​​:=B(F)
    如果FBF_BF​B​​是unsatunsatunsat,那么返回unsatunsatunsat
    否则,获得一个FBF_BF​B​​的赋值α\alphaα
    构造C=⋀i=1nPi↔α(Pi)C=\bigwedge^n_{i=1} P_i\leftrightarrow \alpha (P_i)C=⋀​i=1​n​​P​i​​↔α(P​i​​)
    将B−1(C)B^{-1}(C)B​−1​​(C)发送到TTT-求解器
    如果TTT-求解器判断为satsatsat,那么返回satsatsat
    否则,更新FB:=FB∧¬CF_B :=F_B\wedge \neg CF​B​​:=F​B​​∧¬C,重复以上步骤

    最后一步更新的解释:

    如果不更新,我们的FBF_BF​B​​会得到同样的unsatunsatunsat模型
    其中¬C\neg C¬C叫做理论冲突子句(theory conflict clause)
    更新之后,可以防止求解器未来搜索同样的路径

    3.2.2 举例判断以下公式的可满足性:
    F:g(a)=c∧(f(g(a))≠f(c)∨g(a)=d)∧c≠dF:g(a)=c\wedge (f(g(a))\ne f(c)\vee g(a)=d)\wedge c\ne dF:g(a)=c∧(f(g(a))≠f(c)∨g(a)=d)∧c≠d构造布尔抽象:
    B(F)=P1∧(¬P2∨P3)∧¬P4B(F)=P_1\wedge (\neg P_2\vee P_3)\wedge \neg P_4B(F)=P​1​​∧(¬P​2​​∨P​3​​)∧¬P​4​​找到一个satsatsat赋值(通过SAT求解器):
    α={P1↦1,P2↦0,P3↦1,P4↦0}\alpha =\{P_1\mapsto 1,P_2\mapsto 0,P_3\mapsto 1,P_4\mapsto 0\}α={P​1​​↦1,P​2​​↦0,P​3​​↦1,P​4​​↦0}构造C=P1∧¬P2∧P3∧¬P4C = P_1\wedge \neg P_2\wedge P_3\wedge \neg P_4C=P​1​​∧¬P​2​​∧P​3​​∧¬P​4​​。
    在TTT-求解器中搜索B−1(C)B^{-1}(C)B​−1​​(C):
    g(a)=c∧f(g(a))≠f(c)∧g(a)=d∧c≠dg(a)=c\wedge f(g(a))\ne f(c)\wedge g(a)=d\wedge c\ne dg(a)=c∧f(g(a))≠f(c)∧g(a)=d∧c≠dunsatunsatunsat更新FBF_BF​B​​:
    P1∧(¬P2∨P3)∧¬P4∧(¬P1∨P2∨¬P3∨P4)P_1\wedge (\neg P_2\vee P_3)\wedge \neg P_4\wedge (\neg P_1\vee P_2\vee\neg P_3 \vee P_4)P​1​​∧(¬P​2​​∨P​3​​)∧¬P​4​​∧(¬P​1​​∨P​2​​∨¬P​3​​∨P​4​​)找到一个satsatsat赋值(通过SAT求解器):
    α={P1↦1,P2↦1,P3↦1,P4↦0}\alpha =\{P_1\mapsto 1,P_2\mapsto 1,P_3\mapsto 1,P_4\mapsto 0\}α={P​1​​↦1,P​2​​↦1,P​3​​↦1,P​4​​↦0}构造C=P1∧P2∧P3∧¬P4C=P_1\wedge P_2\wedge P_3\wedge \neg P_4C=P​1​​∧P​2​​∧P​3​​∧¬P​4​​。
    在TTT-求解器中搜索B−1(C)B^{-1}(C)B​−1​​(C):
    g(a)=c∧f(g(a))=f(c)∧g(a)=d∧c≠dg(a)=c\wedge f(g(a))=f(c)\wedge g(a)=d\wedge c\ne dg(a)=c∧f(g(a))=f(c)∧g(a)=d∧c≠dunsatunsatunsat更新FBF_BF​B​​:
    P1∧(¬P2∨P3)∧¬P4∧(¬P1∨P2∨¬P3∨P4)∧(¬P1∨¬P2∨¬P3∨P4)P_1\wedge (\neg P_2\vee P_3)\wedge \neg P_4\wedge (\neg P_1\vee P_2\vee\neg P_3\vee P_4)\wedge (\neg P_1\vee\neg P_2\vee\neg P_3\vee P_4)P​1​​∧(¬P​2​​∨P​3​​)∧¬P​4​​∧(¬P​1​​∨P​2​​∨¬P​3​​∨P​4​​)∧(¬P​1​​∨¬P​2​​∨¬P​3​​∨P​4​​)找到一个赋值:
    α={P1↦1,P2↦0,P3↦0,P4↦0}\alpha = \{P_1\mapsto 1,P_2\mapsto 0,P_3\mapsto 0,P_4\mapsto 0\}α={P​1​​↦1,P​2​​↦0,P​3​​↦0,P​4​​↦0}构造C=P1∧¬P2∧¬P3∧¬P4C=P_1\wedge \neg P_2\wedge \neg P_3\wedge \neg P_4C=P​1​​∧¬P​2​​∧¬P​3​​∧¬P​4​​ 。
    在TTT-求解器中搜索B−1(C)B^{-1}(C)B​−1​​(C):
    g(a)=c∧f(g(a))≠f(c)∧g(a)≠d∧c≠dg(a)=c\wedge f(g(a))\ne f(c)\wedge g(a)\ne d\wedge c\ne dg(a)=c∧f(g(a))≠f(c)∧g(a)≠d∧c≠d更新FBF_BF​B​​:
    P1∧(¬P2∨P3)∧¬P4∧(¬P1∨P2∨¬P3∨P4)∧(¬P1∨¬P2∨¬P3∨P4)∧(¬P1∨P2∨P3∨P4)P_1\wedge (\neg P_2\vee P_3)\wedge \neg P_4\wedge (\neg P_1\vee P_2\vee\neg P_3\vee P_4)\wedge (\neg P_1\vee\neg P_2\vee \neg P_3\vee P_4)\wedge (\neg P_1\vee P_2\vee P_3\vee P_4)P​1​​∧(¬P​2​​∨P​3​​)∧¬P​4​​∧(¬P​1​​∨P​2​​∨¬P​3​​∨P​4​​)∧(¬P​1​​∨¬P​2​​∨¬P​3​​∨P​4​​)∧(¬P​1​​∨P​2​​∨P​3​​∨P​4​​)注意,这个布尔抽象已经是unsatunsatunsat了,所以我们说FFF是unsatunsatunsat了。
    3.2.3 另一个例子考虑这样的TZT_ZT​Z​​-公式FFF:
    F:0<x∧x<1wedge(x<2∨..∨x<99)F:0 < x\wedge x < 1wedge (x < 2\vee .. \vee x < 99)F:0<x∧x<1wedge(x<2∨..∨x<99)布尔抽象:
    P0∧P1∧(P2∨..∨P99)P_0\wedge P_1\wedge (P_2\vee .. \vee P_99)P​0​​∧P​1​​∧(P​2​​∨..∨P​9​​9)一共有298−12^{98}-12​98​​−1个可满足的赋值,但是没有一个满足FFF。然而,我们每次只能添加一个冲突子句!所以我们需要改进。
    四、真正的DPLL(TTT)4.1 思路
    不要把SAT求解器看做一个黑箱
    当构造出赋值的时候,渐进的查询理论求解器
    在之前的例子中,添加{0<x,x<1}\lbrace 0<x,x<1 \rbrace{0<x,x<1}后会立刻停止

    4.2 举例还是之前的例子:

    布尔抽象:B(F)=P1,¬P2,P3,¬P4B(F)={{P_1},{\neg P_2,P_3},{\neg P_4}}B(F)=P​1​​,¬P​2​​,P​3​​,¬P​4​​
    DPLL从P1P_1P​1​​,¬P4\neg P_4¬P​4​​开始
    此时,根据公理,我们有更多的逻辑传递:

    g(a)=c⇒f(g(a))=f(c)g(a)=c\Rightarrow f(g(a))=f(c)g(a)=c⇒f(g(a))=f(c)g(a)=c∧c≠d⇒g(a)≠dg(a)=c\wedge c\ne d\Rightarrow g(a)\ne dg(a)=c∧c≠d⇒g(a)≠d判定¬P2\neg P_2¬P​2​​与P3P_3P​3​​过于冗长,所以我们可以添加一些引理(theory lemmas):
    P1→P2P_1\to P_2P​1​​→P​2​​P1∧¬P4→¬P3P_1\wedge \neg P_4\to \neg P_3P​1​​∧¬P​4​​→¬P​3​​4.3 核(unsat core)我们之前是把¬C\neg C¬C添加到原式,一个不满足核(unsatisfiable core)C∗C^{*}C​∗​​是CCC的一个子集,满足:

    C∗C^{*}C​∗​​依然是不可满足的
    删除C∗C^{*}C​∗​​的任何元素,都使它可满足

    比如
    F:0<x∧x<1∧x<2∧..∧x<99F:0 < x\wedge x < 1\wedge x < 2\wedge .. \wedge x < 99F:0<x∧x<1∧x<2∧..∧x<99不满足核是0<x∧x<10<x \wedge x<10<x∧x<1,所以我们添加¬C∗\neg C^{*}¬C​∗​​而不是¬C\neg C¬C。
    0  留言 2020-06-30 16:30:18
  • 程序验证(六):纳尔逊-欧朋算法(Nelson-Oppen Procedure)


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

    一、动机截至目前,我们学习了一些一阶理论,每一个都是关于某一种数据类型。然而,现实中的公式并不是由单一的理论组成,如:
    ∀i.0≤i≤n→a[i]≤a[i+1]\forall i.0\le i\le n\to a[i]\le a[i+1]∀i.0≤i≤n→a[i]≤a[i+1]这个公式实际上包含了两个理论:等价与数组。
    我们需要找到一个方法,将复杂的一阶逻辑公式转化为简单的一阶逻辑公式
    二、一些概念2.1 复合理论给定T1T_1T​1​​和T2T_2T​2​​,且Σ1∩Σ2={=}\Sigma_1\cap \Sigma_2 = \lbrace = \rbraceΣ​1​​∩Σ​2​​={=},那么复合理论T1∪T2T_1\cup T_2T​1​​∪T​2​​有:

    符号集:Σ1∪Σ2\Sigma_1 \cup \Sigma_2Σ​1​​∪Σ​2​​
    公理集:A1∪A2A_1 \cup A_2A​1​​∪A​2​​

    纳尔逊-欧朋(Nelson-Oppen)复合方法:T1∪T2T_1\cup T_2T​1​​∪T​2​​是可判定的,如果T1T_1T​1​​与T2T_2T​2​​均满足:

    是量词自由的合取的片段(Quantifier-free, conjunctive fragments)
    可判定的
    稳定无限的(stably-infinite)

    2.2 稳定无限的理论一个建立在符号集Σ\SigmaΣ上的理论TTT是稳定无限的,如果对于每个量词自由的公式FFF,只要FFF是TTT-可满足的,存在一个解释,它的大小(cardinality)是无限的。
    例如这样的一个理论:
    Σ={a,b,=}\Sigma =\{a,b,=\}Σ={a,b,=}公理:∀x.x=a∨x=b\forall x.x=a\vee x=b∀x.x=a∨x=b
    这个理论不是稳定无限的,因为每个解释(D,I)(D,I)(D,I)都有这样的性质:DDD包含至多两个元素,即∣D∣≤2|D|\le 2∣D∣≤2。
    但是大多数我们关心的理论,即TE,TA,TZT_E,T_A,T_ZT​E​​,T​A​​,T​Z​​等等,都是稳定无限的。
    三、纳尔逊-欧朋算法3.1 概况输入:由复合理论T1∪T2T_1\cup T_2T​1​​∪T​2​​得到的公式FFF
    输出:等价的公式F1∧F2F_1\wedge F_2F​1​​∧F​2​​,这里:

    其中F1F_1F​1​​是一个T1T_1T​1​​公式
    其中F2F_2F​2​​是一个T2T_2T​2​​公式

    这个算法的功能:

    将FFF净化为F1F_1F​1​​和F2F_2F​2​​
    将F1F_1F​1​​和F2F_2F​2​​中共享的变量做等价变换

    3.2 步骤1:变量抽象3.2.1 理论目标:FFF中所有的文字或者属于T1T_1T​1​​,或者属于T2T_2T​2​​,但不能是二者共有
    方法:将以下两个转化方法不断使用,直到不能再用为止:

    对于任何一项f(..,t,..)f(.. , t, ..)f(..,t,..),满足f∈Σif\in \Sigma_if∈Σ​i​​且t∉Σit\notin \Sigma_it∉Σ​i​​,将ttt用一个新的(fresh)变量www替换,并在最后合取上t=wt=wt=w
    对于任一谓词p(..,t,..)p(.. ,t, ..)p(..,t,..),满足p∈Σip\in \Sigma_ip∈Σ​i​​且t∉Σit\notin \Sigma_it∉Σ​i​​,将ttt用一个新的(fresh)变量www替换,并在最后合取上t=wt=wt=w
    结束的时候,我们就可以把FFF分为F1F_1F​1​​和F2F_2F​2​​了

    3.2.2 举例考虑TE∪TZT_E\cup T_ZT​E​​∪T​Z​​公式FFF:
    F:1≤x∧x≤2∧f(x)≠f(1)∧f(x)≠f(2)F:1\le x\wedge x\le 2\wedge f(x)\ne f(1)\wedge f(x)\ne f(2)F:1≤x∧x≤2∧f(x)≠f(1)∧f(x)≠f(2)
    在TET_ET​E​​中的非逻辑符是哪些?f,=f,=f,=
    在TZT_ZT​Z​​中的非逻辑符是哪些? 1,2,≤,=1,2,\le,=1,2,≤,=
    净化:用f(w1)f(w_1)f(w​1​​)代替f(1)f(1)f(1),用f(w2)f(w_2)f(w​2​​)代替f(2)f(2)f(2),加入w1=1w_1=1w​1​​=1,w2=2w_2=2w​2​​=2,得到

    1≤x∧x≤2∧f(x)≠f(w1)∧f(x)≠f(w2)∧w1=1∧w2=21\le x\wedge x\le 2\wedge f(x)\ne f(w_1)\wedge f(x)\ne f(w_2)\wedge w_1=1\wedge w_2=21≤x∧x≤2∧f(x)≠f(w​1​​)∧f(x)≠f(w​2​​)∧w​1​​=1∧w​2​​=2
    其中FE:f(x)≠f(w1)∧f(x)≠f(w2)F_E:f(x)\ne f(w_1)\wedge f(x)\ne f(w_2)F​E​​:f(x)≠f(w​1​​)∧f(x)≠f(w​2​​)
    其中FZ:1≤x∧x≤2∧w1=1∧w2=2F_Z:1\le x\wedge x\le 2\wedge w_1 = 1\wedge w_2 = 2F​Z​​:1≤x∧x≤2∧w​1​​=1∧w​2​​=2

    3.3 步骤2:猜测与检查(guess and check)3.3.1 理论给定F1F_1F​1​​与F2F_2F​2​​,定义共享变量集VVV:
    V=free(F1)∩free(F2)V=free(F_1)\cap free(F_2)V=free(F​1​​)∩free(F​2​​)令EEE为VVV上的一个等价关系,由EEE生成的arrangement α(V,E)\alpha (V,E)α(V,E)即为:
    α(V,E):⋀u,v∈V.uEvu=v∧⋀u,v∈V.¬(uEv)u¬v\alpha (V,E): \bigwedge _{u,v\in V.uEv} u=v \wedge\bigwedge _{u,v\in V.\neg (uEv)} u\neg vα(V,E):⋀​u,v∈V.uEv​​u=v∧⋀​u,v∈V.¬(uEv)​​u¬v公式F=F1∧F2F=F_1 \wedge F_2F=F​1​​∧F​2​​是(T1∪T2)(T_1\cup T_2)(T​1​​∪T​2​​)-可满足的当且仅当存在这样的α(V,E)\alpha (V,E)α(V,E)使得:

    其中F1∧α(V,E)F_1\wedge \alpha (V,E)F​1​​∧α(V,E)是T1T_1T​1​​-可满足的
    其中F2∧α(V,E)F_2\wedge \alpha (V,E)F​2​​∧α(V,E)是T2T_2T​2​​-可满足的

    3.3.2 举例考虑之前的净化后的两个公式,共享变量V={w1,w2,x}V= \lbrace w_1,w_2,x \rbraceV={w​1​​,w​2​​,x}。
    猜测并检查VVV上的等价关系:
    {{w1},{w2},{x}}\{\{w_1\},\{w_2\},\{x\}\}{{w​1​​},{w​2​​},{x}}{{w1,w2},{x}}\{\{w_1,w_2\},\{x\}\}{{w​1​​,w​2​​},{x}}{{w1},{w2,x}}\{\{w_1\},\{w_2,x\}\}{{w​1​​},{w​2​​,x}}{{w2},{w1,x}}\{\{w_2\},\{w_1,x\}\}{{w​2​​},{w​1​​,x}}{{w1,w2,x}}\{\{w_1,w_2,x\}\}{{w​1​​,w​2​​,x}}3.3.3 效率问题这个guess and check的时间复杂度是指数级的,所以不太实用,所以我们换个方法。
    3.4 步骤3:等价推导(equality propagation)3.4.1 凸理论(convex theory)一个理论是凸的(convex),如果它对于每个变量自由的公式FFF,都满足:

    F⇒⋁i=1nui=viF\Rightarrow \bigvee ^n_{i=1} u_i =v_iF⇒⋁​i=1​n​​u​i​​=v​i​​则
    F⇒ui=vi for some i∈{1,..,n}F\Rightarrow u_i = v_i~for~some~i\in\{1,.. , n\}F⇒u​i​​=v​i​​ for some i∈{1,..,n}其中TZ,TAT_Z, T_AT​Z​​,T​A​​不是凸的,但是TE,TQT_E,T_QT​E​​,T​Q​​是凸的。
    举例:TZT_ZT​Z​​不是凸的
    例如,考虑这样的量词自由的合取ΣZ\Sigma_ZΣ​Z​​ -公式
    F:1≤z∧z≤2∧u=1∧v=2F: 1\le z\wedge z\le 2\wedge u=1\wedge v=2F:1≤z∧z≤2∧u=1∧v=2那么
    F⇒z=u∨z=vF\Rightarrow z=u\vee z=vF⇒z=u∨z=v但是无法推出
    F⇒z=uF\Rightarrow z=uF⇒z=u或
    F⇒z=vF\Rightarrow z=vF⇒z=v3.4.2 等价推导给定F1F_1F​1​​与F2F_2F​2​​

    让Ti(i=1,2)T_i (i=1,2)T​i​​(i=1,2)报告任何有关共享变量(包括u,vu, vu,v)的新推出的等价关系

    如果TiT_iT​i​​是凸的,令u=vu=vu=v为新推出的等价关系
    如果TiT_iT​i​​不是凸的,令⋁i(ui=vi)\bigvee_i (u_i = v_i)⋁​i​​(u​i​​=v​i​​)为推出的等价关系的析取

    将新推出的等价关系存储到EEE中(EEE是已经发现的等价关系的集合)

    如果TiT_iT​i​​是凸的,将u=vu=vu=v添加到EEE
    如果TiT_iT​i​​不是凸的,将搜索过程依据不同的析取⋁i(ui=vi)\bigvee_i(u_i = v_i)⋁​i​​(u​i​​=v​i​​) 分成不同的分支(通过在EEE中添加相应的等价关系)

    对于每一个分支,将EEE传播到另一个判定程序(也就是递归进行),重复以上步骤

    算法返回:

    satsatsat如果任一分支得到一个完整的arrangement
    unsatunsatunsat如果所有的分支都推出矛盾
    satsatsat如果所有的分支都不能发现新的等价关系

    3.4.3 举例考虑ΣE∪ΣQ\Sigma_E\cup \Sigma_QΣ​E​​∪Σ​Q​​-公式:
    F:f(f(x)−f(y))≠f(z)∧x≤y∧y+z≤x∧0≤zF:f(f(x)-f(y))\ne f(z)\wedge x\le y\wedge y+z\le x\wedge 0\le zF:f(f(x)−f(y))≠f(z)∧x≤y∧y+z≤x∧0≤z在第一步后,FFF被分为两个公式:
    FE:f(w)≠f(z)∧u=f(x)∧v=f(y)F_E:f(w)\ne f(z)\wedge u=f(x)\wedge v=f(y)F​E​​:f(w)≠f(z)∧u=f(x)∧v=f(y)FQ:x≤y∧y+z≤x∧0≤z∧w=u−vF_Q:x\le y\wedge y+z\le x\wedge 0\le z\wedge w=u-vF​Q​​:x≤y∧y+z≤x∧0≤z∧w=u−vV=shared(FE,FQ)={x,y,z,u,v,w}V=shared(F_E,F_Q)=\{x,y,z,u,v,w\}V=shared(F​E​​,F​Q​​)={x,y,z,u,v,w}注意,TET_ET​E​​与TQT_{Q}T​Q​​都是凸理论。
    于是

    考虑TE∪TZT_E\cup T_{Z}T​E​​∪T​Z​​-公式FFF:
    F:1≤x∧x≤2∧f(x)≠f(1)∧f(x)≠f(2)F:1\le x\wedge x\le 2\wedge f(x)\ne f(1)\wedge f(x)\ne f(2)F:1≤x∧x≤2∧f(x)≠f(1)∧f(x)≠f(2)在第一步后,FFF被分为两个公式:
    FE:f(x)≠f(w1)∧f(x)≠f(w2)F_E:f(x)\ne f(w_1)\wedge f(x)\ne f(w_2)F​E​​:f(x)≠f(w​1​​)∧f(x)≠f(w​2​​)FZ:1≤x∧x≤2∧w1=1∧w2=2F_{Z} :1\le x\wedge x\le 2\wedge w_1=1\wedge w_2=2F​Z​​:1≤x∧x≤2∧w​1​​=1∧w​2​​=2V=shared(FE,FZ)={w1,w2,x}V=shared(F_E,F_{Z})=\{w_1,w_2,x\}V=shared(F​E​​,F​Z​​)={w​1​​,w​2​​,x}注意,TET_ET​E​​是凸的,TZT_{Z}T​Z​​不是。
    于是

    考虑TE∪TZT_E\cup T_{Z}T​E​​∪T​Z​​-公式FFF:
    F:1≤x∧x≤3∧f(x)≠f(1)∧f(x)≠f(3)∧f(1)≠f(2)F: 1\le x\wedge x\le 3\wedge f(x)\ne f(1)\wedge f(x)\ne f(3)\wedge f(1)\ne f(2)F:1≤x∧x≤3∧f(x)≠f(1)∧f(x)≠f(3)∧f(1)≠f(2)在第一步后,FFF被分为两个公式:
    FE:f(x)≠f(w1)∧f(x)≠f(w3)∧f(w1)≠f(w2)F_E:f(x)\ne f(w_1)\wedge f(x)\ne f(w_3)\wedge f(w_1)\ne f(w_2)F​E​​:f(x)≠f(w​1​​)∧f(x)≠f(w​3​​)∧f(w​1​​)≠f(w​2​​)FZ:1≤x∧x≤3∧w1=1∧w2=2∧w3=3F_{Z}:1\le x\wedge x\le 3\wedge w_1=1\wedge w_2=2\wedge w_3=3F​Z​​:1≤x∧x≤3∧w​1​​=1∧w​2​​=2∧w​3​​=3V=shared(FE,FZ)={w1,w2,w3,x}V=shared(F_E,F_{Z})=\{w_1,w_2,w_3,x\}V=shared(F​E​​,F​Z​​)={w​1​​,w​2​​,w​3​​,x}注意,TET_ET​E​​是凸的,TZT_{Z}T​Z​​不是。
    于是
    0  留言 2020-06-30 13:27:01
  • 程序验证(五):一阶理论的过程


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

    主要讨论TET_ET​E​​的量词自由片段以及TAT_AT​A​​
    一、等价理论的判定1.1 等价及未解释函数理论(Theory of Equality and Uninterpreted Functions)除=外的谓词实际上使我们的讨论不必要地复杂化,去除这些累赘谓词的方法如下:

    对每个谓词ppp,引入一个新的(fresh)函数符号fpf_pf​p​​
    引入一个新的常量∙\bullet∙
    将每个谓词实例p(t1,..,tn)p(t_1 ,.., t_n)p(t​1​​,..,t​n​​)替换为fp(t1,..,tn)=∙f_p(t_1 ,.., t_n)=\bulletf​p​​(t​1​​,..,t​n​​)=∙,这样就得到了等价及未解释函数理论(EUF):

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

    转化方法举例:
    x=y→(p(x)↔p(y))x=y\to (p(x)\leftrightarrow p(y))x=y→(p(x)↔p(y))
    转化为:
    x=y→((fp(x)=∙)↔(fp(y)=∙))x=y\to ((f_p (x)=\bullet)\leftrightarrow (f_p (y)=\bullet))x=y→((f​p​​(x)=∙)↔(f​p​​(y)=∙))
    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)p(x)∧q(x,y)∧q(y,z)→¬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(f​p​​(x)=∙∧f​q​​(x,y)=∙∧f​q​​(y,z)=∙)→f​q​​(x,z)≠∙
    1.2 一些概念1.2.1 关系(relation)给定SSS上的二元关系RRR,∀s1,s2∈S\forall s_1,s_2\in S∀s​1​​,s​2​​∈S,或者s1Rs2s_1Rs_2s​1​​Rs​2​​或者¬(s1Rs2)\neg (s_1Rs_2)¬(s​1​​Rs​2​​)。
    一个二元关系RRR若满足以下三个性质,即为一个等价关系(equivalence relation):

    自反性:∀x∈S.sRs\forall x\in S.sRs∀x∈S.sRs
    对称性:∀s1,s2∈S.s1Rs2→s2Rs1\forall s_1,s_2\in S.s_1Rs_2\to s_2Rs_1∀s​1​​,s​2​​∈S.s​1​​Rs​2​​→s​2​​Rs​1​​
    传递性:∀s1,s2,s3∈S.s1Rs2∧s2Rs3→s1Rs3\forall s_1,s_2,s_3\in S.s_1Rs_2 \wedge s_2Rs_3 \to s_1Rs_3∀s​1​​,s​2​​,s​3​​∈S.s​1​​Rs​2​​∧s​2​​Rs​3​​→s​1​​Rs​3​​

    一个二元关系RRR是同余关系(congruence relation),如果它除以上三个性质外,还满足函数同余性:
    ∀s,t∈Sn.(⋀i=1nsiRti)→f(s)Rf(t)\forall s,t \in S^n .(\bigwedge ^n_{i=1} s_iRt_i)\to f(s)Rf(t)∀s,t∈S​n​​.(⋀​i=1​n​​s​i​​Rt​i​​)→f(s)Rf(t)1.2.2 类(class)令RRR为SSS上的一个等价关系,则s∈Ss\in Ss∈S在RRR下的等价类(equivalence class)为:
    [s]R≡{s′∈S:sRs′}[s] _R \equiv \{s'\in S:sRs'\}[s]​R​​≡{s​′​​∈S:sRs​′​​}SSS中的每个元素都属于RRR的一个等价类。如果RRR是同余关系,那么[s]R[s]_R[s]​R​​ 是sss的同余类。
    举例:Consider the relation ≡2\equiv _2≡​2​​ over ZZZ, where a≡2ba\equiv _2 ba≡​2​​b iff (a mod 2)=(b mod 2)(a \space mod \space 2)=(b \space mod \space 2)(a mod 2)=(b mod 2). The equivalence class of 4 under ≡2\equiv_2≡​2​​ is:
    [4]≡2={n∈Z:(nmod2)=0}={n∈Z:n is even}[4]_{\equiv_2} = \{n\in Z: (n mod 2)=0\}=\{n\in Z : n~is~even\}[4]​≡​2​​​​={n∈Z:(nmod2)=0}={n∈Z:n is even}1.2.3 分割(partition)SSS的一个分割PPP是一个SSS的子集的集合,满足:

    total:(⋃S′∈PS′)=S(\bigcup _{S^{\prime} \in P} S^{\prime} )=S(⋃​S​′​​∈P​​S​′​​)=S
    disjoint:∀S1,S2∈P.S1≠S2→S1∩S2=∅\forall S_1, S_2 \in P.S_1\ne S_2\to S_1 \cap S_2 = \varnothing∀S​1​​,S​2​​∈P.S​1​​≠S​2​​→S​1​​∩S​2​​=∅

    等价关系RRR 产生了SSS的一个分割,叫做SSS除以RRR的商,也就是:
    S/R={[s]R:s∈S}S/R = \{[s]_R : s\in S\}S/R={[s]​R​​:s∈S}例如,商Z/≡2Z /\equiv_2Z/≡​2​​即为这个分割:
    {{n∈Z: n is odd},{n∈Z: n is even}}\{\{n\in Z :~n~is~odd\},\{n\in Z:~n~is~even\}\}{{n∈Z: n is odd},{n∈Z: n is even}}1.2.4 关系的精化(refinement)给定SSS上两个关系R1R_1R​1​​和R2R_2R​2​​,我们说R1R_1R​1​​精化了R2R_2R​2​​,写作R1≺R2R_1 \prec R_2R​1​​≺R​2​​,如果满足条件:
    ∀s1,s2∈S.s1R1s2→s1R2s2\forall s_1, s_2\in S.s_1R_1s_2 \to s_1R_2s_2∀s​1​​,s​2​​∈S.s​1​​R​1​​s​2​​→s​1​​R​2​​s​2​​我们可以把二元关系RRR视为一个对(pair)的集合R^\hat{R}​R​^​​,也就是:
    ∀s1,s2∈S, 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}∀s​1​​,s​2​​∈S, if s​1​​Rs​2​​, then (s​1​​,s​2​​)∈​R​^​​于是我们知道R1≺R2R_1 \prec R_2R​1​​≺R​2​​当且仅当R^1⊆R^2\hat{R}_1 \subseteq \hat{R}_2​R​^​​​1​​⊆​R​^​​​2​​。
    举例:
    R1:{sR1s:s∈S}R_1:\{sR_1s:s\in S\}R​1​​:{sR​1​​s:s∈S}R2:{s1R2s2:s1,s2∈S}R_2:\{s_1R_2s_2:s_1,s_2\in S\}R​2​​:{s​1​​R​2​​s​2​​:s​1​​,s​2​​∈S}那么
    R1≺R2R_1 \prec R_2R​1​​≺R​2​​1.2.5 等价闭包(equivalence closure)一个SSS上的关系RRR的等价闭包RER^ER​E​​是这样的一个等价关系,满足:

    其中RRR精化RER^ER​E​​:R≺RER\prec R^ER≺R​E​​
    对于其他满足R≺R′R\prec R^{\prime}R≺R​′​​的等价关系R′R^{\prime}R​′​​,或者R′=RER^{\prime}=R^ER​′​​=R​E​​或者RE≺R′R^E \prec R^{\prime}R​E​​≺R​′​​ 。也就是说,RER^ER​E​​是包含RRR的最小的等价关系。

    与之相似,RRR的同余闭包(congruence closure)RCR^CR​C​​是包含RRR的最小同余关系。
    等价闭包的构造的一个例子:
    有一个论域S={a,b,c,d}S=\lbrace a,b,c,d \rbraceS={a,b,c,d},一个关系RRR满足:
    aRb,bRc,dRdaRb,bRc,dRdaRb,bRc,dRd为了构造RER^ER​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)\}R​E​​={(a,b),(b,a),(a,a),(b,b),(b,c),(c,a),(c,b),(c,c),(d,d)}1.3 等价理论的判定TET_ET​E​​的量词自由片段是可判定的
    1.3.1 核心逻辑给定一个TET_ET​E​​-公式FFF:
    F:(s1=t1)∧..∧(sm=tm)∧(sm+1≠tm+1)∧..∧(sn≠tn)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)F:(s​1​​=t​1​​)∧..∧(s​m​​=t​m​​)∧(s​m+1​​≠t​m+1​​)∧..∧(s​n​​≠t​n​​)FFF是TET_ET​E​​-可满足的,当且仅当存在一个同余关系∼\sim∼,使得:

    对每个i∈{1,..,m}i\in \lbrace 1,.. ,m \rbracei∈{1,..,m}, si∼tis_i \sim t_is​i​​∼t​i​​
    对每个i∈{m+1,..,n}i\in \lbrace m+1,.. ,n \rbracei∈{m+1,..,n}, si∼tis_i \sim t_is​i​​∼t​i​​

    这样一个同余关系定义了FFF的TET_ET​E​​-解释(D,I)(D,I)(D,I):

    其中DDD由∼\sim∼的同余类构成
    其中IIII将DDD的元素赋值给FFF的子项(subterm)来满足∼\sim∼
    其中III赋值了=,一个与∼\sim∼相似的关系

    我们把(D,I)⊨F(D,I)\models F(D,I)⊨F简记为∼⊨F\sim \models F∼⊨F。
    1.3.2 同余闭包算法令SFS_FS​F​​为FFF的子项,∼\sim∼是SFS_FS​F​​上的关系,那么该算法如下:

    在子项集合SFS_FS​F​​上构造{s1=t1,..,s+m=tm}\lbrace s_1=t_1,.. ,s+m=t_m \rbrace{s​1​​=t​1​​,..,s+m=t​m​​}的同余闭包~
    如果对于任何i∈{m+1,..,n}i\in \lbrace m+1,.. ,n \rbracei∈{m+1,..,n},si∼tis_i \sim t_is​i​​∼t​i​​,那么返回unsatunsatunsat
    否则,返回satsatsat

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

    从“最好”的同余关系开始∼0={{s}:s∈SF}\sim 0 = \lbrace \lbrace s \rbrace :s\in S_F \rbrace∼0={{s}:s∈S​F​​},这里SFS_FS​F​​每个子项都在它本身构成的同余类里
    对于每个i∈{1,..,m}i\in \lbrace 1,.. , m \rbracei∈{1,..,m},通过把si=tis_i = t_is​i​​=t​i​​加入∼i−1\sim _{i-1}∼​i−1​​构造∼i\sim _i∼​i​​

    将同余类[si]∼i−1[s_i]_{\sim _{i-1}}[s​i​​]​∼​i−1​​​​和[ti]∼i−1[t_i]_{\sim _{i-1}}[t​i​​]​∼​i−1​​​​merge起来
    将任何通过以上步骤产生的新的同余关系传递下去


    举例:判断以下公式的可满足性
    F:f(a,b)=a∧f(f(a,b),b)≠aF: f(a,b) = a\wedge f(f(a,b),b)\ne aF:f(a,b)=a∧f(f(a,b),b)≠a建立子项集合SFS_FS​F​​:
    SF={a,b,f(a,b),f(f(a,b),b)}S_F = \{a,b,f(a,b),f(f(a,b),b)\}S​F​​={a,b,f(a,b),f(f(a,b),b)}构造SFS_FS​F​​上的“最好”的闭包关系:
    {{a},{b},{f(a,b)},{f(f(a,b),b)}}\{\{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 \rbracei∈{1,..,m},将同余类[si]∼i−1[s_i]_{\sim _{i-1}}[s​i​​]​∼​i−1​​​​和[ti]∼i−1[t_i]_{\sim_{i-1}}[t​i​​]​∼​i−1​​​​merge起来,这里由f(a,b)=af(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)\}\}{{a,f(a,b)},{b},{f(f(a,b),b)}}每次merge之后,使用公理以推进,由f(a,b)∼a,b∼bf(a,b)\sim a,b\sim bf(a,b)∼a,b∼b,有f(f(a,b),b)∼f(a,b)f(f(a,b),b)\sim f(a,b)f(f(a,b),b)∼f(a,b),从而:
    {{a,f(a,b),f(f(a,b),b)},{b}}\{\{a,f(a,b),f(f(a,b),b)\},\{b\}\}{{a,f(a,b),f(f(a,b),b)},{b}}这也就是SFS_FS​F​​的同余闭包。
    FFF是TET_ET​E​​-不可满足的,因为f(f(a,b),b)∼af(f(a,b),b)\sim af(f(a,b),b)∼a而FFF声称f(f(a,b),b)≠af(f(a,b),b)\ne af(f(a,b),b)≠a。
    判断以下公式的可满足性:
    F:f(f(f(a)))=a∧f(f(f(f(f(a)))))=a∧f(a)≠aF:f(f(f(a)))=a\wedge f(f(f(f(f(a)))))=a\wedge f(a)\ne aF:f(f(f(a)))=a∧f(f(f(f(f(a)))))=a∧f(a)≠a建立子项集合SFS_FS​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)\}S​F​​={a,f(a),f​2​​(a),f​3​​(a),f​4​​(a),f​5​​(a)}构造SFS_FS​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)\}\}{{a},{f(a)},{f​2​​(a)},{f​3​​(a)},{f​4​​(a)},{f​5​​(a)}}由f3(a)=af^3(a) = af​3​​(a)=a,合并{f3(a)}\lbrace f^3(a) \rbrace{f​3​​(a)}和{a}\lbrace a \rbrace{a}:
    {{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)\}\}{{a,f​3​​(a)},{f(a)},{f​2​​(a)},{f​4​​(a)},{f​5​​(a)}}由f3(a)∼af^3(a)\sim af​3​​(a)∼a,推导出f4(a)∼f(a)f^4(a)\sim f(a)f​4​​(a)∼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)\}\}{{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)f​4​​(a)∼f(a),推导出f5(a)∼f2(a)f^5(a)\sim f^2(a)f​5​​(a)∼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)\}\}{{a,f​3​​(a)},{f(a),f​4​​(a)},{f​2​​(a),f​5​​(a)}}由f5(a)=af^5(a)=af​5​​(a)=a,合并{f2(a),f5(a)}\lbrace f^2(a),f^5(a) \rbrace{f​2​​(a),f​5​​(a)}:
    {{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)\}\}{{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)f​3​​(a)∼f​2​​(a),推导出f4(a)∼f3(a)f^4(a)\sim f^3(a)f​4​​(a)∼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)\}\}{{a,f(a),f​2​​(a),f​3​​(a),f​4​​(a),f​5​​(a)}}这就是SFS_FS​F​​的同余闭包。
    由FFF声称f(a)≠af(a)\ne af(a)≠a,而f(a)∼af(a)\sim af(a)∼a,所以unsatunsatunsat。
    实现同余闭包算法的底层算法:并查集
    1.3.3 性质
    可靠性与完备性:如果同余闭包算法返回satsatsat那么量词自由的FFF就是TE−satT_E-satT​E​​−sat的
    复杂度:O(e2)O(e^2)O(e​2​​)(参见并查集算法)

    二、数组的判定理论2.1 核心逻辑将TAT_AT​A​​可满足性判定归约为TET_ET​E​​可满足性判定。
    如果一个ΣZ\Sigma_ZΣ​Z​​-公式FFF不包含任何写项:

    将每个数组变量aaa与一个新的(fresh)函数符号faf_af​a​​关联起来
    将每个读项a[i]a[i]a[i]替换为fa(i)f_a(i)f​a​​(i)判断并返回得到的公式的TET_ET​E​​可满足性;否则,取一个项a⟨i◃v⟩[j]a\langle i\triangleleft v\rangle [j]a⟨i◃v⟩[j],并分为两种情况:

    将F[a⟨i◃v⟩[j]]F[a\langle i\triangleleft v\rangle [j]]F[a⟨i◃v⟩[j]]替换为F1:F[v]∧i=jF_1:F[v]\wedge i=jF​1​​:F[v]∧i=j
    将F[a⟨i◃v⟩[j]]F[a\langle i\triangleleft v\rangle [j]]F[a⟨i◃v⟩[j]]替换为F2:F[a[j]]∧i≠jF_2:F[a[j]]\wedge i\ne jF​2​​:F[a[j]]∧i≠j

    递归地对F1F_1F​1​​于F2F_2F​2​​做以上处理。只要有一个分支是satsatsat,那么返回satsatsat
    否则,返回unsatunsatunsat

    举例:判断以下公式的可满足性
    F:i1=j∧i1≠i2∧a[j]=v1∧a⟨i1◃v1⟩⟨i2◃v2⟩[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]F:i​1​​=j∧i​1​​≠i​2​​∧a[j]=v​1​​∧a⟨i​1​​◃v​1​​⟩⟨i​2​​◃v​2​​⟩[j]≠a[j]由FFF本身知,i2≠ji_2 \ne ji​2​​≠j:
    F2:i1=j∧i1≠i2∧a[j]=v1∧a⟨i1◃v1⟩[j]≠a[j]∧i2≠jF_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 jF​2​​:i​1​​=j∧i​1​​≠i​2​​∧a[j]=v​1​​∧a⟨i​1​​◃v​1​​⟩[j]≠a[j]∧i​2​​≠j其中有一个写项,所以分为两种情况:
    F3:i1=j∧i1≠i2∧a[j]=v1∧v1≠a[j]∧i2≠j∧i1=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 =jF​3​​:i​1​​=j∧i​1​​≠i​2​​∧a[j]=v​1​​∧v​1​​≠a[j]∧i​2​​≠j∧i​1​​=jF4:i1=j∧i1≠i2∧a[j]=v1∧a[j]≠a[j]∧i2≠j∧i1≠jF_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 jF​4​​:i​1​​=j∧i​1​​≠i​2​​∧a[j]=v​1​​∧a[j]≠a[j]∧i​2​​≠j∧i​1​​≠j二者都是不可满足的。
    所有的分支都是unsatunsatunsat,所以得出结论:FFF是TAT_AT​A​​-不可满足的。
    2.2 性质
    可靠性与完备性:给定一个ΣA\Sigma_AΣ​A​​公式FFF,以上判定算法返回satsatsat当且仅当FFF是TAT_AT​A​​-可满足的,否则,它返回unsatunsatunsat
    复杂度:这是一个NP完全问题
    0  留言 2020-06-30 11:37:13
  • 程序验证(四):一阶理论


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

    注意:原文中有部分公式书写错误,本文转载的时候,修正了这部分错误!
    一、定义一个一阶理论(theory)TTT被以下两点定义:

    它的符号集Σ\SigmaΣ, 一个非逻辑符号的集合
    它的公理AAA, 一个在Σ\SigmaΣ上的闭公式(closed formula)

    一阶逻辑理论定义了一个有限的词汇表以讨论所关注的主题,而理论中的公理定义了所意指的涵义(intended meaning)。
    Σ−formula\Sigma-formulaΣ−formula:一个Σ−formula\Sigma-formulaΣ−formula只包含Σ\SigmaΣ中的非逻辑符号,以及逻辑变元,逻辑连接词和量词。
    举例:
    ∀x,y.x=y→y=x\forall x,y.x=y\to y=x∀x,y.x=y→y=x
    a[i]=e→a⟨i◃e⟩=aa[i] = e\to a \langle i \triangleleft e\rangle = aa[i]=e→a⟨i◃e⟩=a
    二、常用理论(theory)2.1 等价理论(Theory of Equality)2.1.1 定义等价理论TET_ET​E​​由以下符号集给出:
    ΣE:{=,a,b,c,...,f,g,h,...,p,q,r,...}\Sigma_E: \{=,a,b,c, ... ,f,g,h, ... ,p,q,r, ...\}Σ​E​​:{=,a,b,c,...,f,g,h,...,p,q,r,...}这里有二元等价符号 =,以及其他的常量、函数、谓词符号。TET_ET​E​​的公理 “=” 满足自反性、对称性、传递性,以及函数与谓词的同余性(congruence)。
    TET_ET​E​​公式举例:

    ∀x,y.x=y→y=x\forall x,y.x=y\to y=x∀x,y.x=y→y=x
    a=b∧b=c→g(f(a),b)=g(f(c),a)a=b\wedge b=c\to g(f(a),b) = g(f(c),a)a=b∧b=c→g(f(a),b)=g(f(c),a)

    符号集:
    ΣE:{=,a,b,c,...,f,g,h,...,p,q,r,...}\Sigma_E : \{=,a,b,c, ... ,f,g,h, ... ,p,q,r, ...\}Σ​E​​:{=,a,b,c,...,f,g,h,...,p,q,r,...}公理集:

    自反性(refelxivity):∀x.x=x\forall x.x=x∀x.x=x
    对称性(symmetry):∀x,y.x=y→y=x\forall x,y.x=y \to y=x∀x,y.x=y→y=x
    传递性(transitivity):∀x,y,z.x=y∧y=z→x=z\forall x,y,z.x=y\wedge y=z \to x=z∀x,y,z.x=y∧y=z→x=z
    函数同余性(function congruence):∀x,y.(⋀i=1nxi=yi)→f(x)=f(y)\forall x,y.(\bigwedge ^n_{i=1} x_i=y_i)\to f(x) = f(y)∀x,y.(⋀​i=1​n​​x​i​​=y​i​​)→f(x)=f(y)
    谓词同余性(predicate congruence):谓词同余性(predicate congruence):∀x,y.(⋀i=1nxi=yi)→(p(x)↔p(y))\forall x,y.(\bigwedge ^n_{i=1} x_i = y_i)\to (p(x) \leftrightarrow p(y))∀x,y.(⋀​i=1​n​​x​i​​=y​i​​)→(p(x)↔p(y))

    注意,以上公理并不是标准的公理,实际上,它只是一个模式(schema)因为表达式中的fff或ppp可以代表任何函数(或谓词)。
    2.1.2 性质TET_ET​E​​是可判定的吗?(不是)
    证明方法:将TET_ET​E​​公式转化为一阶逻辑公式:

    TET_ET​E​​仍然允许所有常量、函数以及谓词符号存在
    可以将任何一阶逻辑公式FFF编码为TET_ET​E​​公式F′F^{\prime}F​′​​

    将FFF中所有 = 符号用一个新的(fresh)谓词符号替换
    F′F^{\prime}F​′​​中不出现 = 符号
    TET_ET​E​​中的公理与此无关


    然而,TET_ET​E​​的量词自由片段(quantifier-free fragment)是可判定的。
    2.1.3 理论的片段(theory fragment)一个理论的片段(fragment)是TTT中公式的一个由语义约束的(syntactically-restricted)子集,如果对于每个符合片段的语义约束的公式FFF,T⊨FT\models FT⊨F是可判定的,那么这个片段是可判定的量词自由的片段:TTT中没有量词的永真公式(也可以看做是所有量词都是全称量词)。
    2.1.4 永真性的证明使用一阶逻辑中的语义分析方法,同时假如TET_ET​E​​的公理。
    举例:证明以下公式的永真性
    F:x=y∧y=z→g(f(x),y)=g(f(z),x)F: x=y\wedge y=z \to g(f(x),y) = g(f(z), x)F:x=y∧y=z→g(f(x),y)=g(f(z),x)

    2.2 佩亚诺算术(Peano Arithmetic)2.2.1 定义符号集:
    ΣPA:{0,1,+,×,=}\Sigma_{PA} : \{0,1,+,\times , =\}Σ​PA​​:{0,1,+,×,=}
    0与1是常量
    +与×\times×是二元函数
    =是二元谓词
    没有其他符号

    公理集:

    所有的等价公理:自反性、对称性、传递性、以及同余性
    Zero: ∀x.¬(x+1=0)Zero: \space \forall x.\neg(x+1=0)Zero: ∀x.¬(x+1=0)
    Successor: ∀x,y.(x+1=y+1)→x=ySuccessor: \space \forall x,y.(x+1=y+1)\to x=ySuccessor: ∀x,y.(x+1=y+1)→x=y
    Plus zero: ∀x.x+0=xPlus \space zero: \space \forall x.x+0=xPlus zero: ∀x.x+0=x
    Plus successor: ∀x,y.x+(y+1)=(x+y)+1Plus \space successor: \space \forall x,y.x+(y+1)=(x+y)+1Plus successor: ∀x,y.x+(y+1)=(x+y)+1
    Times zero: ∀x.x×0=0Times \space zero: \space \forall x.x\times 0=0Times zero: ∀x.x×0=0
    Times successor: ∀x,y.x×(y+1)=x×y+xTimes \space successor: \space \forall x,y.x\times (y+1)=x\times y+xTimes successor: ∀x,y.x×(y+1)=x×y+x

    为了方便,以后我们把x×yx\times yx×y记作xyxyxy。
    数学归纳法:
    一个模板:
    (F(0)∧(∀x.F[x]→f[x+1]))→∀x.F[x](F(0)\wedge (\forall x.F[x]\to f[x+1]))\to \forall x.F[x](F(0)∧(∀x.F[x]→f[x+1]))→∀x.F[x]
    这里FFF代表任意的TPAT_{PA}T​PA​​公式,这就是数学归纳法在佩亚诺算术下的表达。
    2.2.2 一种佩亚诺算术因为算术中的函数与谓词符号可以有多种解释,所以这里说是“一种”。
    最常见的:

    Domain:NNN
    I[0],I[1]:0N,1N∈NI[0],I[1]: 0_{N}, 1_{N} \in NI[0],I[1]:0​N​​,1​N​​∈N
    I[+]:+N, addition over NI[+]: +_{N}, \space addition \space over \space NI[+]:+​N​​, addition over N
    I[×]:×N, multiplication over NI[\times]:\times _{N}, \space multiplication \space over \space NI[×]:×​N​​, multiplication over N
    I[=]:=N, equality over NI[=]:=_{N}, \space equality \space over \space NI[=]:=​N​​, equality over N

    2.2.3 语法糖在TPAT_{PA}T​PA​​中如何写3x+5=2y3x+5=2y3x+5=2y?
    (1+1+1)×x+1+1+1+1+1=(1+1)×y(1+1+1)\times x +1+1+1+1+1=(1+1)\times y(1+1+1)×x+1+1+1+1+1=(1+1)×y如何表达x>5x>5x>5?
    ∃y.¬(y=0)∧x=5+y\exists y.\neg (y=0)\wedge x = 5+y∃y.¬(y=0)∧x=5+y如何表达x+1≤yx+1\le yx+1≤y
    ∃z.x+1+z=y\exists z.x+1+z = y∃z.x+1+z=y2.2.4 性质TPAT_{PA}T​PA​​中的可满足性与永真性是不可判定的,甚至量词自由的TPAT_{PA}T​PA​​也是不可判定的。
    另外,TPAT_{PA}T​PA​​是不完备的。
    总结:很多永真的数学命题在TPA T_{PA}T​PA​​上是非永真的,原因是由于乘法过于复杂。
    2.3 Presburger算术2.3.1 定义符号集:
    ΣN:{0,1,+,=}\Sigma_{N}:\{0,1,+,=\}Σ​N​​:{0,1,+,=}公理集:

    所有的等价公理:自反性、对称性、传递性、同余性
    Zero: ∀x.¬(x+1=0)Zero:\space \forall x.\neg (x+1=0)Zero: ∀x.¬(x+1=0)


    Successor: ∀x,y.(x+1=y+1)→x=ySuccessor: \space \forall x,y.(x+1=y+1)\to x=ySuccessor: ∀x,y.(x+1=y+1)→x=y
    Plus zero: ∀x.x+0=xPlus \space zero: \space \forall x.x+0=xPlus zero: ∀x.x+0=x
    Plus successor: ∀x,y.x+(y+1)=(x+y)+1Plus \space successor: \space \forall x,y.x+(y+1)=(x+y)+1Plus successor: ∀x,y.x+(y+1)=(x+y)+1
    Induction: (F[0]∧(∀x.F[x]→F[x+1]))→∀x.F[x]Induction: \space (F[0]\wedge (\forall x.F[x]\to F[x+1]))\to \forall x.F[x]Induction: (F[0]∧(∀x.F[x]→F[x+1]))→∀x.F[x]

    2.3.2 性质常用的解释与佩亚诺算术一样,但是,它有很好的性质:

    永真性可判定,但是很困难:复杂度O(22n)O(2^{2^n})O(2​2​n​​​​)
    完备性:对于任一TNT_{N}T​N​​上的公式FFF,或者⊨F\models F⊨F或者⊨¬F\models \neg F⊨¬F
    可以量词消除:对于任一TNT_{N}T​N​​上的公式FFF,存在一个等价的量词自由的F′F^{\prime}F​′​​量词自由的片段的可判定性是coNP-complete的

    2.3.3 技巧:如何证明整数考虑这样一个公式:
    F0:∀w,x.∃y,z.x+2y−z−13>−2w+5F_0:\forall w,x.\exists y,z.x+2y-z-13 > -2w+5F​0​​:∀w,x.∃y,z.x+2y−z−13>−2w+5这里的 - 被解释为标准减法,w,x,y,zw,x,y,zw,x,y,z的范围为整数集ZZZ。
    为了表示TNT_NT​N​​中的公式,为F0F_0F​0​​中每个变量vvv都引入两个变量vpv_pv​p​​和vnv_nv​n​​:
    F1:∀wp,wn,xp,xn.∃yp,yn,zp,zn.(xp−xn)+2(yp−yn)−(zp−zn)−13>−3(wp−wn)+5F_1: \forall w_p ,w_n ,x_p ,x_n.\exists y_p ,y_n ,z_p ,z_n.(x_p-x_n)+2(y_p-y_n)-(z_p-z_n)-13 > -3(w_p-w_n)+5F​1​​:∀w​p​​,w​n​​,x​p​​,x​n​​.∃y​p​​,y​n​​,z​p​​,z​n​​.(x​p​​−x​n​​)+2(y​p​​−y​n​​)−(z​p​​−z​n​​)−13>−3(w​p​​−w​n​​)+5“移项”(因为TNT_NT​N​​中没有减号),得到最终形式:
    F2:∀wp,wn,xp,xn.∃yp,yn,zp,zn.∃u.¬(u=0)∧xp+yp+yp+zn+wp+wp+wp=xn+yn+yn+zp+wn+wn+wn+u+1+1+...+1F_2: \forall w_p ,w_n ,x_p ,x_n. \exists y_p ,y_n ,z_p ,z_n. \exists u. \neg(u=0)\wedge x_p +y_p +y_p +z_n+w_p+w_p+w_p = x_n +y_n +y_n +z_p + w_n +w_n +w_n + u +1+1+...+1F​2​​:∀w​p​​,w​n​​,x​p​​,x​n​​.∃y​p​​,y​n​​,z​p​​,z​n​​.∃u.¬(u=0)∧x​p​​+y​p​​+y​p​​+z​n​​+w​p​​+w​p​​+w​p​​=x​n​​+y​n​​+y​n​​+z​p​​+w​n​​+w​n​​+w​n​​+u+1+1+...+1(一共13个+1)
    2.4 线性整数算术2.4.1 定义符号集:
    ΣZ:{...,−2,−1,0,1,2,...,−3×,−2×,2×,3×,...,+,−,=,>}\Sigma_{Z}: \{...,-2,-1,0,1,2, ... ,-3\times ,-2\times ,2\times ,3\times ,...,+,-,=,>\}Σ​Z​​:{...,−2,−1,0,1,2,...,−3×,−2×,2×,3×,...,+,−,=,>}
    -2,-1,0,1,2,…,+,-,=,>就是通常情况下的涵义
    −3×\times×, -2×\times×, 2×\times×, 3×\times×都是常系数的一元乘法函数

    论断:TZT_{Z}T​Z​​可以归约(reduce)为TNT_{N}T​N​​。

    它们的表达能力相同
    TZT_{Z}T​Z​​更加方便,所以比TNT_{N}T​N​​更加常用

    举例:证明以下公式的永真性
    F:∀x,y,z.x>z∧y≥0→x+y>zF: \forall x,y,z.x>z\wedge y\ge 0\to x+y>zF:∀x,y,z.x>z∧y≥0→x+y>z

    2.5 数列理论2.5.1 定义符号集:
    ΣA:{=,⋅[⋅],⋅⟨⋅◃⋅⟩}\Sigma_A: \{=,\cdot [\cdot], \cdot \langle \cdot\triangleleft \cdot\rangle\}Σ​A​​:{=,⋅[⋅],⋅⟨⋅◃⋅⟩}
    其中,a[i]a[i]a[i]是一个二元函数,表示在索引为iii处读取aaa
    其中,a⟨i◃v⟩a\langle i\triangleleft v\ranglea⟨i◃v⟩是一个三元函数,代表在索引为iii处向aaa写入值vvv
    如果一个值vvv被写入到aaa的位置iii处,那么之后对于aaa位置iii处的读操作应当返回vvv
    逻辑是静态的,所以数组可以函数化表示,如(a⟨i1◃v1⟩)⟨i2◃v2⟩(a\langle i_1\triangleleft v_1\rangle)\langle i_2 \triangleleft v_2 \rangle(a⟨i​1​​◃v​1​​⟩)⟨i​2​​◃v​2​​⟩

    公理集:

    自反性、对称性、传递性的等价公理
    数组同余:∀a,i,j.i=j→a[i]=a[j]\forall a,i,j.i=j\to a[i]=a[j]∀a,i,j.i=j→a[i]=a[j]
    读写-1:∀a,v,i,j.i=j→a⟨i◃v⟩[j]=v\forall a,v,i,j.i=j\to a\langle i \triangleleft v\rangle [j]=v∀a,v,i,j.i=j→a⟨i◃v⟩[j]=v
    读写-2:∀a,v,i,j.i≠j→a⟨i◃v⟩[j]=a[j]\forall a,v,i,j. i\ne j\to a\langle i \triangleleft v\rangle [j]=a[j]∀a,v,i,j.i≠j→a⟨i◃v⟩[j]=a[j]

    注意:等价性只在数组元素之间被讨论。比如公式a[i]=v→a⟨i◃v⟩=aa[i] = v\to a\langle i\triangleleft v\rangle = aa[i]=v→a⟨i◃v⟩=a就不是TAT_AT​A​​-永真的。
    举例:证明以下公式的永真性
    F:a[i]=v→(∀j.a⟨i◃v⟩[j]=a[j])F: a[i]=v\to (\forall j.a\langle i\triangleleft v\rangle [j] = a[j])F:a[i]=v→(∀j.a⟨i◃v⟩[j]=a[j])
    2.5.2 性质
    不可判定
    但是量词自由片段可以判定
    0  留言 2020-06-29 21:05:56
  • 程序验证(三):一阶逻辑


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

    注意:原文中有部分公式书写错误,本文转载的时候,修正了这部分错误!
    一、语法1.1 逻辑符号包括:

    命题连接符:∧\wedge∧, ∨\vee∨ ,¬ \neg¬ , →\to→ , ↔\leftrightarrow↔
    变元:vvv, yyy, zzz, x1x_1x​1​​, x2x_2x​2​​, …
    量词:∃\exists∃, ∀\forall∀

    1.2 非逻辑符号(参数)包括:

    常量:c1c_1c​1​​, c2c_2c​2​​, …
    函数符号:ggg, hhh, fff, f1f_1f​1​​, f2f_2f​2​​, …
    谓词符号:rrr, qqq, ppp, p1p_1p​1​​, p2p_2p​2​​, …谓词与函数符号通过元数(arity)联系起来,也就是:元数:一个描述参数数量的自然数举例:

    =:: arity 2f(a,b,c): arity 3
    常量:可以视为0元函数

    1.3 项(term)项是用来描述对象的表达式。定义:

    常量是项
    变量是项
    对于n元函数符号fff,f(t1,..,tn)f(t_1, .., t_n)f(t​1​​,..,t​n​​)是一个项,如果t1,..,tnt_1, .. ,t_nt​1​​,..,t​n​​是项

    1.4 原子公式(atom)一阶逻辑(FOL)中的原子公式取值或为真、或为假。定义:

    对于⊥\bot⊥和⊤\top⊤均为原子
    对于每个n元谓词符号ppp,p(t1,..,tn)p(t_1, .., t_n)p(t​1​​,..,t​n​​)是一个原子如果t1,..,tnt_1, .. , t_nt​1​​,..,t​n​​是项
    一个文字(literal)是一个原子或它的非

    1.5 公式(formula)一个一阶逻辑公式是:

    一个文字
    使用¬,∧,∨,→,↔\neg ,\wedge ,\vee ,\to ,\leftrightarrow¬,∧,∨,→,↔连接的公式
    使用量词(quantifier)的公式(两种量词)

    全称量词 ∀x.F[x]\forall x.F[x]∀x.F[x]: For all xxx, F[x]F[x]F[x]
    存在量词 ∃x.F[x]\exists x.F[x]∃x.F[x]: There exists an xxx such that F[x]F[x]F[x]

    其中,xxx是约束变元(quantified variable),F[x]F[x]F[x]是量词的辖域(scope),xxx在F[x]F[x]F[x]中被量词约束(bind)。如果FFF中yyy没有被任何量词约束,那么它是自由(free)的

    一阶逻辑公式的一些名称:

    一个不包含自由变量的公式是关闭的(closed)(也叫做一个句子)
    一个包含自由变量的公式是开放的(open)
    一个不包含任何变量的公式是ground

    1.6 一阶逻辑表达式举例“All cats have more days than dogs”
    ∀x,y.dog(x)∧cat(y)→ndays(y)>ndays(x)\forall x,y.dog(x)\wedge cat(y)\to ndays(y) > ndays(x)∀x,y.dog(x)∧cat(y)→ndays(y)>ndays(x)“The numeric array a is sorted”
    ∀i.0≤i<∣a∣→a[i]≤a[i+1]\forall i.0\le i < |a|\to a[i] \le a[i+1]∀i.0≤i<∣a∣→a[i]≤a[i+1]“Graph G contains a triangle”
    ∃v1,v2,v3.e(v1,v2)∧e(v2,v3)∧e(v3,v1)\exists v_1 ,v_2 ,v_3 .e(v_1, v_2)\wedge e(v_2, v_3)\wedge e(v_3, v_1)∃v​1​​,v​2​​,v​3​​.e(v​1​​,v​2​​)∧e(v​2​​,v​3​​)∧e(v​3​​,v​1​​)二、语义一个一阶逻辑解构是一个对(pair)S=(D,I)S=(D,I)S=(D,I):

    其中DDD是论域(universe of discourse),也就是说,一个我们要讨论的对象的非空集合
    其中III是解释,是以下三种映射(map):

    从每个常量到DDD中的一个值
    每个n元函数变量fff到n元函数:
    fI:Dn↦Df_I:D^n \mapsto Df​I​​:D​n​​↦D每个n元谓词符号p到n元关系:
    pI⊆Dnp_I \subseteq D^np​I​​⊆D​n​​

    一个赋值(assignment)α:Vars→D\alpha : Vars\to Dα:Vars→D将每个变量映射到DDD中的一个值。
    举例:
    x+y>z→y>z−xx+y > z\to y>z-xx+y>z→y>z−x

    论域:D=Z={..,−1,0,1,..}D=Z = \lbrace .., -1,0,1, .. \rbrace D=Z={..,−1,0,1,..}
    解释:

    函数符号:+↦+Z,−↦−Z+\mapsto +{Z}, - \mapsto -{Z}+↦+Z,−↦−Z
    谓词符号:>↦>Z> \mapsto >_{Z}>↦>​Z​​

    一个可能的赋值:α={x↦0,y↦1,z↦−1}\alpha = \lbrace x\mapsto 0,y\mapsto 1, z\mapsto -1 \rbrace α={x↦0,y↦1,z↦−1}

    2.1 项求值给定解释III以及赋值α\alphaα,我们可以计算项在DDD中的值。给定一个项aaa,aaa的值⟨I,α⟩(a)\langle I,\alpha \rangle (a)⟨I,α⟩(a)是:

    如果aaa为常量:⟨I,α⟩(a)=I(a)\langle I,\alpha \rangle (a) = I(a)⟨I,α⟩(a)=I(a)
    如果aaa为变量:⟨I,α⟩(v)=α(v)\langle I,\alpha \rangle (v) = \alpha (v)⟨I,α⟩(v)=α(v)
    如果a=f(t1,..,tn)a=f(t_1, .. , t_n)a=f(t​1​​,..,t​n​​)是一个函数项:⟨I,α⟩(f(t1,..,tn))=I(f)(⟨I,α⟩(t1),..,⟨I,α⟩(tn))\langle I,\alpha \rangle (f(t_1, .. ,t_n)) = I(f)(\langle I,\alpha \rangle (t_1),..,\langle I, \alpha \rangle (t_n))⟨I,α⟩(f(t​1​​,..,t​n​​))=I(f)(⟨I,α⟩(t​1​​),..,⟨I,α⟩(t​n​​))

    2.2 公式求值给定DDD, III, α\alphaα,令FFF为一阶逻辑公式,我们有:
    D,I,α⊨F if F evaluatesto trueD,I, \alpha \models F \space if \space F \space evaluates to \space trueD,I,α⊨F if F evaluatesto true
    D,I,α⊭F if F evaluatesto falseD,I, \alpha \nvDash F \space if \space F \space evaluates to \space falseD,I,α⊭F if F evaluatesto false
    对于原子:
    D,I,α⊨⊤ and D,I,α⊭⊥D,I, \alpha \models \top \space and \space D,I, \alpha \nvDash \botD,I,α⊨⊤ and D,I,α⊭⊥
    D,I,α⊨p(t1,..,tn) iff (⟨I,α⟩(t1),..,⟨I,α⟩(tn))∈I(p)D,I, \alpha \models p(t_1,..,t_n) \space iff \space (\langle I, \alpha\rangle (t_1),..,\langle I, \alpha \rangle (t_n)) \in I(p)D,I,α⊨p(t​1​​,..,t​n​​) iff (⟨I,α⟩(t​1​​),..,⟨I,α⟩(t​n​​))∈I(p)
    对于复合情况下的归纳定义:
    D,I,α⊨¬F iff D,I,α⊭FD,I,\alpha \models \neg F \space iff \space D,I,\alpha \nvDash FD,I,α⊨¬F iff D,I,α⊭F
    D,I,α⊨F1∧F2 iff D,I,α⊨F1 and D,I,α⊨F2D,I,\alpha \models F_1\wedge F_2 \space iff \space D,I,\alpha \models F_1 \space and \space D,I,\alpha\models F_2D,I,α⊨F​1​​∧F​2​​ iff D,I,α⊨F​1​​ and D,I,α⊨F​2​​
    D,I,α⊨F1∨F2 iff D,I,α⊨F1 or D,I,α⊨F2D,I,\alpha \models F_1\vee F_2 \space iff \space D,I,\alpha \models F_1 \space or \space D,I,\alpha\models F_2D,I,α⊨F​1​​∨F​2​​ iff D,I,α⊨F​1​​ or D,I,α⊨F​2​​
    D,I,α⊨F1→F2 iff D,I,α⊭F1 or I⊨F2D,I,\alpha \models F_1 \to F_2 \space iff \space D,I,\alpha \nvDash F_1 \space or \space I\models F_2D,I,α⊨F​1​​→F​2​​ iff D,I,α⊭F​1​​ or I⊨F​2​​
    D,I,α⊨F1↔F2 iff D,I,α⊨F1 and I⊨F2 ,or D,I,α⊭F1 and D,I,α⊭F2D,I,\alpha\models F_1 \leftrightarrow F_2 \space iff \space D,I,\alpha \models F_1 \space and \space I\models F_2 \space, or \space D,I,\alpha \nvDash F_1 \space and \space D,I,\alpha \nvDash F_2D,I,α⊨F​1​​↔F​2​​ iff D,I,α⊨F​1​​ and I⊨F​2​​ ,or D,I,α⊭F​1​​ and D,I,α⊭F​2​​
    举例:
    对于论域D=∘,∙D={\circ, \bullet}D=∘,∙,赋值α=x↦∙,y↦∘\alpha = {x\mapsto \bullet , y\mapsto \circ}α=x↦∙,y↦∘,以及III:
    I(a)=∘I(a) = \circI(a)=∘
    I(f)=(∘,∘)↦∘,(∘,∙)↦∙,(∙,∘)↦∙,(∙,∙)↦∘I(f) = {(\circ , \circ)\mapsto \circ ,(\circ ,\bullet)\mapsto \bullet ,(\bullet ,\circ)\mapsto \bullet ,(\bullet ,\bullet)\mapsto \circ}I(f)=(∘,∘)↦∘,(∘,∙)↦∙,(∙,∘)↦∙,(∙,∙)↦∘
    I(g)=∘↦∙,∙↦∘I(g) = {\circ\mapsto\bullet ,\bullet\mapsto\circ}I(g)=∘↦∙,∙↦∘
    I(p)=(∘,∙),(∙,∙)I(p) = {(\circ ,\bullet),(\bullet ,\bullet)}I(p)=(∘,∙),(∙,∙)
    p(a,g(∘))=truep(a,g(\circ)) = truep(a,g(∘))=true
    p(x,f(g(x),y))→p(y,g(x))=truep(x,f(g(x),y))\to p(y,g(x)) = truep(x,f(g(x),y))→p(y,g(x))=true
    2.3 量词求值给定一个变元xxx,以及一个赋值α\alphaα,一个α\alphaα的xxx变元,写作α[x↦c]\alpha [x\mapsto c]α[x↦c],是这样的赋值:

    除xxx外的变量都与α\alphaα取值相同
    将xxx赋值为某个给定的值c∈Dc\in Dc∈D,那么我们可以这样表示量词:
    全称量词:
    D,I,α⊨∀x.F iff for all c∈D,D,I,α[x↦c]⊨FD,I,\alpha \models \forall x.F \space iff \space for \space all \space c\in D,D,I,\alpha [x\mapsto c]\models FD,I,α⊨∀x.F iff for all c∈D,D,I,α[x↦c]⊨F
    存在量词:
    D,I,α⊨∃x.F iff there exists c∈D,D,I,α[x↦c]⊨FD,I,\alpha \models \exists x.F \space iff \space there \space exists \space c\in D,D,I,\alpha [x\mapsto c]\models FD,I,α⊨∃x.F iff there exists c∈D,D,I,α[x↦c]⊨F

    2.4 可满足性与永真性一个一阶逻辑公式FFF是可满足的当且仅当:存在S=(D,I)S=(D,I)S=(D,I)以及赋值α\alphaα使得D,I,α⊨FD,I,\alpha \models FD,I,α⊨F。
    一个一阶逻辑公式FFF是永真的当且仅当:对于所有S=(D,I)S=(D,I)S=(D,I)以及赋值α\alphaα,D,I,α⊨FD,I,\alpha \models FD,I,α⊨F。
    当FFF是永真的时,记作⊨F\models F⊨F。
    可满足性与永真性二者是对偶的。
    三、证明系统3.1 永真性证明类似于命题逻辑中的证明方法:

    假定FFF不是永真的,存在III使得I⊭FI \nvDash FI⊭F
    应用证明规则
    如果没有矛盾,没有能够继续应用的证明规则,那么得出结论:FFF是非永真的
    如果每一个分支都推出矛盾,得出结论:FFF是永真的

    3.2 证明规则全称量词1

    如果我们知道D,I,α⊨∀x.p(x,α)D,I,\alpha\models \forall x.p(x,\alpha)D,I,α⊨∀x.p(x,α),那么我们得出结论:D,I,α[x↦b]⊨p(x,a)D,I,\alpha [x\mapsto b]\models p(x,a)D,I,α[x↦b]⊨p(x,a)。
    全称量词2

    这里,fresh的意思是在证明中没有用过。
    如果D,I,α⊭∀x.FD,I,\alpha \nvDash \forall x.FD,I,α⊭∀x.F,那么我们只知道FFF对于某些对象不成立,但我们不知道对哪个对象不成立。
    因此,我们选择一个新的(fresh),不做假设。
    存在量词1:

    存在量词2:

    不论xxx映射为什么,FFF都不成立。
    3.3 得到矛盾
    前两个前提的赋值都是α\alphaα的variant,只要ppp的值不同,矛盾就产生了。
    例如:

    举例:证明以下公式是永真的
    F:(∀x.p(x))→(∀y.p(y))F: (\forall x.p(x))\to (\forall y.p(y))F:(∀x.p(x))→(∀y.p(y))

    3.4 可靠性与完备性(soundness and completeness)
    可靠性:如果语义分析(semantic argument)的每一分支都得到矛盾,那么FFF是永真的。也就是说,证明规则不会得到错误的结果
    完备性:如果FFF是完备的,那么存在一个有限长的证明序列,其中每一分支都能得到矛盾。也就是说,不存在我们不能证明为永真式的永真式。这叫做指称完备性(refutational completeness)。

    四、一阶逻辑的可判定性一个判定问题当且仅当存在一个过程PPP满足对于任何输入:

    答案为真时,停机并输出真
    答案为假时,停机并输出假

    一阶逻辑是不可判定的(丘奇(Church)&图灵(Turing)),但一阶逻辑是半可判定的,即当FFF是永真的时,程序总是终止,当FFF不是永真的时,程序可能不终止。
    0  留言 2020-06-29 13:49:44
  • 程序验证(二):SAT问题


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

    注意:原文中有部分公式书写错误,本文转载的时候,修正了这部分错误!
    一、概念:Satisfiability ProblemSAT问题:给定一个命题公式FFF,决定是否存在一个解释III使得I⊨FI\models FI⊨F。
    3SAT问题是首个被确定的NP完全问题。
    大多数重要逻辑问题可以归约为SAT:

    永真性
    蕴含
    等价性

    SAT求解能力的发展关键:将搜索与推理结合以提高效率。
    二、CNF详解SAT求解器的输入一般是CNF,这里为便于讨论,引入关于CNF的集合表示。
    2.1 集合表示一个公式(formula)可以视为子句(clause)的集合:

    可以表示为:

    同样,子句可以视为文字(literal)的集合:

    可以表示为:

    一些通用的表示方法:
    Ci{P↦F}C_i\left \lbrace P\mapsto F \right \rbraceC​i​​{P↦F}:在子句CiC_iC​i​​中使用FFF替代PPP。
    Ci[P]C_i\left [ P \right ]C​i​​[P]:变量PPP在子句CiC_iC​i​​中是不取非的,也就是 Ci={..,P,..}C_i = \lbrace .. , P , .. \rbrace C​i​​={..,P,..} 。
    Ci[¬P]C_i[\neg P]C​i​​[¬P]:变量PPP在CiC_iC​i​​中是取非的,也就是Ci={..,¬P,..}C_i = \lbrace .. , \neg P , .. \rbrace C​i​​={..,¬P,..} 。
    在这种符号体系下,会有以下命题成立(有点绕,需要多看几遍):
    以FFF表示公式,CCC表示子句,基于CNF公式的集合表示,有:

    2.2 归结(resolution)只有一条规则:

    给定两个具有相同变量PPP,但是对于PPP取非情况不同的两个子句,那么:

    如果PPP为真,那么C2C_2C​2​​中的其它文字必然为真
    如果PPP为假,那么C1C_1C​1​​中的其它文字必然为假

    因此,可以在两个子句中都移除PPP,也就是归结。
    C1{P↦⊥}∨C2{¬P↦⊥}C_1\{P\mapsto \bot\}\vee C_2\{\neg P\mapsto\bot\}C​1​​{P↦⊥}∨C​2​​{¬P↦⊥}叫做归结式(resolvent)。这个归结式可以作为一个合取子句加入到原公式,这样得到的新公式与原公式等价。
    而如果:
    C1{p↦⊥}∨C2{¬P↦⊥}=⊥∨⊥=⊥C_1\{p\mapsto \bot\}\vee C_2\{\neg P\mapsto\bot\}=\bot\vee\bot=\botC​1​​{p↦⊥}∨C​2​​{¬P↦⊥}=⊥∨⊥=⊥那么C1∧C2C_1\wedge C_2C​1​​∧C​2​​是不可满足的。任何包括 {C1,C2} \lbrace C_1,C_2 \rbrace {C​1​​,C​2​​} 在内的CNF都是不可满足的。
    举例:
    A∨B∨CA\vee B\vee CA∨B∨C与¬A∨B∨D\neg A\vee B\vee D¬A∨B∨D的归结子句是B∨C∨DB\vee C\vee DB∨C∨D。
    三、归结法求解SAT3.1 归结算法

    F′F^{\prime}F​′​​ 是所有归结式的集合
    每一轮迭代,更新FFF以包含以产生的归结式
    每一轮迭代,计算所有可能的归结式
    在更新后的FFF上重复归结过程
    终止条件:

    出现⊥\bot⊥归结式
    无法再更新FFF(此时所有的可归结的子句都已经被归结了)


    举例:
    (P∨Q)∧(P→R)∧(Q→R)∧¬R(P\vee Q)\wedge (P\to R)\wedge (Q\to R)\wedge \neg R(P∨Q)∧(P→R)∧(Q→R)∧¬R

    3.2 归结算法的评价解决较大规模问题的效率低下。
    四、基于搜索的方法大致思路:从一个空的解释(interpretation)出发,每次扩展一个变量的取值。
    4.1 部分解释如果III是一个部分解释,文字ℓ\ellℓ可以为true,false,undeftrue, false, undeftrue,false,undef:

    若truetruetrue(satisfied):I⊨ℓI\models \ellI⊨ℓ
    若falsefalsefalse(conflicting):I⊭ℓI \nvDash \ellI⊭ℓ
    若undefundefundef:var(ℓ)∉Ivar(\ell)\notin Ivar(ℓ)∉I

    给定一个子句CCC和解释III:

    若CCC is truetruetrue under III iff I⊨CI\models CI⊨C
    若CCC is falsefalsefalse under III iff I⊭CI \nvDash CI⊭C
    若CCC is unitunitunit under III iff C=C′∨ℓ,I⊭C′,ℓC=C^{\prime} \vee \ell, I \nvDash C^{\prime}, \ellC=C​′​​∨ℓ,I⊭C​′​​,ℓ is undefundefundef
    Otherwise it is undefundefundef

    说明:iff: if and only if,当且仅当unit: 单元,一个新引入的概念举例:
    令I={P1↦1,P2↦0,P4↦1}I= \lbrace P_1\mapsto 1,P_2\mapsto 0,P_4\mapsto 1 \rbraceI={P​1​​↦1,P​2​​↦0,P​4​​↦1},那么有:

    1.P1∨P3∨¬P4P_1\vee P_3\vee\neg P_4P​1​​∨P​3​​∨¬P​4​​ is truetruetrue
    2.¬P1∨P2\neg P_1\vee P_2¬P​1​​∨P​2​​ is falsefalsefalse
    3.¬P1∨¬P4∨P3\neg P_1\vee\neg P_4 \vee P_3¬P​1​​∨¬P​4​​∨P​3​​ is unitunitunit
    4.¬P1∨P3∨P5\neg P_1\vee P_3 \vee P_5¬P​1​​∨P​3​​∨P​5​​ is undefundefundef

    4.2 搜索程序:一个状态机每一个状态都记录了部分解释与当前的公式,状态之间的转化由转化规则决定。程序的状态包括:

    1.satsatsat
    2.unsatunsatunsat
    3.[I]∥F[I]\Vert F[I]∥F,这里的[I][I][I]是一个解释,FFF是一个CNF

    初始状态:[Φ]∥F[\Phi]\Vert F[Φ]∥F
    结束状态:sat,unsatsat, unsatsat,unsat
    中间状态:

    (1) [Φ]∥F1[\Phi]\Vert F_1[Φ]∥F​1​​, CCC:解释为空,F=F1∧CF=F_1\wedge CF=F​1​​∧C
    (2) [I1,P¯,I2]∥F[I_1,\bar{P},I_2]\Vert F[I​1​​,​P​¯​​,I​2​​]∥F:解释先置为I1I_1I​1​​,然后P↦0P\mapsto 0P↦0,然后解释为I2I_2I​2​​



    4.3 搜索规则通俗的说,就是深度优先搜索。在某些算法中优化了回退策略。
    判定规则(Decision Rule)

    回退规则(Backtrack Rule)

    可满足规则(Sat Rule)

    不可满足规则(Unsat Rule)

    以上 4 条规则足以构建一个基本的 sat 求解器。
    单元传播规则(Unit Propagation Rule)

    条件是

    4.4 高级回退&子句学习基础的回退规则比较“笨”:

    它总是回退到最近确定的解释
    它不保留子句冲突的信息

    引入回跳规则(BackJump Rule):

    这里C→lC\to lC→l就叫做冲突子句,我们只要避免冲突子句就可以进一步寻找解。
    那么,如何找到冲突子句呢?
    构造一个蕴含图(implication graph) G=(V,E)G=(V,E)G=(V,E):

    其中VVV对于解释III中每一个判定文字都有一个节点,用这个文字的值和它的判定等级来标记(说白了就是这个文字是你所判定的第几个文字)
    对于每个子句C=ℓ1∨..∨ℓn∨ℓC=\ell_1\vee .. \vee\ell_n \vee \ellC=ℓ​1​​∨..∨ℓ​n​​∨ℓ,其中ℓ1,..,ℓn\ell_1, .. ,\ell_nℓ​1​​,..,ℓ​n​​被赋值为假,首先为ℓ\ellℓ添加一个节点,它的判定等级就是它进入到III的顺序,然后添加边(ℓi,ℓ)(\ell_i, \ell)(ℓ​i​​,ℓ)到EEE,其中1≤i≤n1\le i\le n1≤i≤n
    添加一个冲突节点Λ\LambdaΛ。对于所有标记为PPP与¬P\neg P¬P的冲突变元,在EEE中添加从这些节点到Λ\LambdaΛ的边
    将每条边都标记上导致这个蕴含关系的子句

    例如:

    冲突图:只有一个冲突变元,且所有节点都具有通往Λ\LambdaΛ的路径的蕴含图。
    例如:

    获得冲突子句,考虑一个冲突图GGG:

    在GGG中切一刀,使得:

    所有的判定节点在一侧(“原因”)至少一个冲突文字在另一侧(“结果”)
    在“原因”一侧中,选出所有与被切割的边相连的节点KKK
    在KKK中的节点即为冲突的原因
    相应的文字的非生成了冲突子句

    例如:

    图中¬P5∨¬P2\neg P_5\vee\neg P_2¬P​5​​∨¬P​2​​和¬P5∨P6\neg P_5\vee P_6¬P​5​​∨P​6​​可以作为冲突子句。
    4.5 DPLL & CDCLCDCL即为(Conflict-Driven Clause Learning),是目前SAT求解器主要采用的方法。
    0  留言 2020-06-29 10:51:21
  • Tseitin算法


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

    Tseitin算法是一个在线性时间内将命题公式转化为CNF范式的算法。
    例子:使用 Tseitin 算法将以下命题公式转化为 CNF 范式

    上述公式等价于:

    Tseitin算法
    为每个非原子子式引入一个新变量:

    将上述每个等价式转换为 CNF:

    最后将T1T_1T​1​​与转换后的CNF进行合取,得到最终的CNF:

    F1F_1F​1​​到F4F_4F​4​​其实就是第二步(就是T在箭头左边那些式子)的等价变形。
    0  留言 2020-06-28 12:56:37
  • 程序验证(一):命题逻辑


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

    注意:原文中有部分公式书写错误,本文转载的时候,修正了这部分错误!
    一、概念1.1 命题逻辑例如:


    一个原子(atom)是一个或为真或为假的判断
    一个文字(literal)是一个原子或它的非
    命题公式(propositional formulas)由文字和逻辑连接符组成

    1.2 合式公式合式公式(well-formed formulas) 由以下语法得到:

    举例:

    1.3 语义目的:给命题逻辑赋予涵义,把布尔值赋值给(公式,解释)对,即

    什么是解释?
    对于一个命题公式FFF,一个解释III将FFF中每个命题变元映射为一个布尔值,也就是说:

    满足解释:
    如果命题公式在解释III下值为真,那么说III是FFF的满足解释(satisfying interpretation),记作:

    不满足解释:
    如果命题公式在解释III下值为假,那么说III是FFF的不满足解释(falsifying interpretation),记作:

    语义的归纳定义:
    首先定义原子的涵义,然后根据这些定义,定义每个逻辑连接的涵义。
    举例:


    1.4 可满足性与永真性一个公式FFF是可满足的(satisfiable)当且仅当存在一个解释III使得I⊨FI\models FI⊨F
    一个公式FFF是永真的(valid)当且仅当对于所有解释III,I⊨FI\models FI⊨F
    注意:可满足性与永真性是成对的(dual)符号,即FFF是永真的当且仅当¬F\neg F¬F是不可满足的。
    如何证明可满足性?

    真值表穷举:蛮力搜索复杂度为2n2^n2​n​​,其中nnn为变元的数量
    演绎推理:语义讨论(Semantic Argument)

    假定FFF为非永真的,即存在III不满足FFF
    应用推理规则
    如果每一分支都得到矛盾,那么FFF是永真的
    如果没有矛盾,且不能进一步应用推理规则,那么FFF是非永真的


    二、语义规则2.1 公式
    这个规则产生了分支:

    例子1:

    例子2:

    发现矛盾,所以FFF是永真的。
    注意:⇒\Rightarrow⇒ 这样的双线箭头不属于命题逻辑的符号集。
    三、范式(Normal Forms)3.1 概念一种逻辑的范式,应当:

    限制公式的语法(Restricts the syntax of formulas)
    对于此逻辑中的任意公式,范式具有等价的表达能力(Has equivalent representation for any formula in the logic)

    3.2 三种主要范式Negation Normal Form (NNF):只包含 ∧\wedge∧、∨\vee∨、¬\neg¬ 三个符号,且 ¬\neg¬ 只能用于文字(literal)。
    Disjunctive Normal Form (DNF):合取子句的析取。
    Conjunctive Normal Form (CNF):析取子句的合取。
    举例:

    四、范式转化由于主流的SAT solver(就是一个程序,输入一个公式,输出这个公式是否是可满足的,例子见一个简单的DPLL实现)一般接受CNF为输入,所以面对一个一般的公式,我们需要先把它转化为一个CNF。如何实现?等价的转换比较困难,但是我们可以采用一种逻辑上更弱的方法,即进行可满足性等价(equisatisfiability)转换。也就是说,我不要求转换后的CNF与原来的公式在所有的解释下真值都一样,我只要求若CNF可满足,则原公式可满足;若原公式可满足,则CNF可满足。
    转换的方法,可采用 Tseitin 算法.
    0  留言 2020-06-28 12:56:21
  • 从零开始编写SAT求解器


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

    一、源起二、背景知识2.1 SAT问题2.2 DIMACS文件2.3 DPLL算法三、项目架构四、文件解析器五、assert宏六、核心算法 DPLL七、其他文件八、测试效果8.1 输入8.2 输出一、源起最近在github上看到了非常有名的cryptominisat开源项目。目前的SAT问题自动求解器有在线版的MiniSAT,但是这个需要科学上网。正好最近一直在写Java和python,C++有点生疏,而网上有大神用Haskell实现了简易的SAT求解器,就想用C++写一个自己的SAT求解器。(C++是最棒的语言)
    二、背景知识2.1 SAT问题SAT问题是布尔可满足性问题(又名命题可满足性问题)的缩写,即给定一个布尔公式,判断是否存在满足它的解释的问题。SAT问题是第一个被证明的NP问题。这里,我把问题简化为:输入一个析取范式(CNF),输出一个布尔值表示它是否是可满足的,若它是可满足的,再输出一个使它为真的解释。
    2.2 DIMACS文件DIMACS文件是对于CNF形式的命题公式的一种简单的ASCII表示,它的结构为:

    开头是几行注释,以字符 ’c’ 开头
    注释行之后,是一个文件头,格式为 p cnf nvars nclauses,这里nvars是公式中变量的数量,nclauses是命题中子句的数量
    在文件头之后,每一行代表一个子句。一个子句是一系列空格分隔的非零整数,最后以0结尾。一个正数代表对应的变量(从1到nvars),一个负数代表对应变量的非

    举个例子:
    c A simple examplep cnf 3 3-1 2 0-2 3 0-1 -3 0
    它代表的公式是:

    2.3 DPLL算法DPLL算法是一个判断命题公式可满足性的算法,本质上是一个深度优先搜索算法。基本思想为:首先假定一个变量的值(真/假),然后检查当前条件下命题公式是否为真,若为真,程序退出,返回可满足以及一个使命题公式为真的解释;若为假,则回溯(可能改变当前变量的假定值,或退到之前的某个变量);若为假且没有变量可以回溯,程序退出,返回该公式是不可满足的。
    三、项目架构main函数如下:
    #include <chrono>#include "common.h"#include "DimacsParser.h"#include "DPLL.h"int main(int argc, char **argv) { //argc=2; if (argc < 2) { std::cerr << "error: no input files" << std::endl; return 1; } for (int i = 1; i < argc; i++) { std::string f(argv[i]); //std::string f="tests\\test5.dimacs"; std::cout << f << std::endl; formula phi = DimacsParser::parse(f); // timer start auto start = std::chrono::steady_clock::now(); DPLL solver(phi); bool sat = solver.check_sat(); model m; if (sat) { m = solver.get_model(); } auto end = std::chrono::steady_clock::now(); // timer end if (sat) { std::cout << " sat" << std::endl; for (const auto &p : m) { std::cout << " " << p.first << " -> " << p.second << std::endl; } } else { std::cout << " unsat" << std::endl; } auto duration = std::chrono::duration_cast<std::chrono::duration<double>>(end - start); std::cout << " time: " << duration.count() << std::endl; } return 0;}
    采用命令行输入,首先判断参数合法性,若合法,读入文件,将文件解析,返回自定义的formula对象。接着调用DPLL方法,返回是否可解;若可解,输出一个可行的解。可行解使用map存储。
    那么,接下来的任务就是实现文件解析、DPLL核心算法。
    四、文件解析器//// Dimacs parser.//filename:DimacsParser.h//#include <iostream>#include <fstream>#include <cstdlib>#include <cassert>#include "common.h"#ifndef DPLL_DIMACSPARSER_H#define DPLL_DIMACSPARSER_Hclass DimacsParser {public: /** * Parse a dimacs file. * @param file_name dimacs file name * @return a parsed formula (if succeeds) */ static formula parse(const std::string &file_name) { std::ifstream fin(file_name); if (!fin) { std::cerr << "file not found: " << file_name << "'" << std::endl; std::exit(1); } int n = 0, m = 0; while (!fin.eof()) { char ch; fin >> ch; if (ch == 'c') { // c-line: comment char buf[1024]; fin.getline(buf, 1024); } else if (ch == 'p') { // p-line: clauses will begin std::string buf; fin >> buf; assert(buf == "cnf"); fin >> n >> m; break; } else { // unexpected line std::cerr << "parse error at char '" << ch << "'" << std::endl; std::exit(1); } } // clauses begin std::vector<clause> clauses; for (int i = 0; i < m; i++) { clause c; while (!fin.eof()) { int v; fin >> v; if (v == 0) { clauses.push_back(c); break; } assert(VAR(v) <= n); c.push_back(v); } } assert(clauses.size() == m); return formula(n, clauses); }};#endif //DPLL_DIMACSPARSER_H
    五、assert宏assert宏的原型定义在<assert.h>中,其作用是如果它的条件返回错误,则终止程序执行,原型定义:
    #include <assert.h>void assert( int expression );
    assert的作用是现计算表达式 expression ,如果其值为假(即为0),那么它先向stderr打印一条出错信息,然后通过调用 abort 来终止程序运行。
    请看下面的程序清单badptr.c:
    #include <stdio.h>#include <assert.h>#include <stdlib.h>int main( void ){ FILE *fp; fp = fopen( "test.txt", "w" );//以可写的方式打开一个文件,如果不存在就创建一个同名文件 assert( fp ); //所以这里不会出错 fclose( fp ); fp = fopen( "noexitfile.txt", "r" );//以只读的方式打开一个文件,如果不存在就打开文件失败 assert( fp ); //所以这里出错 fclose( fp ); //程序永远都执行不到这里来 return 0;}
    执行这个文件,输出:
    [root@localhost error_process]# gcc badptr.c [root@localhost error_process]# ./a.out a.out: badptr.c:14: main: Assertion `fp'' failed.
    使用assert的缺点是,频繁的调用会极大的影响程序的性能,增加额外的开销。
    在调试结束后,可以通过在包含#include <assert.h>的语句之前插入 #define NDEBUG 来禁用assert调用,示例代码如下:
    #include <stdio.h>#define NDEBUG#include <assert.h>
    用法总结与注意事项:

    在函数开始处检验传入参数的合法性,如:
    int resetBufferSize(int nNewSize){ //功能:改变缓冲区大小, //参数:nNewSize 缓冲区新长度 //返回值:缓冲区当前长度 //说明:保持原信息内容不变 nNewSize<=0表示清除缓冲区 assert(nNewSize >= 0); assert(nNewSize <= MAX_BUFFER_SIZE); ...}
    每个assert只检验一个条件,因为同时检验多个条件时,如果断言失败,无法直观的判断是哪个条件失败“不好”例子:
    assert(nOffset>=0 && nOffset+nSize<=m_nInfomationSize);
    “好”例子:
    assert(nOffset >= 0);assert(nOffset+nSize <= m_nInfomationSize);
    不能使用改变环境的语句,因为assert只在DEBUG个生效,如果这么做,会使用程序在真正运行时遇到问题“错误”例子:
    assert(i++ < 100)
    “正确”例子:
    assert(i < 100) i++;
    assert和后面的语句应空一行,以形成逻辑和视觉上的一致感
    有的地方,assert不能代替条件过滤

    六、核心算法 DPLL//DPLL.cpp#include "DPLL.h"bool DPLL::check_sat() { // TODO: your code here, or in the header file std::unordered_map<int,int> atomStatus;//记录节点状态0,1,2 int clause_num = phi.clauses.size();//子句数量 int atomNum = phi.num_variable;//变量数量 for(int i=1;i<=atomNum;i++) result.insert(std::make_pair(i,true)); int* nodeStatus = new int[atomNum]; for(int i=0;i<atomNum;i++) nodeStatus[i]=0; int ptr = 0;//指向当前节点 while(true){ if(nodeStatus[ptr]==2) break; else if(nodeStatus[ptr]==0) { nodeStatus[ptr]++; result[ptr + 1] = false; } else { nodeStatus[ptr]++; result[ptr + 1] = true; } int solveStatus = 2;//0 肯定不是解,1 肯定是解,2 不确定 //检查是否是解 bool wholeValue = true;//整个式子的真值 for(int i=0;i<clause_num;i++) //每个子句 { bool currValue=false;//这个子句是不是假的 bool any_notsure=false;//有没有不确定的literature int len = phi.clauses[i].size(); for(int j=0;j<len;j++) { int currvar = phi.clauses[i][j]; if(VAR(currvar)<=ptr+1) { if((POSITIVE(currvar)&&result[currvar])||(NEGATIVE(currvar)&&!result[VAR(currvar)])){//有一个为真,子句为真 currValue=true; break; } } else{ any_notsure=true; } } wholeValue=wholeValue&&currValue; if(currValue||any_notsure){ continue; } else{ solveStatus=0; break; } } if(wholeValue) solveStatus=1; //检查完毕 if(solveStatus==0)//肯定不是解,回溯 { while(ptr>0&&nodeStatus[ptr]==2) ptr--; for(int i=ptr+1;i<atomNum;i++) nodeStatus[i]=0; } else if(solveStatus==1) return true; else ptr++; } return false;}model DPLL::get_model() { // TODO: your code here, or in the header file return this->result;}
    其基本流程我举个例子:

    假设五个变量A,B,C,D,E
    我先假定A取真,其他的不确定,然后我检查输入的CNF是否为真

    如果是真,那太好了,返回退出如果不确定,那我再假定B取真,再检查如果是假,那么回溯/取另外一个值

    怎么回溯?再举个例子:

    假如ABCDE分别是1,1,1,1,null,这时发现CNF为假!
    现在指针指向的是D,所以从D取另外的值,此时ABCDE分别为1,1,1,0,null
    发现还是不行,CNF为假,这时就要回溯,回溯到哪?递归的搜索当前节点的父亲,直到找到这样一个节点,它还有没有取到的值(也就是说它没“脏”),或者到根节点(此时如果根节点为“脏”,证明所有情况搜索完毕,输入的CNF是不可满足的)
    回溯完成后,注意,在当前节点以下的所有节点,它们的状态都被重新标记为“干净”,也就是它们既没有取过真值,也没有取过假值,因为它们的父节点状态发生了变化,相当于它们即使与之前取同样的布尔值,ABCDE作为一个整体,这五个布尔值的组合也与之前不同

    七、其他文件common.h
    #include <vector>#include <unordered_map>#include <string>#include <sstream>#ifndef DPLL_COMMON_H#define DPLL_COMMON_H// A literal is a atomic formula (that contains a variable). Like in dimacs,// + positive numbers denote the corresponding variables;// - negative numbers denote the negations of the corresponding variables.// Variables are numbered from 1.typedef int literal;#define POSITIVE(x) ((x) > 0)#define NEGATIVE(x) ((x) < 0)#define VAR(x) (((x) > 0) ? (x) : (-(x)))// A clause is a list of literals (meaning their disjunction).typedef std::vector<literal> clause;// A formula is a list of clauses (meaning their conjunction).// We also specify the total number of variables, as some of them may not occur in any clause!struct formula { int num_variable; std::vector<clause> clauses; formula(int n, const std::vector<clause>& clauses): num_variable(n), clauses(clauses) {}};// A satisfying model (interpretation).// e.g. `model[i] = false` means variable `i` is assigned to false.typedef std::unordered_map<int, bool> model;#endif //DPLL_COMMON_H
    DPLL.h
    #ifndef DPLL_DPLL_H#define DPLL_DPLL_H#include "common.h"class DPLL {public: DPLL(const formula &phi) : phi(phi) {} bool check_sat(); model get_model();private: formula phi; model result;};#endif //DPLL_DPLL_H
    CMakeLists.txt
    # cmake_minimum_required(VERSION <specify CMake version here>)cmake_minimum_required(VERSION 3.15)project(dpll)set(CMAKE_CXX_STANDARD 17)set(CMAKE_BUILD_TYPE "Debug")set(CMAKE_CXX_FLAGS_DEBUG "$ENV{CXXFLAGS} -O0 -Wall -g -ggdb")set(CMAKE_CXX_FLAGS_RELEASE "$ENV{CXXFLAGS} -O2 -Wall")add_executable(dpll main.cpp DimacsParser.h common.h DPLL.cpp DPLL.h common.h DPLL.h DimacsParser.h)
    八、测试效果8.1 输入c Generated with `cnfgen`c (C) 2012-2016 Massimo Lauria <lauria.massimo@gmail.com>c https://massimolauria.github.io/cnfgencp cnf 12 321 -2 0-1 2 01 3 4 01 -3 -4 0-1 3 -4 0-1 -3 4 03 -5 0-3 5 02 6 -7 02 -6 7 0-2 6 7 0-2 -6 -7 04 6 8 -9 04 6 -8 9 04 -6 8 9 04 -6 -8 -9 0-4 6 8 9 0-4 6 -8 -9 0-4 -6 8 -9 0-4 -6 -8 9 05 8 -10 05 -8 10 0-5 8 10 0-5 -8 -10 07 11 0-7 -11 09 11 -12 09 -11 12 0-9 11 12 0-9 -11 -12 010 -12 0-10 12 0
    8.2 输出
    0  留言 2020-06-27 16:35:56
  • 基于Python使用TensorBoard可视化工具

    首先展示一下代码:
    writer = tf.summary.FileWriter("./summary/linear-regression-0/", sess.graph)
    我们将数据流图的事件保存到当前目录下的/summary/linear-regression-0/中,记得后面关闭一下 writer.close(),我们来看一下运行后的结果。

    那么我们现在需要如何显示呢?写这个目的就是告诉到家是如何使用 TensorBoard 可视化的,步骤如下:

    Windows+R 打开 Terminal
    cd 到 summary 目录(注意不是 cd 到 linear-regression-0 目录)
    使用 TensorBoard —logdir=linear-regression-0

    我们来看一下图应该就能明白:

    如果打不开,中间的 DESKTOP-A0JMDP5 换成 localhost 试试!好了!现在让我们输入网址试试:
    1  留言 2019-04-20 12:27:01
  • 基于Detours库HOOK API

    背景可能我们开发程序的时候,会用到Inline Hook Api的技术。Inline Hook 的原理是在系统访问一个函数的时候先替换原函数入口处的内容跳转到自己设计的Hook函数中,然后在自己函数中进行Hook工作。但在并行系统中,很可能有个线程就在这个时候调用了被自己改掉的系统函数,出现我们无法预期的结果。
    这时,我们可以考虑使用Detuors库。Detours是微软开发的一个函数库,可用于捕获系统API。Detours库Hook过程原理和我们自己写的基本一样,不同的地方在于微软做了封装和相关的冲突检查,所以这种基于Detoursku的Api Hook更稳定些。
    现在,我对使用Detours库进行HOOK API进行下讲解,并写成文档,分享给大家。
    前期准备本文开发的程序是使用VS2013进行开发的,开发之前,需要到微软的官网上下载Detuors库的源码程序,然后在本地编译得到库文件。至于Detours库的下载地址以及具体的编译步骤,可以参考本站上其他人写的“使用VS2013编译Detours库”这篇文章,里面有详细介绍。
    实现原理我们把使用Detuors库HOOK API的代码实现都写在DLL里面,方便以后的调用。在DLL加载的时候,即DLL入口点函数DllMain的DLL_PROCESS_ATTACH中,执行HOOK部分的代码。在DLL卸载的时候,即DLL入口函数DllMain的DLL_PROCESS_DETACH中,执行UNHOOK部分的代码。
    那么,HOOK的原理是:

    首先,先调用Detours函数DetourRestoreAfterWith,恢复之前状态,避免反复拦截
    然后,调用DetourTransactionBegin,表示开始事务,准备HOOK;并调用DetourUpdateThread刷新当前线程
    接着,开始调用DetourAttach函数设置HOOK,可以连续多次HOOK不同的API函数
    最后,使用DetourTransactionCommit提交事务,上一步设置的HOOK操作,会立即生效

    其中,DetourAttach传的是实际的API函数地址的指针和代替API函数的替代函数地址。
    UNHOOK的原理和HOOK的原理是差不多的,原理是:

    首先,调用DetourTransactionBegin,表示开始事务,准备HOOK;并调用DetourUpdateThread刷新当前线程
    然后,开始调用DetourDetach函数设置UNHOOK,可连续多次UNHOOK不同的API函数
    最后,使用DetourTransactionCommit提交事务,上一步设置的UNHOOK操作,会立即生效

    其中,DetourDetach传的是实际的API函数地址的指针和代替API函数的替代函数地址。
    至于,Detours具体的操作,我们可以不用理会,只需交给Detours API去实现吧。
    编码实现导入Detours库文件#include "Detours\\detours.h"#pragma comment(lib, "Detours\\detours.lib")
    HOOK APIVOID HookApi_Detours(){ // 恢复之前状态,避免反复拦截 DetourRestoreAfterWith(); // 开始事务, 开始HOOK API DetourTransactionBegin(); // 刷新当前的线程 DetourUpdateThread(GetCurrentThread()); // 保存旧函数的地址 Old_MessageBoxA = ::MessageBoxA; // HOOK API.这里可以连续多次调用DetourAttach, 表明HOOK多个函数 DetourAttach((PVOID *)(&Old_MessageBoxA), New_MessageBoxA); // 提交事务, HOOK API立即生效 DetourTransactionCommit();}
    UNHOOK APIVOID UnhookApi_Detours(){ // 开始事务, 开始UNHOOK API DetourTransactionBegin(); // 刷新当前的线程 DetourUpdateThread(GetCurrentThread()); // UNHOOK API.这可多次调用DetourDetach,表明撤销多个函数HOOK DetourDetach((PVOID *)(&Old_MessageBoxA), New_MessageBoxA); // 提交事务, UNHOOK API立即生效 DetourTransactionCommit();}
    程序测试我们将上述封装好的Detours Hook Api函数写在一个DLL工程中,然后还另外写了一个控制台工程。让控制台工程加载DLL文件,DLL便会在入口点HOOK进程的API函数。当进程调用HOOK掉的API函数是,会直接执行到我们的NEW_API函数。
    控制台工程的 main 函数为:
    int _tmain(int argc, _TCHAR* argv[]){ // HOOK API前弹窗 MyMessage(); // 加载DLL, 执行HOOK API HMODULE hDll = ::LoadLibrary("HookApi_Detours_Dll.dll"); if (NULL == hDll) { printf("LoadLibrary Error!\n"); } // HOOK API后弹窗 MyMessage(); // 卸载DLL ::FreeLibrary(hDll); // UNHOOK API后弹窗 MyMessage(); system("pause"); return 0;}
    测试结果:
    运行控制台.exe程序,首先弹出第一个HOOK MessageBoxA前的消息对话框:

    然后,点击“确定”关闭对话框后,便会执行加载DLL,程序没有加载DLL出错提示,所以加载成功。而且,弹出第二个HOOK MessageBoxA之后的消息对话框,内容已经更改,所以,HOOK API成功:

    然后,点击“确定”关闭对话框后,便会执行卸载DLL,那么DLL卸载处就会调用UNHOOK API,还原API,所以看到弹出的第三个消息对话框,内容是正常的:

    总结基于Detours库实现HOOK API确实很方便,即使你不理解其中的原理,照样可以根据Detours提供的API接口,实现较为完美的API HOOK。
    参考参考自《Windows黑客编程技术详解》一书
    1  留言 2018-12-20 12:14:21

发送私信

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

48
文章数
33
评论数
eject