منطق جدایی

منطق جدایی (به انگلیسی: Separation Logic) تعمیمی از منطق هور (Hoare logic) است که هدف اصلی ابداع آن، بررسی و وارسی ریاضی برنامه‌هایی است که داده‌ها را در حافظه تغییر می‌دهند و خانه‌های مختلف از حافظه هستند که در معرض تحول هستند. این منطق توسط جان سی رینولدز, Peter O'Hearn, Samin Ishtiaq و Hongseok Yang معرفی شده‌است.^[۱]^[۲]^[۳]^[۴]

مفاهیم کلی

در برنامه‌هایی که از اشاره‌گر بهره می‌برند، استفاده از منطق‌های پیشین نظیر منطق هور ممکن نیست. علت آن است که در این‌جا، هر خانه از حافظه اهمیت دارد و باید زبان منطق مورد نظر، توانایی اشاره به قسمت‌های مختلف از حافظهٔ رایانه را داشته باشد. به این دلیل، نیاز به تعریف عملگری جدید حس شد. این احساس نیاز، منجر به تعریف عملگر $\ast$ شد که به صورت شهودی یعنی دو عملوند آن، در قسمت‌های مجزا از حافظهٔ پشته هستند؛ لذا، با شکل‌گیری این منطق و ابزارهای آن، وارسی الگوریتم‌ها و برنامه‌های موازی امکان‌پذیر شده‌است.^[۲]

اعلان‌ها

منظور ما در این‌جا از حالت، وضعیت مقادیر موجود در حافظهٔ تصادفی و همچنین حافظهٔ پشته است. اعلان $P$ در منطق جدایی، تعدادی حالت را مشخص می‌کند که در آن‌ها $P$ درست است. با تعریف استقرایی ساختار لغوی منطق جدایی، عبارت $P\ast Q$ حالاتی را مشخص می‌کند که $P$ در یک قسمت از ساختار حافظهٔ تصادفی/پشته و $Q$ در قسمتی کاملاً مجزا از آن درست باشد. پس تعریف استقرایی زبان منطق به این صورت است:

گزارهٔ $\mathbf {e} \mathbf {m} \mathbf {p}$ یک پشتهٔ خالی را نشان می‌دهد. یعنی پشته‌ای که هیچ خانهٔ آن، به متغیری اختصاص داده نشده باشد.
عملگر دوتایی $\mapsto$ نشان‌دهندهٔ یک اشاره‌گر است. یعنی متغیری به خانه‌ای از حافظه اشاره می‌کند.
عملگر دوتایی $\ast$ نشان‌دهندهٔ درستی دو عبارت در دو قسمت مجزای حافظه است.
عملگر دوتایی $-\!\!\ast$ به این معنا است که اگر بتوانیم حافظه را طوری گسترش دهیم که عملگر اول برقرار باشد، عملگر دوم نیز ناگزیر برقرار است.^[۵]

حال می‌توان این عملگرها را در مفاهیم منطق مرتبهٔ اول به کار برد و با آن عباراتی در مورد تأثیر یک برنامه بر حافظه گفت یا در بیان مشخصات حافظه استفاده کرد.

شکل عبارت $x\mapsto 3,y\ast y\mapsto 3,x$ در حافظه

استدلال و استنتاج

در این منطق هم مانند دیگر منطق‌ها می‌توان اصول استنتاج تعریف و طبق آن‌ها استدلال کرد. برای مثال طبق تعریف عملگر $-\!\!\ast$ ، داریم: ${\frac {s,h\models P\ast (P-\!\!\ast \,Q)}{s,h\models Q}}$

تمامی قواعد استنتاج در منطق هور، در منطق جدایی هم معتبر هستند؛ و همچنین در این منطق، قاعدهٔ قاب هست که برای سه‌تایی‌های هور تعریف می‌شود. یک سه‌تایی هور، به شکل کلی $\{P\}\ C\ \{Q\}$ است که یعنی اگر، حافظه قبل از اجرای برنامهٔ $C$ ، در حالت $P$ باشد، پس از اجرای آن به حالت $Q$ می‌رود. حال طبق قاعدهٔ قاب داریم:

${\frac {\{P\}\ C\ \{Q\}}{\{P\ast R\}\ C\ \{Q\ast R\}}}$

به‌وسیلهٔ این قاعده، می‌توان استدلالات محلی در مورد حافظه را گسترش داد و در مورد بخش بزرگ‌تری از حافظه صحبت کرد. استدلال محلی برای یک برنامهٔ $C$ ، یعنی استدلال در مورد تمامی متغیرها و خانه‌های حافظه که توسط $C$ تغییر می‌یابند. این‌ها را O'Hearn، ردپای $C$ می‌نامد. او بیان می‌دارد که: «برای فهم رفتار یک برنامه، باید در مورد خانه‌هایی اطلاع کسب کنید که توسط آن برنامه تغییر می‌یابند. ارزش دیگر خانه‌ها به صورت خودبه‌خود ثابت باقی می‌ماند.»^[۴]

ابزارهای وارسی مدلّ‌ها و تحلیل برنامه‌ها

منطق جدایی به دلیل کاربرد در درستی‌یابی برنامه‌های کامپیوتری، عملکرد وسیعی در ابزارهای مختلف وارسی مدل‌ها و همچنین کاربردهای صنعتی دارد. به‌نحوی‌که O'Hearn که از مبدعین این منطق بوده، از سال ۲۰۱۳ در شرکت فیسبوک مشغول به کار است. به صورت کلی، ابزارهایی که از منطق جدایی استفاده می‌کنند در دسته‌های مختلف هستند:

تحلیل خودکار برنامه‌ها: این دسته از ابزارها، تلاش می‌کنند تا به صورت خودکار تحلیل‌هایی را در مورد ساختار، تأثیر و معنای برنامه‌ها انجام دهند. به‌طور مثال شرکت فیسبوک از ابزار Facebook Infer استفاده می‌کند که در این دسته جای می‌گیرد.
اثبات‌ها تعاملی: در این دسته، سعی بر آن است که با استفاده از قواعد استنتاج از پیش تعیین شده به اثبات‌های ریاضی برای عبارات در منطق جدایی برسیم. در حقیقت، این ابزارها جایگزین تلاش‌های طولانی افراد برای درستی‌یابی عبارات هستند. از نمونهٔ این ابزارها، اثبات‌کنندهٔ Coq است که دستهٔ وسیعی از عبارات، از ساده تا پیچیده را در بر می‌گیرد. Coq، در حقیقت یک زبان برنامه‌نویسی است که به‌وسیلهٔ آن می‌توان اعلان‌های مختلف را بیان کرد.
ابزارهای بینابین: این گروه، رویکردی مخلوط از اثبات‌کننده و تحلیل‌گر دارند. به این صورت که با دریافت برخی ویژگی‌ها، ویژگی‌های دیگر را می‌یابند و برای درستی آن‌ها اثبات ارائه می‌دهند. یک نمونه از این الگوریتم‌ها، مسئلهٔ قیاس دوگانه است. در این مسئله، به دنبال یافتن پیش‌شرط کافی برای به دست آوردن شرایط پس از اجرای یک برنامه هستیم. یک نمونه از این ابزارها، Smallfoot است که جزو نخستین نسل از آن‌هاست.

منابع

↑ Reynolds, John C. (2002). "Separation Logic: A Logic for Shared Mutable Data Structures" (PDF). LICS.
↑ ^۲٫۰ ^۲٫۱ Reynolds, John C. (1999). "Intuitionistic Reasoning about Shared Mutable Data Structure". In Davies, Jim; Roscoe, Bill; Woodcock, Jim (eds.). Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford–Microsoft Symposium in Honour of Sir Tony Hoare. Palgrave. {{cite book}}: Unknown parameter |editorlink1= ignored (|editor-link1= suggested) (help); Unknown parameter |editorlink2= ignored (|editor-link2= suggested) (help); Unknown parameter |editorlink3= ignored (|editor-link3= suggested) (help)
↑ Ishtiaq, Samin; O'Hearn, Peter (2001). "BI as an Assertion Language for Mutable Data Structures". POPL. ACM.
↑ ^۴٫۰ ^۴٫۱ O'Hearn, Peter; Reynolds, John C.; Yang, Hongseok (2001). "Local Reasoning about Programs that Alter Data Structures". CSL.
↑ O'hearn, Peter (2012). "A Primer on Separation Logic". {{cite book}}: Cite has empty unknown parameter: |1= (help); Missing or empty |title= (help)

Reynolds, John C, (2002),. "Separation Logic: A Logic for Shared Mutable Data Structures". LICS
Reynolds, John C. (1999). "Intuitionistic Reasoning about Shared Mutable Data Structure". In Davies, Jim; Roscoe, Bill; Woodcock, Jim. Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford–Microsoft Symposium in Honour of Sir Tony Hoare.
.Ishtiaq, Samin; O'Hearn, Peter (2001). "BI as an Assertion Language for Mutable Data Structures". POPL.
O'Hearn, Peter; Reynolds, John C. ; Yang, Hongseok (2001). "Local Reasoning about Programs that Alter Data Structures"
O'Hearn, Peter (2012). "A Primer on Separation Logic"

[lics02-1] Reynolds, John C. (2002). "Separation Logic: A Logic for Shared Mutable Data Structures" (PDF). LICS.

[sl1999-2] ۲٫۰ ^۲٫۱ Reynolds, John C. (1999). "Intuitionistic Reasoning about Shared Mutable Data Structure". In Davies, Jim; Roscoe, Bill; Woodcock, Jim (eds.). Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford–Microsoft Symposium in Honour of Sir Tony Hoare. Palgrave. {{cite book}}: Unknown parameter |editorlink1= ignored (|editor-link1= suggested) (help); Unknown parameter |editorlink2= ignored (|editor-link2= suggested) (help); Unknown parameter |editorlink3= ignored (|editor-link3= suggested) (help)

[popl01-3] Ishtiaq, Samin; O'Hearn, Peter (2001). "BI as an Assertion Language for Mutable Data Structures". POPL. ACM.

[csl01-4] ۴٫۰ ^۴٫۱ O'Hearn, Peter; Reynolds, John C.; Yang, Hongseok (2001). "Local Reasoning about Programs that Alter Data Structures". CSL.

[five-5] O'hearn, Peter (2012). "A Primer on Separation Logic". {{cite book}}: Cite has empty unknown parameter: |1= (help); Missing or empty |title= (help)

[۱]

[۲]

[۳]

[۴]

[۵]