CHAPTER 1.AN OVERVIEW particular,do not depend upon the heap,so that they are always well-defined and never cause side-effects. Thus expressions do not contain notations,such as cons or [-that refer to the heap;instead these notations are part of the structure of com- mands (and thus cannot be nested).It follows that none of the new heap- manipulating commands are instances of the simple assignment command (var):=(exp e h we w ite the allo lookup, and mutation ands with the familiar operator:=).In act,these com vill n obey Hoare's inference rule for assignment.However,since they alter the store at the variable v,we will say that the commands v:=cons(.)and v:=[el,as well as v:=e (but not [u]:=e or dispose v)modify v. Our strict avoidance of side-effects in expressions will allow us to use them in assertions with the same freedom as in ordinary mathematics.This will substantially simplify the logic,at the expense occasional co mplications in programs. The semantics of the new commands is simple enough to be conveyed by example.If we begin with a state where the store maps the variables x and y into three and four,and the heap is empty,then the typical effect of each kind of heap-manipulating command is: Store:x:3,y:4 Heap:empty Allocation ×:=cons(1,2); Store:x:37,y:4 Heap:37:1,38:2 Lookup y:=[x]; Store:x:37.y:1 Heap:37:1,38:2 Mutation x+1刂=3； Store:x:37,y:1 Heap:37:1,38:3 Deallocation dispose(x+1) Store:x:37,y:1 Heap:37:1 The allocation operation cons(ei,. .en)activates and initializes n cells in the heap.It is important to notice that,aside from the requirement that the addresses of these cells be consecutive and previously inactive,the choice of addresses is indeterminate. 10 CHAPTER 1. AN OVERVIEW particular, expressions do not depend upon the heap, so that they are always well-defined and never cause side-effects. Thus expressions do not contain notations, such as cons or [−], that refer to the heap; instead these notations are part of the structure of com￾mands (and thus cannot be nested). It follows that none of the new heap￾manipulating commands are instances of the simple assignment command hvari := hexpi (even though we write the allocation, lookup, and mutation commands with the familiar operator :=). In fact, these commands will not obey Hoare’s inference rule for assignment. However, since they alter the store at the variable v, we will say that the commands v := cons(· · ·) and v := [e], as well as v := e (but not [v] := e or dispose v) modify v. Our strict avoidance of side-effects in expressions will allow us to use them in assertions with the same freedom as in ordinary mathematics. This will substantially simplify the logic, at the expense of occasional complications in programs. The semantics of the new commands is simple enough to be conveyed by example. If we begin with a state where the store maps the variables x and y into three and four, and the heap is empty, then the typical effect of each kind of heap-manipulating command is: Store : x: 3, y: 4 Heap : empty Allocation x := cons(1, 2) ; ⇓ Store : x: 37, y: 4 Heap : 37: 1, 38: 2 Lookup y := [x] ; ⇓ Store : x: 37, y: 1 Heap : 37: 1, 38: 2 Mutation [x + 1] := 3 ; ⇓ Store : x: 37, y: 1 Heap : 37: 1, 38: 3 Deallocation dispose(x + 1) ⇓ Store : x: 37, y: 1 Heap : 37: 1 The allocation operation cons(e1, . . . , en) activates and initializes n cells in the heap. It is important to notice that, aside from the requirement that the addresses of these cells be consecutive and previously inactive, the choice of addresses is indeterminate