程序验证(六):纳尔逊-欧朋算法(Nelson-Oppen Procedure)

2024-03-02 14:38

本文主要是介绍程序验证(六):纳尔逊-欧朋算法(Nelson-Oppen Procedure),希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

程序验证(六):纳尔逊-欧朋算法(Nelson-Oppen Procedure)

动机

截至目前,我们学习了一些一阶理论,每一个都是关于某一种数据类型
然而,现实中的公式并不是由单一的理论组成,如:
∀ i . 0 ≤ i ≤ n → a [ i ] ≤ a [ i + 1 ] \forall i.0\le i\le n\to a[i]\le a[i+1] i.0ina[i]a[i+1]
这个公式实际上包含了两个理论:等价与数组
我们需要找到一个方法,将复杂的一阶逻辑公式转化为简单的一阶逻辑公式

一些概念

复合理论

给定 T 1 , T 2 T_1,T_2 T1,T2,且 Σ 1 ∩ Σ 2 = { = } \Sigma_1\cap \Sigma_2 = \{=\} Σ1Σ2={=},那么复合理论 T 1 ∪ T 2 T_1\cup T_2 T1T2有:

  • 符号集: Σ 1 ∪ Σ 2 \Sigma_1 \cup \Sigma_2 Σ1Σ2
  • 公理集: A 1 ∪ A 2 A_1 \cup A_2 A1A2
    纳尔逊-欧朋(Nelson-Oppen)复合方法: T 1 ∪ T 2 T_1\cup T_2 T1T2是可判定的,如果 T 1 T_1 T1 T 2 T_2 T2均满足:
  • 是量词自由的合取的片段(Quantifier-free, conjunctive fragments)
  • 可判定的
  • 稳定无限的(stably-infinite)

稳定无限的理论

一个建立在符号集 Σ \Sigma Σ上的理论 T T T是稳定无限的,如果对于每个量词自由的公式 F F F,只要 F F F T T T-可满足的,存在一个解释,它的大小(cardinality)是无限的
例如这样的一个理论:

  • Σ = { a , b , = } \Sigma =\{a,b,=\} Σ={a,b,=}
  • 公理: ∀ x . x = a ∨ x = b \forall x.x=a\vee x=b x.x=ax=b
    这个理论不是稳定无限的,因为每个解释 ( D , I ) (D,I) (D,I)都有这样的性质: D D D包含至多两个元素,即 ∣ D ∣ ≤ 2 |D|\le 2 D2
    但是大多数我们关心的理论,即 T E , T A , T Z T_E,T_A,T_Z TE,TA,TZ等等,都是稳定无限的

纳尔逊-欧朋算法

概况

输入:由复合理论 T 1 ∪ T 2 T_1\cup T_2 T1T2得到的公式 F F F
输出:等价的公式 F 1 ∧ F 2 F_1\wedge F_2 F1F2,这里:

  • F 1 F_1 F1是一个 T 1 T_1 T1公式
  • F 2 F_2 F2是一个 T 2 T_2 T2公式
    这个算法的功能:
  • F F F净化为 F 1 F_1 F1 F 2 F_2 F2
  • F 1 F_1 F1 F 2 F_2 F2中共享的变量做等价变换

步骤1:变量抽象

理论

目标: F F F中所有的文字或者属于 T 1 T_1 T1,或者属于 T 2 T_2 T2,但不能是二者共有
方法:将以下两个转化方法不断使用,直到不能再用为止:

  • 对于任何一项 f ( … , t , … ) f(\dots ,t,\dots) f(,t,),满足 f ∈ Σ i f\in \Sigma_i fΣi t ∉ Σ i t\not\in \Sigma_i tΣi,将 t t t用一个新的(fresh)变量 w w w替换,并在最后合取上 t = w t=w t=w
  • 对于任一谓词 p ( … , t , … ) p(\dots ,t,\dots) p(,t,),满足 p ∈ Σ i p\in \Sigma_i pΣi t ∉ Σ i t\not\in \Sigma_i tΣi,将 t t t用一个新的(fresh)变量 w w w替换,并在最后合取上 t = w t=w t=w
    结束的时候,我们就可以把 F F F分为 F 1 F_1 F1 F 2 F_2 F2了。
举例

考虑 T E ∪ T Z T_E\cup T_Z TETZ公式 F F F:
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:1xx2f(x)=f(1)f(x)=f(2)

  • T E T_E TE中的非逻辑符是哪些? f , = f,= f,=
  • T Z T_Z TZ中的非逻辑符是哪些? 1 , 2 , ≤ , = 1,2,\le,= 1,2,,=
  • 净化:用 f ( w 1 ) f(w_1) f(w1)代替 f ( 1 ) f(1) f(1),用 f ( w 2 ) f(w_2) f(w2)代替 f ( 2 ) f(2) f(2),加入 w 1 = 1 w_1=1 w1=1 w 2 = 2 w_2=2 w2=2,得到 1 ≤ x ∧ x ≤ 2 ∧ f ( x ) ≠ f ( w 1 ) ∧ f ( x ) ≠ f ( w 2 ) ∧ w 1 = 1 ∧ w 2 = 2 1\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=2 1xx2f(x)=f(w1)f(x)=f(w2)w1=1w2=2
  • F E : f ( x ) ≠ f ( w 1 ) ∧ f ( x ) ≠ f ( w 2 ) F_E:f(x)\ne f(w_1)\wedge f(x)\ne f(w_2) FE:f(x)=f(w1)f(x)=f(w2)
  • F Z : 1 ≤ x ∧ x ≤ 2 ∧ w 1 = 1 ∧ w 2 = 2 F_Z:1\le x\wedge x\le 2\wedge w_1 = 1\wedge w_2 = 2 FZ:1xx2w1=1w2=2

步骤2:猜测与检查(guess and check)

理论

给定 F 1 F_1 F1 F 2 F_2 F2,定义共享变量集 V V V:
V = f r e e ( F 1 ) ∩ f r e e ( F 2 ) V=free(F_1)\cap free(F_2) V=free(F1)free(F2)
E E E V V V上的一个等价关系,由 E E E生成的arrangement α ( V , E ) \alpha (V,E) α(V,E)即为:
α ( V , E ) : ⋀ u , v ∈ V . u E v u = v ∧ ⋀ u , v ∈ V . ¬ ( u E v ) 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,vV.uEvu=vu,vV.¬(uEv)u¬v
公式 F = F 1 ∧ F 2 F=F_1 \wedge F_2 F=F1F2 ( T 1 ∪ T 2 ) (T_1\cup T_2) (T1T2)-可满足的当且仅当存在这样的 α ( V , E ) \alpha (V,E) α(V,E)使得:

  • F 1 ∧ α ( V , E ) F_1\wedge \alpha (V,E) F1α(V,E) T 1 T_1 T1-可满足的
  • F 2 ∧ α ( V , E ) F_2\wedge \alpha (V,E) F2α(V,E) T 2 T_2 T2-可满足的
举例

考虑之前的净化后的两个公式
共享变量: V = { w 1 , w 2 , x } V=\{w_1,w_2,x\} V={w1,w2,x}
猜测并检查 V V V上的等价关系:

  • { { 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\}\} {{w1},{w2,x}}
  • { { w 2 } , { w 1 , x } } \{\{w_2\},\{w_1,x\}\} {{w2},{w1,x}}
  • { { w 1 , w 2 , x } } \{\{w_1,w_2,x\}\} {{w1,w2,x}}
效率问题

这个guess and check的时间复杂度是指数级的,所以不太实用,所以我们换个方法。

步骤2:等价推导(equality propagation)

凸理论(convex theory)

一个理论是凸的(convex),如果它对于每个变量自由的公式 F F F,都满足:

F ⇒ ⋁ i = 1 n u i = v i F\Rightarrow \bigvee ^n_{i=1} u_i =v_i Fi=1nui=vi

F ⇒ u i = v i f o r s o m e i ∈ { 1 , … , n } F\Rightarrow u_i = v_i~for~some~i\in\{1,\dots , n\} Fui=vi for some i{1,,n}
T Z , T A T_Z, T_A TZ,TA不是凸的,但是 T E , T Q T_E,T_Q TE,TQ是凸的。
举例: T Z T_Z TZ不是凸的
例如,考虑这样的量词自由的合取 Σ Z \Sigma_Z ΣZ-公式
F : 1 ≤ z ∧ z ≤ 2 ∧ u = 1 ∧ v = 2 F: 1\le z\wedge z\le 2\wedge u=1\wedge v=2 F:1zz2u=1v=2
那么
F ⇒ z = u ∨ z = v F\Rightarrow z=u\vee z=v Fz=uz=v
但是无法推出
F ⇒ z = u F\Rightarrow z=u Fz=u

F ⇒ z = v F\Rightarrow z=v Fz=v

等价推导

给定 F 1 F_1 F1 F 2 F_2 F2

  • T i ( i = 1 , 2 ) T_i (i=1,2) Ti(i=1,2)报告任何有关共享变量(包括 u u u, v v v)的新推出的等价关系
    • 如果 T i T_i Ti是凸的,令 u = v u=v u=v为新推出的等价关系
    • 如果 T i T_i Ti不是凸的,令 ⋁ i ( u i = v i ) \bigvee_i (u_i = v_i) i(ui=vi)为推出的等价关系的析取
  • 将新推出的等价关系存储到 E E E中( E E E是已经发现的等价关系的集合)
    • 如果 T i T_i Ti是凸的,将 u = v u=v u=v添加到 E E E
    • 如果 T i T_i Ti不是凸的,将搜索过程依据不同的析取 ⋁ i ( u i = v i ) \bigvee_i(u_i = v_i) i(ui=vi)分成不同的分支(通过在 E E E中添加相应的等价关系)
  • 对于每一个分支,将 E E E传播到另一个判定程序(也就是递归进行),重复以上步骤

算法返回:

  • s a t sat sat如果任一分支得到一个完整的arrangement
  • u n s a t unsat unsat如果所有的分支都推出矛盾
  • s a t sat sat如果所有的分支都不能发现新的等价关系
举例
1

考虑 Σ E ∪ Σ Q \Sigma_E\cup \Sigma_Q ΣEΣQ-公式:
F : f ( f ( x ) − f ( y ) ) ≠ f ( z ) ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z F:f(f(x)-f(y))\ne f(z)\wedge x\le y\wedge y+z\le x\wedge 0\le z F:f(f(x)f(y))=f(z)xyy+zx0z
在第一步后, F F F被分为两个公式:

  • F E : 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) FE:f(w)=f(z)u=f(x)v=f(y)
  • F Q : x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z ∧ w = u − v F_Q:x\le y\wedge y+z\le x\wedge 0\le z\wedge w=u-v FQ:xyy+zx0zw=uv
  • V = s h a r e d ( F E , F Q ) = { x , y , z , u , v , w } V=shared(F_E,F_Q)=\{x,y,z,u,v,w\} V=shared(FE,FQ)={x,y,z,u,v,w}

注意, T E T_E TE T Q T_{\mathbb{Q}} TQ都是凸理论
于是
在这里插入图片描述

2

考虑 T E ∪ T Z T_E\cup T_{\mathbb{Z}} TETZ-公式 F F F
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:1xx2f(x)=f(1)f(x)=f(2)
在第一步后, F F F被分为两个公式:

  • F E : f ( x ) ≠ f ( w 1 ) ∧ f ( x ) ≠ f ( w 2 ) F_E:f(x)\ne f(w_1)\wedge f(x)\ne f(w_2) FE:f(x)=f(w1)f(x)=f(w2)
  • F Z : 1 ≤ x ∧ x ≤ 2 ∧ w 1 = 1 ∧ w 2 = 2 F_{\mathbb{Z}} :1\le x\wedge x\le 2\wedge w_1=1\wedge w_2=2 FZ:1xx2w1=1w2=2
  • V = s h a r e d ( F E , F Z ) = { w 1 , w 2 , x } V=shared(F_E,F_{\mathbb{Z}})=\{w_1,w_2,x\} V=shared(FE,FZ)={w1,w2,x}

注意, T E T_E TE是凸的, T Z T_{\mathbb{Z}} TZ不是
于是
在这里插入图片描述

3

考虑 T E ∪ T Z T_E\cup T_{\mathbb{Z}} TETZ-公式 F F F:
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:1xx3f(x)=f(1)f(x)=f(3)f(1)=f(2)
在第一步后, F F F被分为两个公式:

  • F E : f ( x ) ≠ f ( w 1 ) ∧ f ( x ) ≠ f ( w 3 ) ∧ f ( w 1 ) ≠ f ( w 2 ) F_E:f(x)\ne f(w_1)\wedge f(x)\ne f(w_3)\wedge f(w_1)\ne f(w_2) FE:f(x)=f(w1)f(x)=f(w3)f(w1)=f(w2)
  • F Z : 1 ≤ x ∧ x ≤ 3 ∧ w 1 = 1 ∧ w 2 = 2 ∧ w 3 = 3 F_{\mathbb{Z}}:1\le x\wedge x\le 3\wedge w_1=1\wedge w_2=2\wedge w_3=3 FZ:1xx3w1=1w2=2w3=3
  • V = s h a r e d ( F E , F Z ) = { w 1 , w 2 , w 3 , x } V=shared(F_E,F_{\mathbb{Z}})=\{w_1,w_2,w_3,x\} V=shared(FE,FZ)={w1,w2,w3,x}

注意, T E T_E TE是凸的, T Z T_{\mathbb{Z}} TZ不是
于是
在这里插入图片描述

这篇关于程序验证(六):纳尔逊-欧朋算法(Nelson-Oppen Procedure)的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/766453

相关文章

SpringBoot实现MD5加盐算法的示例代码

《SpringBoot实现MD5加盐算法的示例代码》加盐算法是一种用于增强密码安全性的技术,本文主要介绍了SpringBoot实现MD5加盐算法的示例代码,文中通过示例代码介绍的非常详细,对大家的学习... 目录一、什么是加盐算法二、如何实现加盐算法2.1 加盐算法代码实现2.2 注册页面中进行密码加盐2.

Java时间轮调度算法的代码实现

《Java时间轮调度算法的代码实现》时间轮是一种高效的定时调度算法,主要用于管理延时任务或周期性任务,它通过一个环形数组(时间轮)和指针来实现,将大量定时任务分摊到固定的时间槽中,极大地降低了时间复杂... 目录1、简述2、时间轮的原理3. 时间轮的实现步骤3.1 定义时间槽3.2 定义时间轮3.3 使用时

如何通过Golang的container/list实现LRU缓存算法

《如何通过Golang的container/list实现LRU缓存算法》文章介绍了Go语言中container/list包实现的双向链表,并探讨了如何使用链表实现LRU缓存,LRU缓存通过维护一个双向... 目录力扣:146. LRU 缓存主要结构 List 和 Element常用方法1. 初始化链表2.

golang字符串匹配算法解读

《golang字符串匹配算法解读》文章介绍了字符串匹配算法的原理,特别是Knuth-Morris-Pratt(KMP)算法,该算法通过构建模式串的前缀表来减少匹配时的不必要的字符比较,从而提高效率,在... 目录简介KMP实现代码总结简介字符串匹配算法主要用于在一个较长的文本串中查找一个较短的字符串(称为

通俗易懂的Java常见限流算法具体实现

《通俗易懂的Java常见限流算法具体实现》:本文主要介绍Java常见限流算法具体实现的相关资料,包括漏桶算法、令牌桶算法、Nginx限流和Redis+Lua限流的实现原理和具体步骤,并比较了它们的... 目录一、漏桶算法1.漏桶算法的思想和原理2.具体实现二、令牌桶算法1.令牌桶算法流程:2.具体实现2.1

Python中的随机森林算法与实战

《Python中的随机森林算法与实战》本文详细介绍了随机森林算法,包括其原理、实现步骤、分类和回归案例,并讨论了其优点和缺点,通过面向对象编程实现了一个简单的随机森林模型,并应用于鸢尾花分类和波士顿房... 目录1、随机森林算法概述2、随机森林的原理3、实现步骤4、分类案例:使用随机森林预测鸢尾花品种4.1

不懂推荐算法也能设计推荐系统

本文以商业化应用推荐为例,告诉我们不懂推荐算法的产品,也能从产品侧出发, 设计出一款不错的推荐系统。 相信很多新手产品,看到算法二字,多是懵圈的。 什么排序算法、最短路径等都是相对传统的算法(注:传统是指科班出身的产品都会接触过)。但对于推荐算法,多数产品对着网上搜到的资源,都会无从下手。特别当某些推荐算法 和 “AI”扯上关系后,更是加大了理解的难度。 但,不了解推荐算法,就无法做推荐系

康拓展开(hash算法中会用到)

康拓展开是一个全排列到一个自然数的双射(也就是某个全排列与某个自然数一一对应) 公式: X=a[n]*(n-1)!+a[n-1]*(n-2)!+...+a[i]*(i-1)!+...+a[1]*0! 其中,a[i]为整数,并且0<=a[i]<i,1<=i<=n。(a[i]在不同应用中的含义不同); 典型应用: 计算当前排列在所有由小到大全排列中的顺序,也就是说求当前排列是第

csu 1446 Problem J Modified LCS (扩展欧几里得算法的简单应用)

这是一道扩展欧几里得算法的简单应用题,这题是在湖南多校训练赛中队友ac的一道题,在比赛之后请教了队友,然后自己把它a掉 这也是自己独自做扩展欧几里得算法的题目 题意:把题意转变下就变成了:求d1*x - d2*y = f2 - f1的解,很明显用exgcd来解 下面介绍一下exgcd的一些知识点:求ax + by = c的解 一、首先求ax + by = gcd(a,b)的解 这个

综合安防管理平台LntonAIServer视频监控汇聚抖动检测算法优势

LntonAIServer视频质量诊断功能中的抖动检测是一个专门针对视频稳定性进行分析的功能。抖动通常是指视频帧之间的不必要运动,这种运动可能是由于摄像机的移动、传输中的错误或编解码问题导致的。抖动检测对于确保视频内容的平滑性和观看体验至关重要。 优势 1. 提高图像质量 - 清晰度提升:减少抖动,提高图像的清晰度和细节表现力,使得监控画面更加真实可信。 - 细节增强:在低光条件下,抖