By convention, the notation (x₂,v₂) ⊕ (x₁ ,v₁) ⊕ Env is used to denote the environment (x₂,v₂) ⊕ ((x₁,v₁) ⊕ Env). For example, ((x,v₂) ⊕ (x,v1) ⊕Env)(x) = v2

      When an environment is represented by a list of bindings, the value Env(x) is found as follows:

      Python def valeur_de(env,x): for (x1,v1) in env: if x==x1: return v1 return NoneOCaml let rec valeur_de env x = match env with | [] -> None | (x1, v1) :: t -> if x = x1 then Some v1 else (valeur_de t x) val valeur_de: (‘a * ‘b) list -> ‘a -> ‘b option

      If no binding can be found in the environment for a given identifier, this function returns a special value indicating the absence of a binding. In Python, the constant None is used to express this absence of value, while in OCaml, the predefined sum type ’a option is used:

      OCaml type ’a option = Some of ’a | None

      The values of the type ’a option are either those of the type ’a or the constant None. The transformation of a value v of type ’a into a value of type ’a option is done by applying the constructor Some to v (see Chapter 5). The value None serves to denote the absence of value of type ’a; more precisely, None is a constant that is not a value of type ’a. This type ’a option will be used further to denote some kind of meaningless or absent values but that are needed to fully complete some definitions.

      The domain of an environment can be computed simply by traversing the list that represents it. A finite set is defined here as the list of all elements with no repetitions.

      Python def union_singleton(e,l): if e in l: return l else: return [e]+l def dom_env(env): r=[] for (x,v) in env: r = union_singleton(x,r) return rOCaml let rec union_singleton e l = if (List.mem e l then l else e::l val union_singleton : ’a -> ’a list -> ’a list let rec dom_env env = match env with | [] -> [] I (x, v) :: t -> (union_singleton x (dom_env t)) val dom_env : (’a * ’b) list -> ’a list

Since the value returned by the function valeur_de is obtained by traversing the list from its head, adding a new binding (x, v) to an environment is done at the head of the list and the previous bindings of x (if any) are masked, but not deleted.

      Python def ajout_liaison_env(env,x,v): return [(x,v)]+envOCaml let ajout_liaison_env env x v = (x, v) :: env val ajout_liaison_env : (’a * ’b) list -> ’a -> ’b -> (’a * ’b) list

      2.1.2. Memory

      The formal model of the memory presented below makes no distinction between the different varieties of physical memory described in Chapter 1. The state of the memory is described by associating a value with the location of the cell in which it is stored. The locations themselves are considered as values, called references. As we have seen, high-level languages allow us to name a location c, containing a value v, by an identifier x bound to the reference r of c.

      Let R be a set of references and V a set of values. The association of a reference r ∈ R with a value v ∈ V is represented by a pair (r, v), and a set Mem of such pairs is called here a memory. Mem(r) denotes the value stored at the reference r in Mem. Let M be the set of memories. In practice, the set of references, which is actually used, is finite: once again, only those locations used by a program are generally considered. This means that the memory can be represented by a list, also called Mem:

The existence of a pair (r, v) in a memory records that an initialization or a writing operation has been carried out at this location. Every referenced memory cell may be consulted through reading and can be assigned a new value by writing. In this case, the value previously held in the cell is deleted, it has “crashed”.

      Writing a value v at an address r transforms a memory Mem into a memory denoted as Mem[r := v]; if a value was stored at this location r in Mem, then this “old” value is replaced by v; otherwise, a new pair is added to Mem to take account of the writing operation. There is no masking, contrary to the case of the environments. Writing a new value v at a location r that already contains a value deletes the old value Mem(r):

      The domain of a memory dom(Mem) depends on the current environment and represents the space of references, which are accessible (directly or indirectly) from bound and non-masked identifiers in the current execution environment. The addition of a binding (x, r) to an environment Env has a twofold effect, creating (x, r) ⊕ Env and extending Mem to Mem[r := v].

      NOTE.– Depending on the language or program in question, the value v may be supplied just when x is introduced, or later, or never. If no value is provided prior to its first use, the result of the program is unpredictable, leading to errors called initialization errors. Indeed, a location always contains a value, which does not need to be suited to the current computation if it has not been explicitly determined by the program.

      Note that the addition of a binding (x, r) in an environment Env, of which the domain contains x, may mask a previous binding of x in Env, but will not add a new pair (r, v) to Mem if r was already present in the domain of Mem. Thus, any list of pairs representing a memory cannot contain two different pairs for the same reference. The memory Mem[r := v] verifies the following property:

      The memory (Mem[r1 := v1

---

Скачать книгу