Therese Hardin - Concepts and Semantics of Programming Languages 1

Let Xbe a set of identifiers and Va set of values. The association of an identifier x ∈ Xwith a value v ∈ Vis called a binding (of the identifier to its value), and a set Env of bindings is called an execution environment or evaluation environment . Env( x ) denotes the value associated with the identifier x in Env. The set of environments is denoted as E.

In practice, the set of identifiers Xthat are actually used is finite: usually, we only consider those identifiers that appear in a program. An environment may thus be represented by a list of bindings, also called Env:

where { x 1, x 2, . . ., x n} denotes a finite subset of X, known as the domain of the environment and denoted as dom(Env). By convention, Env( x ) denotes the value v , which appears in the first ( x , v ) binding encountered when reading the list Env from the head (here, from left to right).

In this model, a binding can be added to an environment using the operator ⊕. By convention, bindings are added at (the left of) the head of the list representing the environment:

Suppose that a certain operation introduces a new binding of an identifier, which is already present in the environment, for example ( x 2, v new):

The so-obtained environment ( x 2, v new) ⊕ Env contains two bindings for x 2. Searching for a binding starts at the head of the environment, and, with our convention, new bindings are added at the head. So the most recent addition, ( x 2, v new), will be the first found. The binding ( x 2, v 2) is not deleted, but it is said to be masked by the new binding ( x 2, v new). Several bindings for a single identifier x may therefore exist within the same environment, and the last binding added for x will be used to determine the associated value of x in the environment. Formally, the environment ( x , v ) ⊕ Env verifies the following property:

By convention, the notation ( x 2, v 2) ⊕ ( x 1, v 1) ⊕ Env is used to denote the environment ( x 2, v 2) ⊕ (( x 1, v 1) ⊕ Env). For example, (( x , v 2) ⊕ ( x , v 1) ⊕Env)( x ) = v 2

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

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 Rbe a set of references and Va set of values. The association of a reference r ∈ Rwith a value v ∈ Vis 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 Mbe 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 ):