ในวิทยาการคอมพิวเตอร์ตรรกะการแยกส่วน^{[ 1 ]}เป็นส่วนขยายของตรรกะ Hoareซึ่งเป็นวิธีการให้เหตุผลเกี่ยวกับโปรแกรม ได้รับการพัฒนาโดยJohn C. Reynolds , Peter O'Hearn , Samin Ishtiaq และ Hongseok Yang ^{[ 1 ] [ 2 ] [ 3 ] [ 4 ]}โดยอ้างอิงจากงานในช่วงแรกของRod Burstall [ ^{5 ] ภาษา}การยืนยันของตรรกะการแยกส่วนเป็นกรณีพิเศษของตรรกะของการบ่งชี้แบบกลุ่ม (BI) ^{[ 6 ]}บทความ วิจารณ์ CACMโดย O'Hearn ได้บันทึกพัฒนาการในหัวข้อนี้จนถึงต้นปี 2019 ^{[ 7 ]}

ตรรกะการแยกส่วนช่วยให้สามารถให้เหตุผลเกี่ยวกับ:

• โปรแกรมที่จัดการโครงสร้างข้อมูลแบบพอยเตอร์ รวมถึงการซ่อนข้อมูลโดยใช้พอยเตอร์
• "การโอนกรรมสิทธิ์" (การหลีกเลี่ยงสัจพจน์ กรอบความหมาย ) และ
• การแยกเสมือน (การให้เหตุผลแบบโมดูลาร์) ระหว่างโมดูลที่ทำงานพร้อมกัน

ตรรกะการแยกส่วนสนับสนุนสาขาการวิจัยที่กำลังพัฒนาซึ่งปีเตอร์ โอ'เฮิร์นและคนอื่นๆ อธิบายว่าเป็น " การให้เหตุผลเฉพาะส่วน"โดยที่ข้อกำหนดและการพิสูจน์ของส่วนประกอบโปรแกรมจะกล่าวถึงเฉพาะส่วนของหน่วยความจำที่ส่วนประกอบนั้นใช้เท่านั้น ไม่ใช่สถานะโดยรวมทั้งหมดของระบบ การประยุกต์ใช้รวมถึงการตรวจสอบโปรแกรม อัตโนมัติ (ที่อัลกอริทึมตรวจสอบความถูกต้องของอัลกอริทึมอื่น) และการประมวลผลแบบขนาน อัตโนมัติ ของซอฟต์แวร์

ตรรกะการแยกส่วนอธิบาย "สถานะ" ที่ประกอบด้วยสโตร์และฮีปซึ่งโดยคร่าวๆ จะสอดคล้องกับสถานะของ ตัวแปรโล คอล (หรือ ตัวแปร ที่จัดสรรบนสแต็ก )และอ็อบเจ็กต์ที่จัดสรรแบบไดนามิกในภาษาโปรแกรมทั่วไป เช่นCและJavaสโตร์คือฟังก์ชันที่แมปตัวแปรไปยังค่าต่างๆ ฮีปคือฟังก์ชันบางส่วนที่แมปที่อยู่หน่วยความจำไปยังค่าต่างๆ ฮีปสองอันและจะแยกจากกัน (แสดงด้วย) หากโดเมนของพวกมันไม่ทับซ้อนกัน (กล่าวคือ สำหรับทุกที่อยู่หน่วยความจำอย่างน้อยหนึ่งในและจะไม่ถูกกำหนด) ${\displaystyle s}$${\displaystyle h}$${\displaystyle h}$${\displaystyle h'}$${\displaystyle h\,\bot \,h'}$${\displaystyle \ell }$${\displaystyle h(\ell )}$${\displaystyle h'(\ell )}$

ตรรกะนี้อนุญาตให้พิสูจน์คำตัดสินในรูปแบบโดยที่คือที่เก็บข้อมูลคือฮีป และคือข้อความยืนยันเหนือที่เก็บข้อมูลและฮีปที่กำหนด ข้อความยืนยันตรรกะการแยก (แทนด้วย, , ) ประกอบด้วยตัวเชื่อมทางตรรกะบูลีนมาตรฐาน และ นอกจากนี้ยังมี , , , และโดยที่และเป็นนิพจน์ ${\displaystyle s,h\models P}$${\displaystyle s}$${\displaystyle h}$${\displaystyle P}$${\displaystyle P}$${\displaystyle Q}$${\displaystyle R}$${\displaystyle \mathbf {e} \mathbf {m} \mathbf {p} }$${\displaystyle e\mapsto e'}$${\displaystyle P\ast Q}$${\displaystyle P{-\!\!\ast }\,Q}$${\displaystyle e}$${\displaystyle e'}$

• ค่าคงที่นี้ระบุว่าฮีปว่างเปล่า กล่าวคือเมื่อค่าไม่ถูกกำหนดสำหรับทุกแอดเดรส${\displaystyle \mathbf {e} \mathbf {m} \mathbf {p} }$${\displaystyle s,h\models \mathbf {e} \mathbf {m} \mathbf {p} }$${\displaystyle h}$
• ตัวดำเนินการไบนารีรับที่อยู่และค่า และยืนยันว่าฮีปถูกกำหนดไว้ที่ตำแหน่งเดียวเท่านั้น โดยแมปที่อยู่ที่กำหนดให้กับค่าที่กำหนด กล่าวคือเมื่อ(โดยที่แทนค่าของนิพจน์ที่ประเมินใน store ) และจะไม่ถูกกำหนดในกรณีอื่น ๆ${\displaystyle \mapsto }$${\displaystyle s,h\models e\mapsto e'}$${\displaystyle h([\![e]\!]_{s})=[\![e']\!]_{s}}$${\displaystyle [\![e]\!]_{s}}$${\displaystyle e}$${\displaystyle s}$${\displaystyle h}$
• ตัวดำเนินการไบนารี(อ่านว่าสตาร์หรือตัวเชื่อมแยก ) ยืนยันว่าฮีปสามารถแบ่งออกเป็นสอง ส่วน ที่ไม่ทับซ้อนกัน โดยที่อาร์กิวเมนต์ทั้งสองเป็นจริงตามลำดับ กล่าวคือเมื่อมีอยู่จริงที่ทำให้และและและ${\displaystyle \ast }$${\displaystyle s,h\models P\ast Q}$${\displaystyle h_{1},h_{2}}$${\displaystyle h_{1}\,\bot \,h_{2}}$${\displaystyle h=h_{1}\cup h_{2}}$${\displaystyle s,h_{1}\models P}$${\displaystyle s,h_{2}\models Q}$
• ตัวดำเนินการไบนารี(อ่านว่าไม้กายสิทธิ์หรือการบ่งชี้การแยก ) ยืนยันว่า การขยายฮีปด้วยส่วนที่ไม่ซ้ำกันซึ่งตรงตามเงื่อนไขข้อแรก จะส่งผลให้ได้ฮีปที่ตรงตามเงื่อนไขข้อที่สอง กล่าวคือเมื่อ สำหรับทุกฮีปที่ ก็จะเป็นจริงเช่นกัน${\displaystyle -\!\!\ast }$${\displaystyle s,h\models P-\!\!\ast \,Q}$${\displaystyle h'\,\bot \,h}$${\displaystyle s,h'\models P}$${\displaystyle s,h\cup h'\models Q}$

ตัวดำเนินการเหล่านี้มีคุณสมบัติบางอย่างร่วมกับ ตัวดำเนิน การเชื่อมโยงและบ่งชี้ แบบคลาสสิก สามารถนำมาใช้ร่วมกันได้โดยใช้กฎการอนุมานที่คล้ายกับmodus ponens${\displaystyle \ast }$${\displaystyle -\!\!\ast }$

${\displaystyle {\frac {s,h\models P\ast (P-\!\!\ast \,Q)}{s,h\models Q}}}$

และพวกมันก่อให้เกิดการเชื่อมโยงกันกล่าวคือ ก็ต่อเมื่อสำหรับ; กล่าวให้แม่นยำยิ่งขึ้น ตัวดำเนินการเชื่อมโยงคือ และ${\displaystyle s,h\cup h'\models P\ast Q\Rightarrow R}$${\displaystyle s,h\models P\Rightarrow Q-\!\!\ast \,R}$${\displaystyle h\,\bot \,h'}$${\displaystyle \_\ast Q}$${\displaystyle Q-\!\!\ast \,\_}$

ในตรรกะการแยกส่วน (separation logic) ไตรเพิลของ Hoare มีความหมายแตกต่างเล็กน้อยจากในตรรกะของ Hoare (Hoare logic ) ไตรเพิลนี้ระบุว่า หากโปรแกรมทำงานจากสถานะเริ่มต้นที่ตรงตามเงื่อนไขก่อนหน้า (precondition) โปรแกรมจะไม่ทำงานผิดพลาด (เช่น มีพฤติกรรมที่ไม่แน่นอน) และหากโปรแกรมหยุดทำงาน สถานะสุดท้ายจะตรงตามเงื่อนไขหลัง (postcondition ) โดยสรุปแล้ว ในระหว่างการทำงาน โปรแกรมจะเข้าถึงได้เฉพาะตำแหน่งหน่วยความจำที่ได้รับการยืนยันในเงื่อนไขก่อนหน้า หรือตำแหน่งที่โปรแกรมจัดสรรไว้เอง เท่านั้น${\displaystyle \{P\}\ C\ \{Q\}}$${\displaystyle C}$${\displaystyle P}$${\displaystyle Q}$${\displaystyle C}$${\displaystyle C}$

นอกเหนือจากกฎมาตรฐานจากตรรกะของ Hoareแล้ว ตรรกะการแยกส่วนยังสนับสนุนกฎที่สำคัญมากต่อไปนี้:

${\displaystyle {\frac {\{P\}\ C\ \{Q\}}{\{P\ast R\}\ C\ \{Q\ast R\}}}~{\mathsf {mod}}(C)\cap {\mathsf {fv}}(R)=\emptyset }$

นี่คือสิ่งที่เรียกว่ากฎเฟรม (ตั้งชื่อตามปัญหาเฟรม ) และช่วยให้สามารถใช้เหตุผลในระดับท้องถิ่นได้ กฎนี้กล่าวว่าโปรแกรมที่ทำงานได้อย่างปลอดภัยในสถานะเล็กๆ (ที่ตรงตามเงื่อนไข) สามารถทำงานได้ในสถานะที่ใหญ่กว่า (ที่ตรงตามเงื่อนไข) และการทำงานของโปรแกรมจะไม่ส่งผลกระทบต่อส่วนเพิ่มเติมของสถานะ (และจะยังคงเป็นจริงในเงื่อนไขหลังการทำงาน) เงื่อนไขด้านข้างบังคับใช้สิ่งนี้โดยระบุว่าตัวแปรใดๆ ที่ถูกแก้ไขโดย จะไม่ปรากฏเป็นตัวแปรอิสระใน กล่าวคือ ไม่มีตัวแปรใดๆ อยู่ในชุด 'ตัวแปรอิสระ' ของ${\displaystyle P}$${\displaystyle P\ast R}$${\displaystyle R}$${\displaystyle C}$${\displaystyle R}$${\displaystyle {\mathsf {fv}}}$${\displaystyle R}$

โดยทั่วไปแล้ว ตรรกะการแยกสามารถมองได้ว่าเป็นวิธีการให้เหตุผลเกี่ยวกับพีชคณิตการแยกพีชคณิตการแยกอาจถูกกำหนดได้หลายวิธี แต่มักจะนำเสนอเป็นโมโนอิดแบบสลับที่ตัดทอนได้บางส่วน^{[ 8 ]}เป็นรูปธรรมมากขึ้น มันคือเซตAการดำเนินการไบนารีบางส่วนและค่าคงที่uที่สอดคล้องกับเอกลักษณ์ต่อไปนี้ โดยในกฎสามข้อแรก หากด้านใดด้านหนึ่งของสมการถูกกำหนด ด้านทั้งหมดก็จะถูกกำหนดเช่นกัน: ${\displaystyle \oplus :A\times A\rightharpoonup A}$

• คุณสมบัติการสลับที่: สำหรับทุกx , yและz ,${\displaystyle (x\oplus y)\oplus z=x\oplus (y\oplus z)}$
• คุณสมบัติการสลับที่: สำหรับทุกxและy ,${\displaystyle x\oplus y=y\oplus x}$
• เอกลักษณ์: สำหรับทุกx ,${\displaystyle x\oplus u=x=u\oplus x}$
• หลักการตัดทอน: สำหรับทุกx , yและzถ้าแล้ว${\displaystyle x\oplus z=y\oplus z}$${\displaystyle x=y}$

สามารถแสดงได้ว่าการนำเสนอสแต็กและฮีปข้างต้นทำให้เกิดพีชคณิตการแยก: ให้Aเป็นเซตของฮีปทั้งหมด การดำเนินการไบนารีเป็นการรวมกันของฮีปสองฮีป (กำหนดเฉพาะเมื่อฮีปไม่ทับซ้อนกัน) และuเป็นฮีปว่าง ในบางคำจำกัดความ การตัดทอนจะถูกละเว้น แต่สิ่งนี้ไม่จำเป็นต้องก่อให้เกิดปัญหา^{[ 9 ]}${\displaystyle \oplus }$

ข้อความยืนยันจำนวนมากสามารถกำหนดความหมายได้โดยใช้พีชคณิตการแยกส่วนเพียงอย่างเดียว โดยเฉพาะอย่างยิ่ง สำหรับข้อความยืนยันPเราสามารถกำหนดเซตย่อยบางส่วนของA ให้กับ ข้อความยืนยันนั้น ได้ โดยใช้สัญลักษณ์ ดังต่อไปนี้: ${\displaystyle [\![P]\!]}$

• ${\displaystyle [\![false]\!]=\emptyset }$
• ${\displaystyle [\![P\Rightarrow Q]\!]=\{h|h\in [\![P]\!]\Rightarrow h\in [\![Q]\!]\}}$
• ${\displaystyle [\![\forall xP]\!]=\{h|\forall vh\in [\![P[x:=v]]\!]\}}$
• ${\displaystyle [\![\mathbf {e} \mathbf {m} \mathbf {p} ]\!]=\{u\}}$
• ${\displaystyle [\![P\ast Q]\!]=\{h_{1}\oplus h_{2}|h_{1}\in [\![P]\!]\wedge h_{2}\in [\![Q]\!]\}}$
• ${\displaystyle [\![P{-\!\!\ast }\,Q]\!]=\{h|\forall h'.h'\,\bot \,h\wedge h'\in [\![P]\!]\Rightarrow h\oplus h'\in [\![Q]\!]\}}$

กฎสำหรับ, , และถูกละเว้น แต่สามารถอนุมานได้ง่ายจากข้างต้น ในขณะที่ความหมายของ นั้นกำหนดโดยพีชคณิตการแยกส่วนที่กล่าวถึง ${\displaystyle \land }$${\displaystyle \vee }$${\displaystyle \neg }$${\displaystyle \exists }$${\displaystyle e\mapsto e'}$

ตรรกศาสตร์การแยกส่วนนำไปสู่การพิสูจน์ที่ง่ายสำหรับการจัดการตัวชี้สำหรับโครงสร้างข้อมูลที่แสดงรูปแบบการแบ่งปันที่สม่ำเสมอซึ่งสามารถอธิบายได้ง่ายโดยใช้การเชื่อมโยงแบบแยกส่วน ตัวอย่างเช่น รายการเชื่อมโยงเดี่ยวและคู่ และต้นไม้ประเภทต่างๆ กราฟและ DAG และโครงสร้างข้อมูลอื่นๆ ที่มีการแบ่งปันทั่วไปนั้นยากกว่าสำหรับการพิสูจน์ทั้งแบบเป็นทางการและไม่เป็นทางการ อย่างไรก็ตาม ตรรกศาสตร์การแยกส่วนได้รับการประยุกต์ใช้ประสบความสำเร็จในการให้เหตุผลเกี่ยวกับโปรแกรมที่มีการแบ่งปันทั่วไป

ในบทความ POPL'01 ของพวกเขา^{[ 3 ]} O'Hearn และ Ishtiaq อธิบายว่าตัวเชื่อมไม้กายสิทธิ์สามารถใช้ในการให้เหตุผลในกรณีที่มีการแบ่งปัน อย่างน้อยก็ในทางทฤษฎี ตัวอย่างเช่น ในสามสิ่ง ${\displaystyle {-\!\!*}}$

${\displaystyle \{(x\mapsto -)\ast ((x\mapsto 42){-\!\!*}P)\}\ [x]=42\ \{P\}}$

เราได้รับเงื่อนไขเบื้องต้นที่อ่อนที่สุดสำหรับข้อความที่เปลี่ยนแปลงฮีปที่ตำแหน่งและสิ่งนี้ใช้ได้กับเงื่อนไขภายหลังใดๆ ไม่ใช่เฉพาะเงื่อนไขที่จัดวางอย่างเรียบร้อยโดยใช้การเชื่อมโยงแบบแยกเท่านั้น แนวคิดนี้ได้รับการพัฒนาไปไกลกว่านั้นโดย Yang ซึ่งเคยให้เหตุผลเฉพาะที่เกี่ยวกับการกลายพันธุ์ในอัลกอริทึมการทำเครื่องหมายกราฟ Schorr-Waite แบบคลาสสิก[ 10 ^{]ในที่สุด}หนึ่งในงานล่าสุดในทิศทางนี้คืองานของ Hobor และ Villard ^{[ 11 ]}ซึ่งไม่เพียงแต่ใช้แต่ยังใช้ตัวเชื่อม ซึ่งถูกเรียกว่าการเชื่อมโยงแบบทับซ้อนหรือ sepish ^{[ 12 ]}และสามารถใช้เพื่ออธิบายโครงสร้างข้อมูลที่ทับซ้อนกันได้: ถือฮีปเมื่อ และถือสำหรับซับฮีปและยูเนียนของมันคือแต่อาจมีส่วนที่ไม่ว่างเปล่าร่วมกัน ในเชิงนามธรรม สามารถมองได้ว่าเป็นเวอร์ชันของตัวเชื่อมฟิวชั่นของตรรกะความเกี่ยวข้อง ${\displaystyle x}$${\displaystyle {-\!\!*}}$${\displaystyle {-\!\!*}}$${\displaystyle \cup \,\!\!\!\!\!*}$${\displaystyle P\cup \!\!\!\!\!*Q}$${\displaystyle h}$${\displaystyle P}$${\displaystyle Q}$${\displaystyle h_{P}}$${\displaystyle h_{Q}}$${\displaystyle h}$${\displaystyle h_{P}\cap h_{Q}}$${\displaystyle P\cup \!\!\!\!\!*Q}$

ตรรกะการแยกแบบพร้อมกัน (CSL) ซึ่งเป็นตรรกะการแยกเวอร์ชันสำหรับโปรแกรมแบบพร้อมกัน ได้รับการเสนอครั้งแรกโดย^Peter O'Hearn [ ^{13 ]} โดยใช้กฎการพิสูจน์

${\displaystyle {\frac {\{P_{1}\}C_{1}\{Q_{1}\}\quad \{P_{2}\}C_{2}\{Q_{2}\}}{\{P_{1}*P_{2}\}C_{1}\parallel C_{2}\{Q_{1}*Q_{2}\}}}}$

ซึ่งช่วยให้สามารถให้เหตุผลอย่างอิสระเกี่ยวกับเธรดที่เข้าถึงพื้นที่จัดเก็บแยกต่างหาก กฎการพิสูจน์ของ O'Hearn ได้ปรับวิธีการในยุคแรกของTony Hoareมาใช้กับการให้เหตุผลเกี่ยวกับการทำงานพร้อมกัน^{[ 14 ]} โดยแทนที่การใช้ข้อจำกัดขอบเขตเพื่อให้แน่ใจว่ามีการแยกออกจากกันด้วยการให้เหตุผลในตรรกะการแยก นอกจากจะขยายวิธีการของ Hoare ไปใช้ในกรณีที่มีตัวชี้ที่จัดสรรในฮีปแล้ว O'Hearn ยังแสดงให้เห็นว่าการให้เหตุผลในตรรกะการแยกพร้อมกันสามารถติดตามการถ่ายโอนความเป็นเจ้าของแบบไดนามิกของส่วนฮีประหว่างกระบวนการได้ ตัวอย่างในเอกสารประกอบด้วยบัฟเฟอร์การถ่ายโอนตัวชี้ และตัวจัดการหน่วยความจำ

โอ'เฮิร์นได้ แสดงความคิดเห็นเกี่ยวกับงานวิจัยคลาสสิกยุคแรกๆ เกี่ยวกับการปราศจากการแทรกแซงโดยซูซาน โอวิคกี้และเดวิด กรีส์ว่า การตรวจสอบอย่างชัดเจนว่าไม่มีการแทรกแซงนั้นไม่จำเป็น เพราะระบบของเขาได้ตัดความเป็นไปได้ของการแทรกแซงออกไปโดยปริยาย ด้วยลักษณะของวิธีการสร้างบทพิสูจน์นั่นเอง

แบบจำลองสำหรับตรรกะการแยกพร้อมกันได้รับการนำเสนอครั้งแรกโดย Stephen Brookes ในบทความประกอบของ O'Hearn ^{[ 15 ]}ความถูกต้องของตรรกะเป็นปัญหาที่ยาก และในความเป็นจริง ตัวอย่างค้านของ John Reynolds ได้แสดงให้เห็นถึงความไม่ถูกต้องของตรรกะเวอร์ชันก่อนหน้าที่ยังไม่ได้ตีพิมพ์ ประเด็นที่ยกขึ้นโดยตัวอย่างของ Reynolds ได้รับการอธิบายโดยย่อในบทความของ O'Hearn และโดยละเอียดมากขึ้นในบทความของ Brookes

ในตอนแรกดูเหมือนว่า CSL จะเหมาะสมกับสิ่งที่ Dijkstra เรียกว่ากระบวนการที่เชื่อมต่อกันอย่างหลวมๆ^{[ 16 ]}แต่อาจจะไม่เหมาะกับอัลกอริธึมแบบขนานที่มีความละเอียดสูงที่มีการรบกวนอย่างมีนัยสำคัญ อย่างไรก็ตาม ค่อยๆ ตระหนักว่าแนวทางพื้นฐานของ CSL มีประสิทธิภาพมากกว่าที่คิดไว้ในตอนแรก หากใช้โมเดลที่ไม่เป็นมาตรฐานของตัวเชื่อมตรรกะและแม้แต่สามเท่าของ Hoare

ด้วยการเลือกพีชคณิตการแยกที่เหมาะสม พบว่ากฎการพิสูจน์ของตรรกะการแยกแบบขนานในเวอร์ชันนามธรรมสามารถใช้ในการให้เหตุผลเกี่ยวกับกระบวนการขนานที่รบกวนกันได้ ตัวอย่างเช่น โดยการเข้ารหัสเทคนิคการรับประกันความน่าเชื่อถือซึ่งเดิมทีเสนอให้ใช้ในการให้เหตุผลเกี่ยวกับการรบกวน^{[ 17 ]}ในงานนี้ องค์ประกอบของแบบจำลองไม่ได้ถูกพิจารณาว่าเป็นทรัพยากร แต่เป็น "มุมมอง" ของสถานะโปรแกรม และการตีความที่ไม่เป็นมาตรฐานของ Hoare triples จะมาพร้อมกับการอ่านเงื่อนไขก่อนและหลังที่ไม่เป็นมาตรฐาน สุดท้าย หลักการแบบ CSL ได้ถูกนำมาใช้ในการประกอบการให้เหตุผลเกี่ยวกับประวัติของโปรแกรมแทนที่จะเป็นสถานะของโปรแกรม เพื่อให้เทคนิคแบบโมดูลาร์สำหรับการให้เหตุผลเกี่ยวกับอัลกอริทึมขนานแบบละเอียด^{[ 18 ]}

เวอร์ชันของ CSL ได้ถูกรวมไว้ในเครื่องมือตรวจสอบแบบโต้ตอบและกึ่งอัตโนมัติ (หรือ "ระหว่างกลาง") จำนวนมาก ดังที่อธิบายไว้ในส่วนถัดไป ความพยายามในการตรวจสอบที่สำคัญอย่างยิ่งคือการตรวจสอบเคอร์เนล μC/OS-II ที่กล่าวถึงในนั้น แต่ถึงแม้จะมีความคืบหน้า^{[ 19 ]}จนถึงปัจจุบัน การให้เหตุผลแบบ CSL ได้ถูกรวมไว้ในเครื่องมือเพียงไม่กี่ชนิดในหมวดหมู่การวิเคราะห์โปรแกรมอัตโนมัติ (และไม่มีเครื่องมือใดที่กล่าวถึงในส่วนถัดไป)

O'Hearn และ Brookes เป็นผู้รับรางวัล Gödel Prize ประจำปี 2016 ร่วมกัน จากการคิดค้น Concurrent Separation Logic ^{[ 20 ]}

ตรรกะการแยกแบบขนานธรรมดาสามารถอธิบายการถ่ายโอนความเป็นเจ้าของได้ โดยที่เธรดหนึ่งอาจมอบการควบคุมตำแหน่งฮีปแต่ละตำแหน่งให้กับเธรดอื่นได้อย่างสมบูรณ์ แต่สิ่งนี้ไม่เพียงพอที่จะให้เหตุผลเกี่ยวกับโปรแกรมแบบขนานจำนวนมาก โดยเฉพาะอย่างยิ่ง เซลล์ฮีปแต่ละเซลล์อาจถูกใช้ร่วมกันโดยหลายเธรด ตราบใดที่แต่ละเธรดอ่านจากเซลล์เท่านั้นและไม่ได้เขียนลงไป หรืออีกทางหนึ่ง เซลล์นั้นอาจถูกเขียนลงไปได้ ตราบใดที่มีเพียงเธรดเดียวเท่านั้นที่สามารถทำการเขียนได้^{[ 21 ]}

สามารถทำได้โดยการกำหนดสิทธิ์แบบเศษส่วนให้กับแต่ละข้อความยืนยันเช่น π = 1 เมื่อπ = 1 เธรดจะมีสิทธิ์ครอบครองเซลล์ฮีปอย่างสมบูรณ์และสามารถเขียนลงในเซลล์นั้นได้: ${\displaystyle \mapsto }$${\displaystyle \pi \in (0,1]}$${\displaystyle e\,{\overset {\pi }{\mapsto }}\,e'}$

${\displaystyle \{x\,{\overset {1}{\mapsto }}\,\_\}\,[x]:=a\,\{x\,{\overset {1}{\mapsto }}\,a\}}$

เมื่อπ < 1 เธรดจะมีสิทธิ์เข้าถึงแบบใช้ร่วมกันเท่านั้น และดังนั้นจึงสามารถอ่านได้เพียงอย่างเดียว:

${\displaystyle \{x\,{\overset {\pi }{\mapsto }}\,v\}\,a:=[x]\,\{x\,{\overset {\pi }{\mapsto }}\,v\ast a=v\}}$

ที่สำคัญคือ สิทธิ์การเข้าถึงสามารถแบ่งได้ไม่จำกัด ทำให้เธรดจำนวนมากสามารถอ่านข้อมูลจากตำแหน่งเดียวกันได้ (โดยสิทธิ์การเข้าถึงแบบเศษส่วนจะคอยติดตามว่าเมื่อใดที่จำนวนเธรดลดลงเหลือหนึ่งอีกครั้ง):

${\displaystyle x\,{\overset {\pi _{1}+\pi _{2}}{\mapsto }}\,v\iff x\,{\overset {\pi _{1}}{\mapsto }}\,v\ast x\,{\overset {\pi _{2}}{\mapsto }}\,v}$

โปรดทราบว่าค่าสิทธิ์ที่น้อยกว่าหนึ่งนั้นไม่มีความสำคัญและจำเป็นสำหรับการติดตามเท่านั้น โปรแกรมไม่ควรใส่ใจว่าค่าสิทธิ์ใด ๆ จะเป็น 0.1 หรือ 0.9 เนื่องจากสามารถอ่านข้อมูลจากเซลล์ฮีปได้เหมือนกัน

เพื่อให้ฮีปสองฮีปสามารถพิจารณาตำแหน่งหน่วยความจำเดียวกันได้ จำเป็นต้องมีการปรับเปลี่ยนคำจำกัดความของฮีปและการแยกออกจากกันของฮีปเหล่านั้น โดยเฉพาะอย่างยิ่ง ตำแหน่งในฮีปแต่ละตำแหน่งจะได้รับสิทธิ์แบบเศษส่วน (และในเชิงความหมายหมายความว่า ในฮีปhตำแหน่งeมีค่าเป็นe'โดยมีสิทธิ์π ) และฮีปสองฮีปจะแยกออกจากกันหากสำหรับทุกตำแหน่งที่อยู่ในทั้งสองฮีป ค่าของตำแหน่งเหล่านั้นเท่ากัน และผลรวมของสิทธิ์แบบเศษส่วนไม่เกินหนึ่ง การดำเนินการรวมฮีปสองฮีปจะรวมสิทธิ์สำหรับตำแหน่งที่ซ้ำกันเหล่านั้นเข้าด้วยกัน ${\displaystyle s,h\vdash e\,{\overset {\pi }{\mapsto }}\,e'}$

เครื่องมือสำหรับการวิเคราะห์โปรแกรมมีหลากหลายระดับ ตั้งแต่เครื่องมือวิเคราะห์โปรแกรมอัตโนมัติเต็มรูปแบบ ซึ่งไม่ต้องการการป้อนข้อมูลจากผู้ใช้ ไปจนถึงเครื่องมือแบบโต้ตอบที่มนุษย์มีส่วนร่วมอย่างใกล้ชิดในกระบวนการพิสูจน์ เครื่องมือดังกล่าวได้รับการพัฒนาขึ้นมากมาย รายการต่อไปนี้ประกอบด้วยตัวอย่างบางส่วนในแต่ละประเภท

• การวิเคราะห์โปรแกรมอัตโนมัติเครื่องมือเหล่านี้มักจะมองหาข้อผิดพลาดในกลุ่มที่จำกัด (เช่น ข้อผิดพลาดด้านความปลอดภัยของหน่วยความจำ) หรือพยายามพิสูจน์ว่าไม่มีข้อผิดพลาดเหล่านั้น แต่ไม่สามารถพิสูจน์ความถูกต้องสมบูรณ์ได้
  • ตัวอย่างปัจจุบันคือFacebook Inferซึ่งเป็นเครื่องมือวิเคราะห์แบบคงที่สำหรับ Java, C และObjective-C โดยอิงตามตรรกะการแยกและการอนุมานแบบสองทาง^{[ 22 ]}ในปี 2015 Infer พบข้อบกพร่องหลายร้อยรายการต่อเดือนและได้รับการแก้ไขโดยนักพัฒนาซอฟต์แวร์ก่อนที่จะส่งไปยังแอปมือถือของ Facebook ^{[ 23 ]}
  • ตัวอย่างอื่นๆ ได้แก่SpaceInvader (หนึ่งในเครื่องมือวิเคราะห์ SL รุ่นแรกๆ), Predator (ซึ่งได้รับรางวัลจากการแข่งขันตรวจสอบหลายรายการ), MemCAD (ซึ่งผสมผสานคุณสมบัติของรูปร่างและตัวเลข) และSLAyer (จาก Microsoft Research ซึ่งมุ่งเน้นไปที่โครงสร้างข้อมูลที่พบในไดรเวอร์อุปกรณ์)
• การ พิสูจน์แบบโต้ตอบการพิสูจน์ได้ดำเนินการโดยใช้การฝังตรรกะการแยกส่วน (Separation Logic) ลงในโปรแกรมพิสูจน์ทฤษฎีบทแบบโต้ตอบ เช่นRocq (เดิมชื่อCoq ) และHOL (proof assistant)เมื่อเปรียบเทียบกับงานวิเคราะห์โปรแกรม เครื่องมือเหล่านี้ต้องการความพยายามจากมนุษย์มากกว่า แต่สามารถพิสูจน์คุณสมบัติที่ลึกซึ้งกว่า จนถึงความถูกต้องเชิงฟังก์ชัน
  • หลักฐานของระบบไฟล์ FSCQ ^{[ 24 ]}ซึ่งข้อกำหนดรวมถึงพฤติกรรมภายใต้การขัดข้องเช่นเดียวกับการทำงานปกติ งานนี้ได้รับรางวัลบทความยอดเยี่ยมในงาน Symposium on Operating System Principles ปี 2015
  • การตรวจสอบความถูกต้องของส่วนใหญ่ของ ระบบประเภทข้อมูลของ Rustและไลบรารีมาตรฐานบางส่วนในโครงการ RustBeltโดยใช้ เฟรมเวิร์ก Irisสำหรับการแยกตรรกะใน Rocq
  • การตรวจสอบการใช้งาน OpenSSL ของอัลกอริธึมการตรวจสอบความถูกต้องทางการเข้ารหัส^{[ 25 ]}โดยใช้C ที่ตรวจสอบได้
  • การตรวจสอบโมดูลหลักของเคอร์เนลระบบปฏิบัติการเชิงพาณิชย์ เคอร์เนล μC/OS-II ซึ่งเป็น เคอร์เนลแบบ พรีเอ็มทีฟเชิง พาณิชย์ตัวแรก ที่ได้รับการตรวจสอบ^{[ 26 ]}
  • ตัวอย่างอื่นๆ ได้แก่ ไลบรารี Ynot ^{[ 27 ]}สำหรับ Rocq; การฝัง Holfootของ Smallfoot ใน HOL; ตรรกะการแยกพร้อมกันแบบละเอียดและBedrock (ไลบรารี Rocq สำหรับการเขียนโปรแกรมระดับต่ำ)
• อยู่ระหว่างกลางเครื่องมือหลายอย่างต้องการการแทรกแซงจากผู้ใช้มากกว่าการวิเคราะห์โปรแกรม กล่าวคือ เครื่องมือเหล่านั้นคาดหวังให้ผู้ใช้ป้อนข้อความยืนยัน เช่น ข้อกำหนดก่อน/หลังการทำงานของฟังก์ชัน หรือเงื่อนไขคงที่ของลูป แต่หลังจากที่ป้อนข้อมูลแล้ว เครื่องมือเหล่านั้นจะพยายามทำงานโดยอัตโนมัติอย่างสมบูรณ์หรือเกือบสมบูรณ์ วิธีการตรวจสอบแบบนี้มีที่มาจากผลงานคลาสสิกในทศวรรษ 1970 เช่น ตัวตรวจสอบของ J King และตัวตรวจสอบ Stanford Pascal รูปแบบของตัวตรวจสอบนี้เพิ่งถูกเรียกว่าการตรวจสอบแบบแอคทีฟอัตโนมัติซึ่งเป็นคำที่ตั้งใจจะสื่อถึงวิธีการโต้ตอบกับตัวตรวจสอบผ่านลูปการตรวจสอบและยืนยัน คล้ายกับการโต้ตอบระหว่างโปรแกรมเมอร์และตัวตรวจสอบประเภท
  • Smallfoot ซึ่ง เป็นตัวตรวจสอบตรรกะการแยกส่วนตัวแรกสุดจัดอยู่ในหมวดหมู่กึ่งกลางนี้ มันต้องการให้ผู้ใช้ป้อนข้อกำหนดก่อน/หลัง เงื่อนไขคงที่ของลูป และเงื่อนไขคงที่ของทรัพยากรสำหรับล็อก มันแนะนำวิธีการดำเนินการเชิงสัญลักษณ์ รวมถึงวิธีการอนุมานสัจพจน์ของเฟรมโดยอัตโนมัติ Smallfoot ยังรวมถึงตรรกะการแยกส่วนแบบพร้อมกันด้วย
  • SmallfootRGเป็นตัวตรวจสอบสำหรับการผสมผสานระหว่างตรรกะการแยกส่วนและวิธีการพึ่งพา/รับประกันแบบคลาสสิกสำหรับโปรแกรมแบบขนาน
  • Heap Hopใช้ตรรกะการแยกส่วนสำหรับการส่งข้อความ โดยยึดตามแนวคิดในระบบปฏิบัติการ Singularity
  • VeriFastเป็นเครื่องมือขั้นสูงที่อยู่ในหมวดหมู่ระหว่างกลาง สามารถพิสูจน์ได้ว่าใช้งานได้กับงานหลากหลาย ตั้งแต่รูปแบบการเขียนโปรแกรมเชิงวัตถุ ไปจนถึงอัลกอริทึมที่มีการทำงานพร้อมกันสูง และโปรแกรมระบบ
  • Viperเป็นโครงสร้างพื้นฐานการตรวจสอบอัตโนมัติที่ทันสมัยสำหรับการให้เหตุผลตามสิทธิ์ โดยส่วนใหญ่ประกอบด้วยภาษาโปรแกรมและแบ็กเอนด์การตรวจสอบสองส่วน ส่วนหนึ่งใช้การดำเนินการเชิงสัญลักษณ์ และอีกส่วนหนึ่งใช้การสร้างเงื่อนไขการตรวจสอบ (VCG) ^{[ 28 ]}บนพื้นฐานของโครงสร้างพื้นฐาน Viper ได้มีการพัฒนาฟรอนต์เอนด์สำหรับภาษาโปรแกรมต่างๆ มากมาย เช่นGobraสำหรับ Go, Naginiสำหรับ Python, Prustiสำหรับ Rust และVerCorsสำหรับ C, Java, OpenCL และ OpenMP ฟรอนต์เอนด์เหล่านี้จะแปลภาษาโปรแกรมฟรอนต์เอนด์เป็น Viper จากนั้นใช้แบ็กเอนด์การตรวจสอบของ Viper เพื่อพิสูจน์ความถูกต้องของโปรแกรมอินพุต
  • ภาษาการเขียนโปรแกรม Mezzoและประเภทการแยกของเหลวแบบอะซิงโครนัส (Asynchronous Liquid Separation Types)มีแนวคิดที่เกี่ยวข้องกับ CSL ในระบบประเภทสำหรับภาษาการเขียนโปรแกรม แนวคิดในการรวมการแยกไว้ในระบบประเภทนั้นมีตัวอย่างมาก่อนหน้านี้ในประเภทนามแฝง (Alias ​​Types)และการควบคุมการแทรกแซงทางไวยากรณ์ (Syntactic Control of Interference )

ความแตกต่างระหว่างตัวตรวจสอบแบบโต้ตอบและแบบกึ่งกลางนั้นไม่ชัดเจนนัก ตัวอย่างเช่น Bedrock มุ่งเน้นที่ระดับการทำงานอัตโนมัติสูง ในสิ่งที่เรียกว่าการตรวจสอบอัตโนมัติเป็นส่วนใหญ่ ในขณะที่ Verifast บางครั้งต้องการคำอธิบายประกอบที่คล้ายกับกลยุทธ์ (โปรแกรมขนาดเล็ก) ที่ใช้ในตัวตรวจสอบแบบโต้ตอบ

ปัญหาความพึงพอใจสำหรับเศษส่วนตรรกะการแยกประเภทแบบหลายลำดับที่ไม่มีตัวบ่งปริมาณซึ่งกำหนดพารามิเตอร์ตามชนิดของตำแหน่งและข้อมูลสามารถแสดงได้ว่า สมบูรณ์ แบบPSPACE ^{[ 29 ]}อัลกอริทึมสำหรับการแก้ปัญหาเศษส่วนนี้ในตัวแก้ปัญหา SMTที่ใช้DPLL(T)ได้ถูกรวมเข้าไว้ในcvc5แล้ว^{[ 30 ]}การขยายผลลัพธ์นี้ ความพึงพอใจสำหรับอนาล็อกของคลาส Bernays–Schönfinkelสำหรับตรรกะการแยกประเภทที่มีตำแหน่งหน่วยความจำที่ไม่ได้ตีความก็สามารถแสดงได้ว่าสมบูรณ์แบบ PSPACE เช่นกัน ในขณะที่ปัญหานี้ไม่สามารถตัดสินได้เมื่อใช้ตำแหน่งหน่วยความจำที่ตีความแล้ว (เช่น จำนวนเต็ม) หรือการสลับตัวบ่งปริมาณเพิ่มเติม^{[ 31 ]}