LITMIR.BIZ

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

Given a state (Env, Mem), we determine the evaluation semantics of an expression e ∈ Exp₁ by computing the value of e in this state, i.e. by evaluating e in this state. Values may be relative integers or references, hence V = ℤ U R. An additional, specific value Err is added to the set V; this result is returned as the value of “meaningless” expressions. The result of the evaluation of an expression in Exp₁ will therefore be a value belonging to the set

      Values in V are either relative integers or references. By defining a sum type, these two collections of values can be grouped into a single type.

      Python class CInt1: def __init__(self,cst_int): self.cst_int = cst_int class CRef1: def __init__(self,cst_adr): self.cst_adr = cst_adr

      Each class possesses a (object) constructor with the same name as the class: the constant k obtained from integer n (or, respectively, from reference r) is thus written as CInt1(n) (respectively, CRef1(r)), and this integer (respectively, reference) can be accessed from (the object) k by writing k.cst_int (respectively k.cst_adr). With OCaml, the type of elements in V is defined directly, as follows:

      OCaml type ’a constl = CIntI of int | CRefl of ‘a

      A value of this type is obtained either using the constructor CInt1 applied to an integer value or using the constructor CRef1 applied to a value of type ’a corresponding to the type used to represent references.

      A type grouping the elements of is defined by applying the same method:

      Python class VCste1: def __init__(self,cste): self.cste = cste class Erreur1: pass

      An element v in is either a value in V obtained from a constant k and written as VCste1(k), or an object in the class Erreur1 (pass is used here to express the fact that the (object) constructor has no argument). With OCaml, the type of the elements in 𝕧 is defined directly as follows:

      OCaml type ’a valeursl = VCstel of ’a constl | Erreur1

2.2.3. Evaluation semantics

      There are several formalisms that may be used to describe the evaluation of an expression. These will be introduced later. Let us construct an evaluation function:

The evaluation of the expression e in the environment Env and memory state Mem is denoted as with v ∈ V. Table 2.2 contains the recursive definition of the function

Table 2.2. Evaluation of the expressions of Exp₁

	(k ∈ ℤ)
	if x ∈ X and x ∈ dom(Env)
	if x ∈ X and x ∉ dom(Env)

      The value of an integer constant is the integer that it represents. The value of an identifier is that which is bound to it in the environment, or Err. The value of an expression constructed with an addition symbol and two expressions e₁ and e₂ is obtained by adding the relative integers resulting from the evaluations of e₁ and e₂; the result will be Err if e₁ or e₂ is not an integer. The value of !x is the value stored at the reference Env(x) when x is a mutable variable, and Err otherwise.

      Thus, if e is evaluated as a reference, then e can only be an identifier. Furthermore, certain expressions in Exp₁ are syntactically correct, but meaningless: for example, the expression !x when x is not a mutable variable, i.e. when x does not bind a reference in the environment, or x₁ + x₂ when x₁ (or x₂) is a mutable variable. On the other hand, !x + y is a meaningful expression that denotes a value when y binds an integer and x binds a reference to an integer.

      EXAMPLE 2.2.– Let us evaluate the expression !x + y

      in the state and

The evaluation function is obtained directly as follows:

      Python def eval_exp1(env,mem,e): if isinstance(e,Cste1): return VCste1(CInt1(e.cste)) if isinstance(e,Var1): x = valeur_de(env,e.symb) if isinstance(x,CInt1) or isinstance(x,CRef1): return VCste1(x) return Erreur1() if isinstance(e,Plus1): ev1 = eval_exp1(env,mem,e.exp1) if isinstance(ev1,Erreur1): return Erreur1() v1 = ev1.cste ev2 = eval_exp1(env,mem,e.exp2) if isinstance(ev2,Erreur1): return Erreur1() v2 = ev2.cste if isinstance(v1,CInt1) and isinstance(v2,CInt1): return VCste1(CInt1(v1.cst_int + v2.cst_int)) return Erreur1() if isinstance(e,Bang1): x = valeur_de(env,e.symb) if isinstance(x,CRef1): y = valeur_ref(mem,x.cst_adr) if y is None: return Erreur1() return VCste1(y) return

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