Declarations In Imperative Languages

Where functional languages like FUN have definitions of variables, imperative languages have declarations. The basic idea is that the environment maps a variable to an address and there is a memory which maps addresses to values. The language IMP is a simple imperative language we can use to demonstrate declarations. IMP uses a hard-coded mapping from variable to memory location so this will need to be changed. We also extend IMP to include the construct

	
var x = e in p
	
      

This construct will lead to the allocation of a new memory address which will be initialised to the value of e. An environment will be created which maps the variable x to this address for the evaluation of the program p. Let E be the environment which maps variables to addresses, and M be a memory which maps addresses to values. So, the variable x will have the value M(E(x)). We will also need a function, New, which will allocate fresh addresses for a given memory.

Relational Semantics for IMP with Declarations

The relational semantics for our extended IMP uses the relations E⊢e,M ⇒ c and E⊢p,M ⇒ M', as shown below. From this we see that expressions, e, do not have side-effects as they do not alter memory, M.

Expressions
Constant	E⊢c,M ⇒ c
Variable	E⊢x,M ⇒ M(E(x)) where x∈dom(E) and E(x)∈dom(M)
Composite	E⊢e1,M ⇒ n1 E⊢e2,M ⇒ n2 --------------------------      E⊢e1 op e2,M ⇒ n3      where n3=n1 op n2
Programs
Null	E⊢null,M ⇒ M
Assignment	E⊢e,M ⇒ n -------------------- E⊢x:=e,M ⇒ M{n/E(x)} Here M{n/α} means memory location α contains value n.
Sequence	E⊢p1,M ⇒ M' E⊢p2,M' ⇒ M'' -------------------------    E⊢(p1;p2),M ⇒ M''
Conditional	E⊢b,M ⇒ true E⊢p1,M ⇒ M' ---------------------------- E⊢if b then p1 else p2,M ⇒ M'   E⊢b,M ⇒ false E⊢p2,M ⇒ M' ---------------------------- E⊢if b then p1 else p2,M ⇒ M'
Iteration	E⊢b,M ⇒ true E⊢p,M' ⇒ M' E⊢while b do p,M' ⇒ M'' --------------------------------------------------            E⊢while b do p,M ⇒ M''    E⊢b,M ⇒ false -------------------- E⊢while b do p,M ⇒ M
Declaration	E⊢e,M ⇒ n E{(x,α))}⊢p,M{(n/α)} ⇒ M' -------------------------------------         E⊢var x = e in p,M ⇒ M' where α=New(dom M) and M{n/α} means memory location α contains value n.

From the above we see that memory locations allocated with New are not deallocated. In the language above we could perform this deallocation in the declaration rule. For this to work we would need a function, Free, which would remove an address mapping from a memory. The declaration rule would then be:

Declaration

E⊢e,M ⇒ n E{(x,α))}⊢p,M{(n/α)} ⇒ M' -------------------------------------         E⊢var x = e in p,M ⇒ M'' where M'' = Free(M',α).

References

R. Burstall. Language Semantics and Implementation. Course Notes. 1994.