CHAPTER 1.AN OVERVIEW that e points to e'somewhere in the heap: eege一e*true and that e points to a record with several fields: ee,,enge一e1*…*e+n-1en ee1,,enge一e1*…*e+n-le 证e一e1,,en*true Notice that assertions of the form ee',e-,and ee1. determine the extent (i.e..domain)of the heap they describe.while those of the form eand do no (Technic ally,the f forme said to be precis given in Section 2.3.3.) By using→，→，and both separating and ordinary conjunction,it is eas to describe simple sharing patterns concisely.For instance: 1.x3,y asserts that x points to an adjacent pair of cells containing 3 and y(i the store maps× x-3 and y into some values a and B,a is an address y and the heap maps a into 3 and a+1 into B). 2.y3.x asserts that y points to an adjacent pair of cells containing 3 and x. 圆 3.￥ →3y y一3，asserts that situations() and(2)hold for separate parts of the heap. ® 4.×-3,yAy一3，×asserts that situations(1)and (2)hold for the same heap,which can only happen if the values of x and y are the same 5.x -3,yy 3,x asserts that either (3)or (4) may hold,and that the heap may contain additional cells. 12 CHAPTER 1. AN OVERVIEW that e points to e 0 somewhere in the heap: e ,→ e 0 def = e 7→ e 0 ∗ true, and that e points to a record with several fields: e 7→ e1, . . . , en def = e 7→ e1 ∗ · · · ∗ e + n − 1 7→ en e ,→ e1, . . . , en def = e ,→ e1 ∗ · · · ∗ e + n − 1 ,→ en iff e 7→ e1, . . . , en ∗ true. Notice that assertions of the form e 7→ e 0 , e 7→ −, and e 7→ e1, . . . , en determine the extent (i.e., domain) of the heap they describe, while those of the form e ,→ e 0 and e ,→ e1, . . . , en do not. (Technically, the former are said to be precise assertions. A precise definition of precise assertions will be given in Section 2.3.3.) By using 7→, ,→, and both separating and ordinary conjunction, it is easy to describe simple sharing patterns concisely. For instance: 1. x 7→ 3, y asserts that x points to an adjacent pair of cells containing 3 and y (i.e., the store maps x and y into some values α and β, α is an address, and the heap maps α into 3 and α + 1 into β). y x ✲ 3 2. y 7→ 3, x asserts that y points to an adjacent pair of cells containing 3 and x. x y ✲ 3 3. x 7→ 3, y ∗ y 7→ 3, x asserts that situations (1) and (2) hold for separate parts of the heap. ◦ x ✲ 3 ◦ ❨✯ 3 ✛ y 4. x 7→ 3, y∧y 7→ 3, x asserts that situations (1) and (2) hold for the same heap, which can only happen if the values of x and y are the same. ◦ 3 ❍❥ ✟✯ x y ② 5. x ,→ 3, y ∧ y ,→ 3, x asserts that either (3) or (4) may hold, and that the heap may contain additional cells