type List = {data next:List;}

proc rotate(data x:List, pointer p:List):void
  pointer X,P,N:List;
[X=x & P=p & (x!=null => N=X.next & x<next*>p & p.next=null)]
{
 if (x!=null) {
   p.next = x;
   x = x.next;
   p = p.next;
   p.next = null;
 }
}
[X!=null => (N<next*>X & X.next=null | X=P)]