8 CHAPTER 1.AN OVERVIEW It should also be mentioned that separation logic is related to other recent logics that embody a notion of separation,such as spatial logics or ambient 1ogic35,36,37,38,39,40. 1.3 The Programming Language The programming language we will use is a low-level imperative language- specifically,the simple imperative language originally axiomatized by Hoare (3,4],extended with new commands for the manipulation of mutable shared data structures: (comm):=… |(var）:=cons(exp〉，.，(exp) allocation I(war〉：=[(expl lookup I[(exp】:=(exp mutation dispose(exp) deallocation Memory managenent is explicit;there is no garbage collection.As we will dereferencing of dangling addresses will cs mantically we extend computational states tocontain two components a store (son mes called stack mapping variables into values(as in the semantics of the unextended simple imperative language),and a heap,map- ping addresses into values(and representing the mutable structures). In the early versions of separation logic,integers,atoms,and addresses were regarded as distinct kinds of value,and heaps were mappings from finite sets of addresses to nonempty tuples of values: Values Integers U Atoms U Addresses where Integers,Atoms,and Addresses are disjoint nil e Atoms Storesy=V→Values Henp --Valae) Statesv =Storesv x Heaps where V is a finite set of variables. 8 CHAPTER 1. AN OVERVIEW It should also be mentioned that separation logic is related to other recent logics that embody a notion of separation, such as spatial logics or ambient logic [35, 36, 37, 38, 39, 40]. 1.3 The Programming Language The programming language we will use is a low-level imperative language — specifically, the simple imperative language originally axiomatized by Hoare [3, 4], extended with new commands for the manipulation of mutable shared data structures: hcommi ::= · · · | hvari := cons(hexpi, . . . ,hexpi) allocation | hvari := [hexpi] lookup | [hexpi] := hexpi mutation | dispose hexpi deallocation Memory managenent is explicit; there is no garbage collection. As we will see, any dereferencing of dangling addresses will cause a fault. Semantically, we extend computational states to contain two components: a store (sometimes called a stack), mapping variables into values (as in the semantics of the unextended simple imperative language), and a heap, map￾ping addresses into values (and representing the mutable structures). In the early versions of separation logic, integers, atoms, and addresses were regarded as distinct kinds of value, and heaps were mappings from finite sets of addresses to nonempty tuples of values: Values = Integers ∪ Atoms ∪ Addresses where Integers, Atoms, and Addresses are disjoint nil ∈ Atoms StoresV = V → Values Heaps = S A fin ⊆Addresses (A → Values+ ) StatesV = StoresV × Heaps where V is a finite set of variables