Recall syntax of Simple Programming Language.

In addition to

x = T
if (F) c1 else c2
c1 ; c2
while (F) c1

we have new basic statement:

x.f = e
x = new

In expressions we use

x.f

for dereferencing.

Resulting syntax:

c ::=  x=T | x.f=T | x=new | 
       assert(F) | assume(F) | havoc x |
       (if (F) c else c) | c ; c | (while (F) c)
T ::= V | null | T.f
F ::= (T=T) | (~F) | (F & F) | (F|F)
V ::= x | y | z | ...