分离逻辑

在计算机科学中，分离逻辑是Hoare逻辑的延伸，是一种程序推理方式。它是由JohnC.Reynolds,PeterO'Hearn,SaminIshtiaq和HongseokYang借鉴RodBurstall的早期工作而开发的。

分离逻辑的断言语言是捆绑暗示逻辑（BI）的一个特例。O'Hearn的一篇CACM评论文章描述了到2019年初该主题的发展。

分离逻辑有助于推理。操作指针数据结构的程序--包括在存在指针的情况下的信息隐藏；所有权的转移（避免语义框架公理）；以及并发模块之间的虚拟分离（模块化推理）。分离逻辑支持PeterO'Hearn等人描述的发展中的研究领域--局部推理，即程序组件的规范和证明只提到组件使用的那部分内存，而不是系统的整个全局状态。

应用包括自动程序验证（一个算法检查另一个算法的有效性）和软件的自动并行化。断言：运算符和语义分离逻辑断言描述了由存储和堆组成的状态，大致对应于C和Java等常见编程语言中的局部（或堆栈分配）变量和动态分配对象的状态。一个存储空间{displaystyleh}对所有地址都是未定义的。

对所有地址都是未定义的。二进制运算符↦{displaystylemapsto}接收一个地址和一个值，并断言堆正好定义在一个位置上。接受一个地址和一个值，并断言堆正好定义在一个位置，将给定的地址映射到给定的值。

即：。{displaystyleast}（发音为星形或分离连词）。(发音为星形或分离连词)断言，堆可以被分割成两个不相干的部分，其两个参数分别成立。即（发音为魔杖或分离牵连）断言，用满足其第 一个参数的不相交部分扩展堆，结果是满足其第二个参数的堆。即{displaystyles,h'modelsP}。也就是说，如果你是一个人，那么你就有可能是一个人。与经典的连词和暗示运算符共享一些属性。