type List = {data next:List;}

pred roots(pointer x,y:List, set R:List) = 
  allpos p of List: p in R <=> x<next*>p | y<next*>p;

proc reverse(data list:List):List
  set R:List;
[roots(list,null,R)]
{
  data res:List;
  pointer temp:List;
  res = null;
  while [roots(list,res,R)] (list!=null) {
    temp = list.next;
    list.next = res;
    res = list;
    list = temp;
  }
  return res;
}
[roots(return,null,R)]