Extending Imp with Memory Accesses Syntax: (comm)c::=... |x:=[e I [e]:=e' x cons(e1,e2) I dispose(e) Program States (store)s∈Var→Z (heap)h∈ N-fin Z (state)σ：= (s,h) Extending Imp with Memory Accesses