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 ])[r2 := v2] is denoted as Mem[r1 := v1 ][r1 := v2].
For example, (Mem[r1:= v1 ][r2:= v2])(r) = v2.
The function valeur_ref computes the value stored at a given location. If nothing has previously been written at this location, the function returns a special value (None), indicating the absence of a known value (i.e. a value resulting from initialization or computation).
Python def valeur_ref(mem,a): if len(mem) == 0: return None else: a1,v1 = mem[0] if a == al: return v1 else: return valeur_ref(mem[1:],a)OCaml let rec valeur_ref mem a = match mem with | [] -> None | (a1, v1) :: t -> if a = a1 then Some v1 els (valeur_ref t a) val valeur_ref : (’a * ’b) list -> ’a -> ’b option
The following function writes a value into the memory:
Python def write_mem(mem,a,v): if len(mem) == 0: return [(a,v)] else: a1,v1 = mem[0] if a == a1: return [(a1,v)] + mem[1:] else: return [(a1,v1)] + write_mem(mem[1:],a,v)OCaml let rec write_mem mem a v = match mem with | [] -> [(a, v)] | (a1, v1) :: t -> if a = a1 then (a1, v) :: t else (a1, v1) :: (write_mem t a v) val write_mem : (’a * ’b) list -> ’a -> ’b -> (’a * ’b) list
2.1.3. State
A state is defined as a pair (Env
Given an environment Env, the set of identifiers X is partitioned into two subsets:
The value associated with an identifier x in
2.2. Evaluation of expressions
The value of an expression is computed according to an evaluation environment and a memory, i.e. in a given state. This computation is defined by the evaluation semantics of the expression.
2.2.1. Syntax
The language of expressions Exp1 used here will be extended in Chapters 3 and 4. Its syntax is defined in Table 2.1.
Table 2.1. Language of expressions Exp1
| e ::= k | Integer constant | (k ∈ ℤ) |
| | x | Identifier | (x ∈ X) |
| | e1 + e2 | Addition | (e1, e2 ∈ Exp1) |
| | !x | Dereferencing | (x ∈ X) |
Thus, an expression e ∈ Exp1 is either an integer constant k ∈ ℤ, an identifier x ∈ X, an expression obtained by applying an addition operator to two expressions in Exp1 or an expression of the form !x denoting the value stored in the memory at the location bound to the mutable variable x. Thus, this is an inductive definition of the set Exp1. Note that Exp1 does not include an assignment construct. This is a deliberate choice. This point will be discussed in greater detail in section 2.3 by means of an extension of Exp1.
NOTE. – The symbol + used in defining the syntax of expressions does not denote the integer addition operator. It could be replaced by any other symbol (for example ⊠). Its meaning will be assigned by the evaluation semantics. The same is true of the constant symbols: for example, the symbol 4 may be interpreted as a natural integer, a relative integer or a character.
EXAMPLE 2.1.– !x + y is an expression of Exp1 in the same way as (x + 2) + 3. Parentheses are used here to structure the expression, they are part of the so-called concrete syntax and will disappear in the AST.
The set Exp1 of well-formed expressions of the language is defined by induction and expressed directly by a recursive sum type. Types of this kind can be constructed in OCaml, but not in Python; in the latter case, they can be partially simulated by defining a class for each sum-type constructor. Each class must contain
