In computer science , separation logic [ 1] is an extension of Hoare logic , a way of reasoning about programs.
It was developed by John C. Reynolds , Peter O'Hearn , Samin Ishtiaq and Hongseok Yang,[ 1] [ 2] [ 3] [ 4] drawing upon early work by Rod Burstall .[ 5] The assertion language of separation logic is a special case of the logic of bunched implications (BI).[ 6] A CACM review article by O'Hearn charts developments in the subject to early 2019.[ 7]
^ a b 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 .
^ Ishtiaq, Samin; O'Hearn, Peter (2001). "BI as an assertion language for mutable data structures". Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages . ACM . pp. 14–26. doi :10.1145/360204.375719 . ISBN 1581133367 . S2CID 2652274 .
^ O'Hearn, Peter; Reynolds, John C.; Yang, Hongseok (2001). "Local Reasoning about Programs that Alter Data Structures". CSL . CiteSeerX 10.1.1.29.1331 .
^ Burstall, R. M. (1972). "Some techniques for proving programs which alter data structures". Machine Intelligence . 7 .
^ O'Hearn, P. W.; Pym, D. J. (June 1999). "The Logic of Bunched Implications". Bulletin of Symbolic Logic . 5 (2): 215–244. CiteSeerX 10.1.1.27.4742 . doi :10.2307/421090 . JSTOR 421090 . S2CID 2948552 .
^ O'Hearn, Peter (February 2019). "Separation Logic" . Commun. ACM . 62 (2): 86–95. doi :10.1145/3211968 . ISSN 0001-0782 .