Separation logic is an extension of Hoare's logic for reasoning about programs that manipulate pointers. Its assertion language extends classical logic with a separating conjunction operator A * B, which asserts that A and B hold for separate portions of memory. In this tutorial I will first cover the basics of the logic, concentrating on highlights from the early work [1,2,3,4].
展开▼
