1.3.THE PROGRAMMING LANGUAGE (Actually,in most work using this kind of state,authors have imposed re- stricted formats on the records in the heap,to reflect the specific usage of the program they are specifying.) To permit unrestricted address arithmetic,however,in the version of the logic used in most of this paper wewill assume that all vales are integers. an infinite number of which are addr we also assume that atoms ar integers that are not addresses,and that heaps map addresses into single values: Values=Integers Atoms U Addresses C Integers where Atoms and Addresses are disjoint nil e Atoms Storesv=V→Values Henps=U(A-Valucs) Statesy =Storesy x Heaps where V is a finite set of variables (To permit unlimited allocation of records of arbitrary size,we require that, for all n >0,the set of addresses must contain infinitely many consecutive sequences of length n.For instance,this will occur if only a finite number of positive integers are not addresses.) Our inte is to apture the low-level character of machine lan uage.One estore as describing the ontents of reg the contents of n addresbe 41 ters,and the heap by assumin g that each address is equipped with an "activity bit";then the domain of the heap is the finite set of active addresses. The semantics of ordinary and boolean expressions is the same as in the simple imperative language: l (exp)Uv)Storesv)-Vales [be(boolexp)lbep∈ Storesv)(true,false) (where FV(p)is the set of variables occurring free in the phrase p).In1.3. THE PROGRAMMING LANGUAGE 9 (Actually, in most work using this kind of state, authors have imposed re￾stricted formats on the records in the heap, to reflect the specific usage of the program they are specifying.) To permit unrestricted address arithmetic, however, in the version of the logic used in most of this paper we will assume that all values are integers, an infinite number of which are addresses; we also assume that atoms are integers that are not addresses, and that heaps map addresses into single values: Values = Integers Atoms ∪ Addresses ⊆ Integers where 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. (To permit unlimited allocation of records of arbitrary size, we require that, for all n ≥ 0, the set of addresses must contain infinitely many consecutive sequences of length n. For instance, this will occur if only a finite number of positive integers are not addresses.) Our intent is to capture the low-level character of machine language. One can think of the store as describing the contents of registers, and the heap as describing the contents of an addressable memory. This view is enhanced by assuming that each address is equipped with an “activity bit”; then the domain of the heap is the finite set of active addresses. The semantics of ordinary and boolean expressions is the same as in the simple imperative language: [[e ∈ hexpi]]exp ∈ ( S V fin ⊇FV(e) StoresV ) → Values [[b ∈ hboolexpi]]bexp ∈ ( S V fin ⊇FV(b) StoresV ) → {true,false} (where FV(p) is the set of variables occurring free in the phrase p). In