SE547: Sequential noninterference [6/23] |

A *memory* μ is a mapping from variables to integers, for example:

{

x= 37,y= 5 }

Write μ(*e*) for the result of evaluating expression *e* in memory μ. For example,
in the above memory, what are:

μ(

x+ 1)

μ(x==y)

Write μ[*x*:=*n*] for the result of updating memory μ so *x* now contains *n*.
For example, in the above memory, what are:

μ[

y:= μ(x+ 1)]

μ[y:= μ(x==y)]