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

type Node = {bool value; data next:Node;} /* simple boolean abstraction of values */

pred greater(bool value1,value2) = 
  value1=true & value2=false;

pred inorder(pointer x:Node) = 
  allpos p of Node: x<next*>p => !greater(x.value,p.value);

pred inorder2(pointer x,y:Node) = 
  (y=null => inorder(x)) &
  (y!=null => allpos p of Node: x<next*>p & p<next*>y => !greater(x.value,p.value));

proc bubblesort(data x:Node):Node
[true]
{
  pointer p,y,yn,t:Node;
  bool change;
  change = true;
  while [!change => inorder(x)] (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) &
           (!change => inorder2(x,y))]
          (yn!=null) {
      if (y.value=true & yn.value=false /* 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;
}
[inorder(return)]