What is null.f in our model?

• does it exist?

What should a verifier say about a program that can do null dereference?

What are preconditions for:

x.f=y

x=y.f

a[i]=v

Examples in Insertion into Doubly-Linked List

More complex examples:

y = x.next.next
x.next.next.prev = y
(x = null || x.next == y)