在計算機科學中，分離邏輯是Hoare邏輯的延伸，是一種程序推理方式。它是由JohnC.Reynolds,PeterO'Hearn,SaminIshtiaq和HongseokYang借鑒RodBurstall的早期工作而開發的。分離邏輯的斷言語言是捆綁暗示邏輯（BI）的一個特例。O'Hearn的一篇CACM評論文章描述了到2019年初該主題的發展。

分離邏輯有助于推理。操作指針數據結構的程序--包括在存在指針的情況下的信息隱藏；所有權的轉移（避免語義框架公理）；以及并發模塊之間的虛擬分離（模塊化推理）。分離邏輯支持PeterO'Hearn等人描述的發展中的研究領域--局部推理，即程序組件的規范和證明只提到組件使用的那部分內存，而不是系統的整個全局狀態。應用包括自動程序驗證（一個算法檢查另一個算法的有效性）和軟件的自動并行化。斷言：運算符和語義分離邏輯斷言描述了由存儲和堆組成的狀態，大致對應于C和Java等常見編程語言中的局部（或堆棧分配）變量和動態分配對象的狀態。一個存儲空間{displaystyleh}對所有地址都是未定義的。對所有地址都是未定義的。二進制運算符?{displaystylemapsto}接收一個地址和一個值，并斷言堆正好定義在一個位置上。接受一個地址和一個值，并斷言堆正好定義在一個位置，將給定的地址映射到給定的值。

即：。{displaystyleast}（發音為星形或分離連詞）。(發音為星形或分離連詞)斷言，堆可以被分割成兩個不相干的部分，其兩個參數分別成立。即。(發音為魔杖或分離牽連)斷言，用滿足其xxx個參數的不相交部分擴展堆，結果是滿足其第二個參數的堆。即，。{displaystyles,h'modelsP},也就是說，如果你是一個人，那么你就有可能是一個人。與經典的連詞和暗示運算符共享一些屬性。