/* from 'Putting Static Analysis to Work for Verification: A Case Study' */

type Node = {/* values abstracted away */ data next:Node;}

proc bubblesort(data x:Node):Node
[true]
{
  pointer p,y,yn,t:Node;
  bool change;
  change = true;
  while [true] (change) {
    p = null;
    change = false;
    y = x;
    if (x!=null) {
      yn = y.next;
    }
    else { /*BUG FIX!*/
      yn = null;
    }
    while [(x!=null => y!=null & yn=y.next & (y!=x => p.next=y) & (y=x => p=null) & x<next*>y) &
           (x=null => yn=null)]
          (yn!=null) {
      if (?/* y.value > yn.value */) {
        t = yn.next;
        change = true;
        y.next = t;
        yn.next = y;
        if (p=null) {
          x = yn;
        }
        else {
          p.next = yn;
        }
        p = yn;
        yn = t;
      }
      else {
        p = y;
        y = yn;
        yn = y.next;
      }
    }
  }
  return x;
}
[true]