type List = {data next:List;}

pred reachable(pointer x:List, set R:List) = x<next*>R;

proc reverse(data x:List):List
  pointer P,Q:List;
  set R:List;
[reachable(x,R) & P=x & (x!=null => Q=x.next)]
{
  pointer t:List;
  if (x!=null) {
    if (x.next!=null) {
      t = reverse(x.next) [P=x & x!=null & x.next!=null & Q=x.next & !empty(reverse.R) &
                           R=reverse.R union {x} & !(x in reverse.R) & reverse.P=Q];
      x.next.next = x;
      x.next = null;
      x = t;
    }
  }
  split [reachable(x,R) & (P=null | P.next=null) & (x!=null => x<next*>P)]
  return x;
}
[reachable(return,R) & (P=null | P.next=null) & (return!=null => return<next*>P)]