example
a procedure
class List {List next}
void insert (List first, List rest) {first.next = rest}
an assertion
insert && Acyclic (rest) -> Acyclic’ (first)
where Acyclic (l : List) {no x : l.*next | x in x.+next}
how insert is translated
(first.next’ = rest) ? (all x | x != first -> x.next = x.next’) ? (rest’ = rest)
a counterexample
first = rest = L1 next = { } next’ = {L1 -> L1}