Assertions for Correct use of Heap and Arrays
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:
Examples in Insertion into Doubly-Linked List
More complex examples:
y = x.next.next x.next.next.prev = y (x = null || x.next == y)