A separation logic framework for HOL

Separation Logic as introduced by Calcagno, O’Hearn, and Yang [7] is the foun- dation of the separation logic framework in HOL4. In the following, this foundation will be described. 3.2.1 States and Predicates on States As the name suggests, Abstract Separation Logic is an abstract version of separation logic. It abstracts from both the concrete specification and the concrete programming 62 CHAPTER 3. THEORETICAL FOUNDATION AND IMPLEMENTATION language. The programming language of Abstract Separation Logic manipulates some abstract states, the specification language is based on predicates on these states. 3.2.1.1 Separation Combinators Since nothing is known about these states, a partial function , called the separation combinator, is used to combine states and define whether two states are separate. Definition 3.2.1 (Separation Combinator (HOL4-Thm 217)). A separation combinator on a set of states Σ is a partially defined function : Σ Σ a Σ that satisfies the following properties: • is partially associative, i. e. s1, s2, s3. Definedps1 ps2 s3qq Definedpps1 s2q s3q ^ s1, s2, s3. Definedps1 ps2 s3qq un ps1 ps2 s3q ps1 s2q s3q • is partially commutative, i. e. s1, s2. Definedps1 s2q Definedps2 s1q ^ s1, s2. Definedps1 s2q un ps1 s2 s2 s1q • is partially cancellative, i. e. s1, s2, s3. Definedps1 s2q ^ Definedps1 s3q ^ ps1 s2 s1 s3q un ps2 s3q • for all states s P Σ there exists a neutral element us P Σ with us s s HOL4 remark 3.2.2. HOL4 supports only total functions. In order to formalise separation combinators, which are only partially defined, option-types are used. The value NONE is used to model undefined, whereas SOME(x) represents the defined value x. Definition 3.2.3 (Separateness, Substates, Superstates (HOL4-Thms 132, 133)). The definition of separation combinators induces notions of separateness (#), substates ( ) and superstates (©). s1 # s2 iff s1 s2 is defined s1 s3 iff Ds2. s3 s1 s2 s3 © s1 iff s1 s3