# from 'Introduction to Algorithms', chapter 14 type Node = { bool color; # false=red, true=black data left,right:Node; pointer p:Node[this^Node.left union this^Node.right={p}]; } pred red(pointer p:Node) = p.color=false; pred black(pointer p:Node) = p.color=true | p=null; pred inv(pointer p:Node) = black(p) & # (missing in the book!!) allpos q of Node: p<(left+right)*>q => (red(q) => black(q.left) & black(q.right)); # note: the arithmetic black-height part cannot be expressed pred almostinv1(pointer p,r:Node) = allpos q of Node: p<(left+right)*>q => (red(q) => (black(q.left) | q.left=r) & (black(q.right) | q.right=r)); pred almostinv2(pointer p,r:Node) = allpos q of Node: p<(left+right)*>q => (red(q) => (black(q.left) | q.left=r | q=r) & (black(q.right) | q.right=r | q=r)); data root:Node; proc leftrotate(pointer x:Node):void pointer B,X,Y,P,Q:Node; [root!=null & root<(left+right)*>x & x.right!=null & (almostinv1(root,x.right) | almostinv1(root,x)) & red(x) & B=x.right.left & X=x & Y=x.right & P=x.p & Q=root] # see leftrotate.pale for implementation [Y.left=X & X.right=B & P=Y.p & root<(left+right)*>X & almostinv2(root,X) & red(X) & (P=null => root=Y) & (P!=null => root=Q)] proc rightrotate(pointer x:Node):void pointer B,X,Y,P,Q:Node; [root!=null & root<(left+right)*>x & x.left!=null & (almostinv1(root,x.left) | almostinv1(root,x)) & red(x) & B=x.left.right & X=x & Y=x.left & P=x.p & Q=root] # see rightrotate.pale for implementation [Y.right=X & X.left=B & P=Y.p & root<(left+right)*>X & almostinv2(root,X) & red(X) & (P=null => root=Y) & (P!=null => root=Q)] proc treeinsert(data z:Node):void pointer Z,Q:Node; [z.left=null & z.right=null & Z=z & inv(root) & Q=root] # see treeinsert.pale for implementation [root<(left+right)*>Z & Z.left=null & Z.right=null & almostinv1(root,Z) & (black(root) | root=Z) & (Q!=null => root=Q)] proc redblackinsert(data t:Node):void [t.left=null & t.right=null & inv(root)] { pointer y,x:Node; x = t; treeinsert(x) [treeinsert.Z=x & treeinsert.Q=root]; x.color = false; while [x!=null & root<(left+right)*>x & almostinv1(root,x) & (black(root) | x=root) & (x!=root & red(x.p) => red(x))] (x!=root & x.p.color=false) { if (x.p=x.p.p.left) { # NULL POINTER ERROR IF NOT REQUIRING INPUT-ROOT TO BE BLACK y = x.p.p.right; if (y!=null & y.color=false) { x.p.color = true; y.color = true; x.p.p.color = false; x = x.p.p; } else { if (x=x.p.right) { x = x.p; leftrotate(x) [leftrotate.X=x & root<(left+right)*>x & black(leftrotate.P.right) & red(leftrotate.Y) & black(leftrotate.X.left) & black(leftrotate.B) & black(leftrotate.Y.right)]; } split [x.p.left=x & x.p.p.left=x.p & black(x.p.p.right) & root<(left+right)*>x & almostinv2(root,x) & black(x.left) & black(x.right) & black(x.p.right)]; x.p.color = true; x.p.p.color = false; rightrotate(x.p.p) [rightrotate.Y.left=x & black(rightrotate.B) & black(rightrotate.X.right) & root<(left+right)*>x & black(rightrotate.Y) & red(rightrotate.X) & rightrotate.Q=root & x!=null]; root.color = true; } } else { y = x.p.p.left; if (y!=null & y.color=false) { x.p.color = true; y.color = true; x.p.p.color = false; x = x.p.p; } else { if (x=x.p.left) { x = x.p; rightrotate(x) [rightrotate.X=x & root<(right+left)*>x & black(rightrotate.P.left) & red(rightrotate.Y) & black(rightrotate.X.right) & black(rightrotate.B) & black(rightrotate.Y.left)]; } split [x.p.right=x & x.p.p.right=x.p & black(x.p.p.left) & root<(right+left)*>x & almostinv2(root,x) & black(x.right) & black(x.left) & black(x.p.left)]; x.p.color = true; x.p.p.color = false; leftrotate(x.p.p) [leftrotate.Y.right=x & black(leftrotate.B) & black(leftrotate.X.left) & root<(left+right)*>x & black(leftrotate.Y) & red(leftrotate.X) & leftrotate.Q=root & x!=null]; root.color = true; } } } root.color = true; } [inv(root)]