摘要: OpenCASCADE-HLR Edge
1 Introduction
用计算机生成三维物体的真实图形，是计算机图形学研究的重要内容。真实图形在仿真模拟、几何造型、广告影视和科学计算可视化等许多领域都有着广泛应用。在用显示设备描述物体的图形时，必须把三维信息经过某种投影变换在二维的显示平面上绘制出来。从三维投影到二维的降维操作，会导致图形的二义性。要消除这类二义性，就必须在绘制时消除被遮挡的不... 阅读全文
摘要: OpenCASCADE 线面求交
eryar@163.com
1 Introduction
OpenCASCADE中几何曲线与曲面求交使用类GeomAPI_IntCS，是对类IntCurveSurface_HInter的简单封装。在IntCurveSurface_HInter中对曲线和曲面求交分为以下几种类型：
PerformConicSurf：二次曲线与曲面求交，其中又分为两类：二次... 阅读全文
摘要: OpenCASCADE二维曲线求交
1 Introduction
OpenCASCADE中对二维曲线求交和三维曲线求交是不同的，三维曲线求交统一使用离散法，二维曲线求交根据曲线类型的不同分种类型进行处理。二维曲线求交中还提供了计算自交的直接接口。在TKGeomAlgo中，主要内容就是拟合、求交算法，理解求交算法的实现原理，达到能阅读和修改源码的状态，能够分析和解决实际遇到的问题，理解OpenC... 阅读全文
摘要: OpenCASCADE曲线上点的反求
eryar@163.com
1 Introduction
曲线可以用代数方程表示，如圆可以用X^2+Y^2=R^2表示，也可以用参数方程X(u)=RCos(u), Y(u)=RSin(u)表示。要判断点是不是在线上，用曲线代数方程可以很直接得出结果，但是使用参数方程就没有那么直接。这也是参数曲线上点的反求问题，参数曲线上点的反求问题应用广泛，如前面所述判... 阅读全文
OpenCASCADE - 曲线自交
1 Introduction
OpenCASCADE为二维曲线提供了求交及自交的类 Geom2dAPI_InterCurveCurve：当传入一个二维几何曲线时可以计算自交self-intersections。但是没有提供直接的三维几何曲线求交的类，也没有直接的计算自交的类。有人同学问OpenCASCADE有没有三维曲线自交的功能，其实理解两个Edge求交算法后，可以自己实现一个自交函数。
2 Self-Intersection
因为OpenCASCADE中两条三维曲线求交的类是IntTools_EdgeEdge，其实现原理是基于包围盒的分割法。基于这个分割递归思想，实现自交也可以参考这个思路。算法的流程为：输入一条要计算自交的边Edge，对边进行离散采样，将采样得到的每段曲线的包围盒生成BVH进行相交检测，将BVH中包围盒相交的两条曲线调用IntTools_EdgeEdge来计算相交。
离散得到的曲线段会比较多，如果用两个循环来检测两两曲线段的相交情况性能差，可以引入BVH提高性能。
3 Test
可以通过插值Interpolate来构造曲线测试，指定几个自交点来构造插值曲线。计算结果如下图所示：
与曲线求交原理类似，都是使用离散的方法，可以思考一下数值算法如何处理。
摘要: OpenCASCADE 曲线求交
eryar@163.com
1 Introduction
OpenCASCADE中提供了二维几何曲线的求交类Geom2dAPI_InterCurveCurve，对应到三维几何只提供了GeomAPI_IntCS, GeomAPI_IntSS，没有提供几何的GeomAPI_IntCC求交类。这些几何求交一般使用的是数值算法，即解方程。对于两条几何曲线P(u1),... 阅读全文
学而不思则罔，思而不学则殆。光看书籍的理论知识，没有实践看不到效果。光看occ的源码，没有理论支撑，不能抓住几何问题的本质。
除了在OpenCASCADE入门指南中推荐的书籍之外，还有一些进阶的书籍，放在那儿有时间就看看，总会有些收获。悟性不足，只有勤能补拙。对于看不懂的，只能用“书读百遍，其义自见”安慰一下自己。
王元 数学大辞典 工具书 方便一些定义，公式，定理的查找。
《计算机辅助几何设计导论》比较全面地介绍了计算机辅助几何设计的发展历史及其主要内容和最新进展，包括现代的T样条曲线曲面。
《样条函数与计算几何》叙述样条函数和计算几何的基本理论和方法，同时，总结了作者几年来在该领域中的研究成果.
《现代数学基础丛书165：散乱数据拟合的模型、方法和理论（第二版）》介绍了多元散乱数据拟合的一般方法，包括多元散乱数据多项式插值、基于三角剖分的插值方法、Boole和与Loons曲面、Sibson方法或自然邻近法、Shepard方法、Kriging方法、薄板样条方法、MQ拟插值法、径向基函数方法、运动*小二乘法、隐函数样条方法、R函数法等。同时还特别介绍了近年来国际上越来越热并在无网格微分方程数值解方面有诸多应用的径向基函数方法及其相关理论。
主要内容包括几何偏微分方程的构造方法、各种微分几何算子的离散化方法及其离散格式的收敛性、几何偏微分方程数值求解的有限差分法、有限元法以及水平集方法，还包括几何偏微分方程在曲面平滑、曲面拼接、N边洞填补、自由曲面设计、曲面重构、曲面恢复、分子曲面构造以及三维实体几何形变中的应用。
摘要: 周知内联是为了消除函数调用的代价，即四大指令序列：调用前序列、被调者起始序列、被调者收尾序列、返回后序列。它们通常对应到体系结构调用者保存/恢复寄存器集合与被调者保存/恢复寄存器集合之约束。这个本质也是内联的前提。试问如果有某体系结构比如S，它任意深度的函数调用代价几乎为零，那么显然内联是没意义没必要的。但是S可能存在吗？我认为不太可能。因为机器的资源比如寄存器集数量与堆栈空间是有限的，且调用需要... 阅读全文
摘要: 谈两个问题：高性能与安全性
先谈高性能：这里指代码实现层面（非数学优化层面），使用寄存器优化，即主密钥/轮密钥、敏感数据比如中间/临时变量必须存于寄存器，明文/密文放在内存（若有够用的寄存器则放寄存器），主密钥用特权寄存器（为支持长期存储，比如调试寄存器、MSR寄存器），轮密钥和敏感数据用通用寄存器。那么怎么做？稳妥快捷的方法是用汇编或内联汇编，手工编排寄存器即构建密钥与敏感数据到寄存器集合... 阅读全文
1. 区间图：用于局部寄存器分配，基本块内的每个活跃范围看作一个区间（最早定义位置+最新使用位置），所有活跃范围构成区间图。区间图是一种不精确的冲突图（因为高估了活跃范围的范围而导致伪冲突，比如认为一个复制操作连接的或两个源相同目标不同的复制操作产生重叠的两个活跃范围冲突，但实际没有冲突），优势在于着色是P（复杂度O(|V|)或O(|E|)）而非NP问题。llvm早期的线性扫描分配器是基于区间图在全局的扩展，比较适用于JIT编译（减少编译时间）
2. 一般图：用于全局寄存器分配，是一种精确的冲突图（由一组定义与一组使用构成的网络）。优势在于努力最小化溢出活跃范围而生成高效执行的代码，但会牺牲编译时间。llvm的greedy寄存器分配是基于一般图的代表。编译器使用的冲突图可能会将机器约束条件比如多寄存器值/调用约定编码进去而存在重复边，导致不满足图论中的简单图定义，故这里采用一般图
3. 弦图：定义详见
https://oi-wiki.org/graph/chord。基于静态单赋值形式名建立的冲突图是弦图。优势在于可以做到最佳着色（复杂度O(|V|+|E|)）而非启发式（基于一般图的全局寄存器分配使用启发式），利于减少寄存器压力。劣势在于必须将指派寄存器后的仍然为静态单赋值代码转换为机器码，而这种转换可能增加寄存器压力，以及插入一些可能非必要的复制操作，若复制操作实现的数据流与ssa phi函数对应，则分配器无法合并这种复制，这将破坏弦图的性质
4. 冲突图拆分：查找其中的团分割即连通子图，移除它划分得到不相交的一些子图，这样一来，各子图可独立着色（有点类似活跃范围拆分）而利于减少寄存器压力，另外实现上还能节省下三角布尔矩阵（用于快速判断两结点是否冲突）的规模
#############################
寄存器分配与图论的染色理论相关。其它的比如常量传播与格代数及不动点相关，循环优化与多面体、矩阵相关。这三方面是我目前看到的编译器所用数学理论
有单向、双向、三向3种认证方式，前两者必须检查时间戳以防重放攻击，单向因为只有一个消息传递，如果仅靠一次性随机数是无法判断消息是否重放。双向有两个消息传递，一来一回，仅靠一次性随机数只能检测到发响应那方的重放。最后者则不必，可仅通过一次性随机数检测自己是否遭遇重放攻击，因为接收第二个消息的那方，通过判断第二个消息中随机数是否等于自己先前已发送第一个消息中的那个，若不等于则为重放，若等于则发第三个确认消息给对方，对方收到并判断确认消息中的随机数是否等于先前它已发送第二个消息中的随机数，若等于则说明第它收到的第一个消息的确是另一方发送的即非重放，否则为重放。因此三向认证可不必同步双方时钟。但正因为不强制检查时间戳而可能导致中间人攻击：假设通信双方为A、B，中间人为C，攻击步骤如下
1. C与B认证时，发送先前已截获的A到B请求消息给B
2. 截获并存储B到A的响应消息x，但不转发，开始与A认证
3. 收到A的请求消息后，解密x取出其中的随机数Rb作为响应给A消息中的随机数，用自己私钥签署整个消息后发给A
4. 收到并转发A的确认消息给B
以上完成后，C就能冒充A与B通信了。一种简单的改进方法是先用对方的公钥加密消息中的随机数，再用自己的私钥签署整个消息。关于网络协议的安全性分析，主流方法是形式化分析，可以借助相关工具来验证找出漏洞
摘要: OpenCASCADE 扫掠曲面
eryar@163.com
1 Introduction
蒙皮（Skinning）就是将一簇截面曲线（section curves）融合在一起生成曲面的过程。蒙皮只是放样（Lofting）的新名词，放样可以追溯到计算机没未诞生的时候，从那时到现在，它一直在造船、汽车和航空工业中被广泛地应用。
扫掠（Sweep）研究的是一条截面曲线沿任意路径曲线扫掠的问题。... 阅读全文
摘要: 布尔数据 面的相交
eryar@163.com
1 Introduction
OpenCASCADE中对面的相交定义如下图所示：
三维空间中两个带有Geometry Surface的面Face，当两个Surface之间的距离小于Face中的容差Tolerance，则认为是相交的。一般两个面之间相交得到的是交线，还有一些情况得到的是交点，如下图所示：
布尔运算中面的相交是相对复杂的... 阅读全文
摘要: 1. 对于RSA，给定大整数n分解的一对素因子p和q，p或q是否素数决定不了安全性，但决定算法的正确性，也就是说p或q不能为合数，而安全性取决于n的位数及p、q的距离，n越大则难于素因子分解（因为素数测试是一个P问题，而因子分解是一个NP问题，其耗时是关于n的指数），|p - q|要大是为抵抗一种特殊因子分解攻击，论证如下：由(p+q)2/4 - n = (p+q)2/4 - pq = (p-q)... 阅读全文
摘要: 布尔数据 边的相交
eryar@163.com
1 Introduction
在OpenCASCADE中对于边的相交分为三类：边与点，边与边，边与面，边与点的相交已经归结为点与边的相交处理了，边的相交主要处理边与边，边与面的相交。边与边、边与面的相交会引入一个新的数据结构-公共部分Common Part，用于保存重叠的公共部分数据。
2 Edge/Edge Interferences
对... 阅读全文
[开源]-OpenCASCADE-IMGUI
1 IMGUI
ImGui 是一个用于C++的用户界面库，跨平台、无依赖，支持OpenGL、DirectX等多种渲染API，是一种即时UI（Immediate Mode User Interface）库，保留模式与即时模式的区别参考保留模式与即时模式。ImGui渲染非常快，但界面上有大量的数据集需要渲染可能会有一些问题，需要使用一些缓存技巧。缓存只是避免数据的更新逻辑耗时太久影响渲染，实际渲染过程不存在瓶颈。
IMGUI很轻量，还支持跨平台，对于小的测试程序IMGUI是理想的GUI。
2 OcctImgui
基于opencascade的glfw sample加入IMGUI，这样就可以开发一些带有GUI的程序。这些程序小巧且能方便跨平台，看上去效果也不错。
现在将OcctImgui开源，开源地址：https://github.com/eryar/OcctImgui
使用Premake来生成解决方案，只需要将premake5.lua中的相关第三方库的路径修改一下，即可以直接编译运行。
3 Next
目前occt的视图作为整个背景，下一步可以做成像CADRays中那样，将occt的视图作为视图的一部分，这样就可以使用IMGUI的Docking功能。
使用IMGUI也可以开发出很Cool的界面，最后放两个基于IMGUI开发的图形界面：
https://github.com/adriengivry/Overload
https://github.com/sasobadovinac/CADRays
https://github.com/MeshInspector/MeshLib
摘要: 布尔数据 BOPDS_DS
eryar@163.com
1 Introduction
在OpenCASCADE中，布尔相关的算子Operator有General Fuse Operator(GFA)，Boolean Operator(BOA)，Section Operator(SA)，Splitter Operator(SPA)，这些布尔算子都共用一套数据结构BOPDS_DS，其中存储了输入... 阅读全文
周知编译原理龙书阐述的基本块指令调度算法，它所使用的空的资源预约表RTD与每个指令的资源预约表RT，可以看作二维矩阵，行表示时钟周期、列表示cpu资源，其定位的元素值1表示占用/预约，0表示空闲/非预约。前者是随周期递增而动态扩大的矩阵，后者是固定尺寸(维数)的矩阵（指令花费周期与每周期预约资源皆已知）。在调度时，按带优先级比如关键路径的拓扑排序基本块内的指令，顺序选取一条指令Inst，计算每前驱发射周期加延迟的结果tmp，取所有tmp的最大值tmax作为Inst的发射周期，再判断处理器资源是否可用，即RTD和RT作与运算，得到一个新矩阵RTN，若RTN为全零矩阵则tmax为Inst的最终发射周期，否则递增tmax再做矩阵与运算，直至得到全零矩阵。最后更新RTD，即RTD与RT作或运算结果存于RTD。重复上述过程直到基本块末尾。
综上不难看出，如果一个基本块很大比如有1000条指令，平均每指令花2个周期，则RTD需要2000个条目，若一条目即矩阵每行占用32字节（256种资源数），则总量约64k。当然这对于现代内存体量来说不算什么，但可以有更好的节省内存的做法：RTD尺寸其实可以相对固定，其上限为基本块中耗费周期最多指令的周期的一个大于1常数因子倍（为兼顾指令并行性），这样一来就要增加当指令完成时（当前指令发射周期大于前一条的终止周期时复位前一条指令的RTD）从发射周期处复位RTD即作一个矩阵反运算的操作，其它步骤对应的矩阵与、矩阵或运算的操作保留不变。另由于RTD固定了尺寸，因此发射周期递增后要取模
【备注】以上是我针对简单机器模型（每种资源数量仅一个，比如整数运算单元1个，内存访问单元1个，浮点运算单元1个）用布尔矩阵作的优化。如果是复杂的超标量机器即每种资源数有多个，那么只需修改如下：布尔矩阵换成整数矩阵；新增一个机器资源可用总数整数矩阵RDA（单列资源数同值），布尔矩阵与运算换成加法并与RDA比较，若大于RDA则递增tmax；布尔矩阵或运算换成加法；布尔矩阵反运算换成减法，RTD减RT存于RTD
摘要: 布尔数据 BOPDS_Iterator
eryar@163.com
1 Introduction
OpenCASCADE中新的布尔工具TKBO相对已经废弃的TKBool代码更规范，更易于理解。与ModelingData和ModelingAlgorithms大的模块组织一样，主要也是数据结构Data Structure+算法Algorithm的组织形式。
其中BOPDS为布尔中的数据结构... 阅读全文
OpenCASCADE GLFW IMGUI
如果从事过C++ Windows客户端开发，大家对MFC、Qt、DuiLib、WxWidgets等各种DirectUI应该有了解，本篇给大家介绍一个超级轻量级的C++开源跨平台图形界面框架ImGUI. ImGUI主要用于游戏行业，所有的控件都需要手绘实现，当然性能也是满满的，毕竟是直接用dx/opengl来实现。ImGUI仓库：https://github.com/ocornut/imgui
ImGUI又称为Dear ImGui，它是与平台无关的C++轻量级跨平台图形界面库，没有任何第三方依赖，可以将ImGUI的源码直接加到项目中使用，也可以编译成dll, ImGUI使用DX或者OpenGL进行界面渲染，对于画面质量要求较高，例如客户端游戏，4k/8k视频播放时，用ImGUI是很好的选择，当然，你得非常熟悉DirectX或者OpenGL，不然就是宝剑在手，屠龙无力。相对于Qt、MFC、DuiLib、SOUI等，ImGUI的拓展性更好，也更轻量级，当然对于开发者的要求也更高.ImGUI没有类似于Qt/MFC这种，可以拖拽控件进行搭建界面，ImGUI的所有控件都必须手写实现。ImGUI的demo基本提供了所有控件、图表等的实现，源码也有，可以对照的学习。在PC端技术选型时，如果公司有音视频、图形图像、4k/8k视频业务，或者一些简单的UI可以考虑一下使用ImGUI，毕竟是直接使用DX/OpenGL来进行绘制渲染，其它功能就直接使用C++来实现。
OpenCASCADE提供了一个GLFW的示例程序，将OpenCASCADE与IMGUI集成起来，对于实现一些简单的小的三维应用程序的UI，有满满的科技感。很多游戏相关的小程序都是使用IMGUI来做界面。
其中OpenCASCAE开源的光线追踪程序CADRays的UI就是用IMGUI实现的：
IMGUI也支持Docking，常见的控件都有，并且也支持跨平台，只依赖OpenGL，生成的程序体积很小。
使用GLFW配置IMGUI可以实现跨平台的界面开发，对于不复杂的应用程序是个不错的选择。
摘要: 几何内核与数学
1 概述
从1950年第一台图形显示器（美国麻省理工大学MIT旋风I号Whirlwind I）的诞生，到1962年MIT林肯实验室的Ivan E. Sutherland发表题为“Sketchpad: 一个人机交互的图形系统”确定计算机图形学作为独立科学分支。经过70多年的发展，计算机图形学中的几何造型技术成了现在的几何内核。
数学是我们从小学、中学到大... 阅读全文
曾因朋友问到监控，致使我探究了kretprobe的实现，想到编译中的尾调用优化，作个小结
1. kretprobe_trampoline_holder该跳转函数无参是必须的或说最好的通用设计，因为替换返回地址是非正常程序流程，即被探测函数的调用者无感知，不存在为跳转函数准备入参。若要设计传参且只读，则不会破坏被探测函数调用者的上下文，但跳转函数内部流程怎么用参数是个问题，这需要一种约定
2. 跳转函数为调用trampoline_handler准备入参，即在栈上构造一个（不完整的）pt_regs，再把它地址即栈顶赋给rdi，rdi是x86_64上传入第一参数使用的寄存器，同时预留一个栈单元存放原返回地址（为什么要预留？因为被探测函数返回时，其调用者存放返回地址的栈空间被释放了，所以得在跳转函数内造一个）。由于trampoline_handler内调到用户自定义handler而传入pt_regs，因此自定义handler内要注意最好别改动pt_regs，否则会破坏被探测函数调用者的上下文
3. 表面看kretprobe的实现流程有点像尾调用优化，但有本质区别。后者中被调尾函数直接释放父调用者的栈帧，就可恢复到父调用者的返回地址；前者不能这样干，因为被探测函数的返回地址被替换了，所以需要一个时地（时机地点）恢复，而这时地正是跳转函数的收尾序列代码，把原来的返回地址放于上述2所讲的预留栈单元，这样最后的ret指令弹出它并跳到原返回地址执行。为保证恢复后正常执行，还得恢复被探测函数调用者的上下文即寄存器信息（无须恢复栈内容，因为上述1讲到了跳转函数是无参的）
有理数域的本原多项式与有限域的本原多项式定义不同，前者不要求不可约（由高斯引理知两个本原多项式的乘积还是本原），后者则必须不可约（确保生成的有限域其每个元素有逆元）。aes基于有限域F{0,1}设计，故使用的模8次多项式不可约P(x)=x^8+x^4+x^3+x+1，但不是本原多项式，因为它的阶是51而非255。有限域次数为8的本原多项式有16个、不可约多项式有30个（由莫比乌斯反演推出），具体多项式影响s盒与列混合操作的实现。不可约加之0的逆元规定为0，保证正确加解密。若0的逆元规定为非0比如x，则导致x有两个逆元，便违反了逆元唯一性，除非s盒不用有限域设计。逆元等于其自身的非0元素只有1，原因可类比模素数二次剩余的求解
1. 若DFA D是用子集构造法从NFA N构造出来的，则L(D)=L(N)
2. 一个语言L被某个DFA接受，当且仅当被某个NFA接受
3. 一个语言L被某个£-NFA接受，当且仅当被某个DFA接受
4. 若对于某个DFA A，L=L(A)，则存在一个正则表达式R使得L=L(R)
5. 每一个用正则表达式定义的语言也可用有穷自动机定义
6. 若通过填表算法不能区分两个状态，则它们是等价的
7. DFA的状态等价性是传递的
8. 若对于DFA每个状态q及与q等价的所有状态组成块，则不同的状态块形成状态集合的划分。也就是说，每个状态恰好属于一个块，同一块中的所有成员都是等价的，从不同块中选择的状态对都不是等价的
9. 根据等价状态划分算法最小化DFA D得到的DFA M是唯一的。也就是说，不存在其它等价于D的DFA N，其状态数比M少
----------------------------------------------------------------------------------------
10. 对于正则表达式，空集是并运算的单位元、连接运算的零元，空串是连接运算的单位元
11. 若L和M都是正则语言，则L和M的并、交、差也是
12. 若L是字母表T上的正则语言，则~L=T*—L也是
13. 若L是正则语言，则L的反转也是
14. 若L是字母表T上的正则语言，h是T上的一个同态，则h(L)也是正则的
15. 若h是字母表A到字母表T的同态，且L是T上的正则语言，则逆同态h^-1(L)也是正则的
因为一个整数p，若检测为合数，这永远是真命题；而检测为素数，这命题只以较大概率成立。 可构造一种NP检测算法，步骤如下：
1. 猜测p（位长度n）的因子列表｛p1,p2,…pi｝，这是非确定的，每个分支耗时O(n)
2. 验证p1*p2*…pi？=p-1，耗时不超过O(n^2)
3. 若各因子乘积等于p-1，则用当前算法递归验证每个因子都是素数
4. 随机选择p最小剩余系内的一个数x，计算x^((p-1)/q) （q遍历上述列表经过步骤3验证过的素因子）是否都不同余于1模p，若是则必有x^(p-1)同余于1模p，则由指数整除p的欧拉数及费马小定理，知p为素数，考虑到有少量的合数也满足费马小定理，故需多次选择x重复验证，选择个数最多为log(p)
分析：本算法涉及的数论定理——设p是奇素数，p-1的所有素因子是q1,q2,…qs，那么g为原根的充要条件是，g^((p-1)/qj)不同余1模p，j=1,2…,s
结论：第3步可以看成递归调用树，每个顶点为待检测整数，其每个子结点为一个因子，则最多n层，每层至多耗时O(n^4)，所以每个路径即检测p是否素数的非确定任一分支中，总耗时O(n^5)。 2002年，印度科学家发现素检测确定性多项式时间算法，于是从NP前进到了P
摘要: 1. 整数r>s>0，(r, s)=1，2∤r+s，x=r^2-s^2, y=2rs, z=r^2+s^2，求证(x, y)=1，(y, z)=1
证明：由2∤r+s（r与s必一奇一偶）知2∤r-s，故2∤r^2-s^2，以及2∤(r+s)(r+s)。又1=(r, s)=(r+s, r)=(r+s, s)=(r+s, rs)。同理得1=(r, s)=(r-s, rs)，故1=((r+s)(r-... 阅读全文
1. 三条定律：交换律、结合律、吸收律（对于半格是幂等律），吸收律包含了幂等律
2. 上下界：交半格每对元素都有唯一最大下界，并半格每对元素都有唯一最小上界，格每对元素都有唯一最大下界和唯一最小上界
3. 格定义一个偏序，偏序有三个性质：自反性、反对称性、传递性
4. 格与偏序的关系：每个格对应一个偏序，但不是所有偏序都对应一个格，要满足每对元素都有唯一最小上界和（或，对于半格）唯一最大下界。如果集合中的任何一个子集（包括空集）均存在最小上界和最大下界，那么对应一个完备格
5. 任何元素有限的格都是完备格，格中的交运算和并运算对于其定义的偏序来说是单调的
6. 格的乘积、和、提升、映射仍然是格，利用这个性质，可以在已有格的基础上增量地构造描述能力更丰富的格，这种技术称为论域精化，是提高程序静态分析精度的重要指导思想之一
【命题1】控制流图G中若a dom n，且b dom n，则a dom b 或b dom a
【证明】设G入口为s，假设结论不成立，即a 不dom b且b 不dom a，或a dom b且b dom a。根据支配结点定义，如果是前者，则从s有全部路径经a（或b）到n但不经过b（或a），这与题设b（或a）dom n矛盾；如果是后者，则从s有全部路径经a，然后经b，再经a，构成了无限循环a->b->a->•••，永远到不了n，这也与题设矛盾。故结论成立
【命题2】控制流图G中若m idom n，则m是唯一的，若d ≠ n 且d dom n ，则d dom m
【证明】设G入口为s，假设不唯一，G中有另一个结点m'且m' idom n，根据支配结点定义，从s经m到n的路径上必有m' dom m，从s经m'到n的路径上必有m dom m'，根据支配关系的反对称性，有m'=m，故唯一。假设d 不dom m，则从s到m的路径上不必然经过d，又m是n的唯一直接支配结点，则从s到n的路径上不必然经过d，即d 不dom n，这与题设矛盾，故d dom m。可以看到用反证法证明后一个结论时，直接支配结点的唯一性很关键
摘要: 【性质】
1. 判定两个完全格L和M能否构成伽罗瓦连接，即抽象化函数α: L—>M是否完全加性的，或具体化函数γ: M—>L是否完全乘性的
2. 构造抽象化函数和具体化函数，即对于一个Galois连接（L, α, γ, M），给定α可通过γ(m) = ⊔{l | α(l) &#... 阅读全文