Example from the paper "Quantitative Shape Analysis" by Radu Rugina


% <0>  y = x.left;
% <1>  if (y.val == 1) {
% <2>    x.val = 0;
% <3>    y.val = 0;
% <4>    z = y.right;
% <5>    y.right = x;
% <6>    x.left = z; <7>
%      }

-------------------------------------------------------------------------------
How the algorithm work:

Given the following input:

             //  depth: DL+1
             |
     +-------+-------+   Notice tree is imbalanced here (skew=2)
     | depth:        |
    () DL           $$ depth: DL-2
     |
 +---+---+
 |       |  depth:
**       [] DL-2
depth:
DL-1

The algorithm produces balanced AVL tree:

             () depth: DL
             |
     +-------+-------+
     |               |
    **              // depth: DL-1
   depth:            |
   DL-1        +-----+-----+
               |           |
               []          $$
          depth: DL-2   depth: DL-2


-------------------------------------------------------------------------------

CLP:

p(0,H,X,Y,Z,Hf,Yf) :- p(1,H,X,H[X+1],Z,Hf,Yf).
p(1,H,X,Y,Z,Hf,Yf) :- H[Y]=1, p(2,H,X,Y,Z,Hf,Yf).
p(2,H,X,Y,Z,Hf,Yf) :- p(3,<H,X,0>,X,Y,Z,Hf,Yf).
p(3,H,X,Y,Z,Hf,Yf) :- p(4,<H,Y,0>,X,Y,Z,Hf,Yf).
p(4,H,X,Y,Z,Hf,Yf) :- p(5,H,X,Y,H[Y+2],Hf,Yf).
p(5,H,X,Y,Z,Hf,Yf) :- p(6,<H,Y+2,X>,X,Y,Z,Hf,Yf).
p(6,H,X,Y,Z,Hf,Yf) :- p(7,<H,X+1,Z>,X,Y,Z,Hf,Yf).
p(7,H,X,Y,Z,H,Y).

-------------------------------------------------------------------------------

Specification:

avl(H,null,0,{}).
avl(H,X,D1+1,{X} * S1 * S2) :-
	H[X]=D1-D2, 0 <= D1-D2, D1-D2 <= 1,
	avl(H,H[X+1],D1,S1), avl(H,H[X+2],D2,S2).
avl(H,X,D2+1,{X} * S1 * S2) :-
	H[X]=D1-D2, D1-D2 = -1,
	avl(H,H[X+1],D1,S1), avl(H,H[X+2],D2,S2).

-------------------------------------------------------------------------------

We prove:

N0: p(0,H,X,Y,Z,Hf,Yf), 
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|=
avl(Hf,Yf,DL,S).

N1: LEFT UNFOLD N0
p(1,H,X,Y1,Z,Hf,Yf), Y1=H[X+1],
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|= 
avl(Hf,Yf,DL,S).

N2: LEFT UNFOLD N1
p(2,H,X,Y1,Z,Hf,Yf), Y1=H[X+1], H[Y1]=1,
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|=
avl(Hf,Yf,DL,S).

N3: LEFT UNFOLD N2
p(3,H1,X,Y1,Z,Hf,Yf), Y1=H[X+1], H[Y1]=1, H1=<H,X,0>,
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|=
avl(Hf,Yf,DL,S).

N4: LEFT UNFOLD N3
p(4,H2,X,Y1,Z,Hf,Yf), Y1=H[X+1], H[Y1]=1, H1=<H,X,0>, H2=<H1,Y1,0>,
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|=
avl(Hf,Yf,DL,S).

N5: LEFT UNFOLD N4
p(5,H2,X,Y1,Z1,Hf,Yf), Y1=H[X+1], H[Y1]=1, H1=<H,X,0>, H2=<H1,Y1,0>,
    Z1=H2[Y1+2],
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|= 
avl(Hf,Yf,DL,S).

N6: LEFT UNFOLD N5
p(6,H3,X,Y1,Z1,Hf,Yf), Y1=H[X+1], H[Y1]=1, H1=<H,X,0>, H2=<H1,Y1,0>,
    Z1=H2[Y1+2], H3=<H2,Y1+2,X>,
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|= 
avl(Hf,Yf,DL,S).

N7: LEFT UNFOLD N6
p(7,H4,X,Y1,Z1,Hf,Yf), Y1=H[X+1], H[Y1]=1, H1=<H,X,0>, H2=<H1,Y1,0>,
    Z1=H2[Y1+2], H3=<H2,Y1+2,X>, H4=<H3,X+1,Z1>,
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|= 
avl(Hf,Yf,DL,S).

N8: LEFT UNFOLD N7, Hf=H4, Yf=Y1
p(7,Hf,X,Yf,H2[Yf+2],Hf,Yf), Yf=H[X+1], H[Yf]=1,
    H1=<H,X,0>, H2=<H1,Yf,0>, H3=<H2,Yf+2,X>,
    Hf=<H3,X+1,H2[Yf+2]>,
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|= 
avl(Hf,Yf,DL,S).

N9: RIGHT UNFOLD
p(7,Hf,X,Yf,H2[Yf+2],Hf,Yf), Yf=H[X+1], H[Yf]=1,
    H1=<H,X,0>, H2=<H1,Yf,0>, H3=<H2,Yf+2,X>,
    Hf=<H3,X+1,H2[Yf+2]>,
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|= 
Hf[Yf]=0, S={Yf}*?T1*?T2,
avl(Hf,Hf[Yf+1],DL-1,?T1),
avl(Hf,Hf[Yf+2],DL-1,?T2)

N10: RIGHT UNFOLD
p(7,Hf,X,Yf,H2[Yf+2],Hf,Yf), Yf=H[X+1], H[Yf]=1,
    H1=<H,X,0>, H2=<H1,Yf,0>, H3=<H2,Yf+2,X>,
    Hf=<H3,X+1,H2[Yf+2]>,
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|=
Hf[Yf]=0, Hf[Hf[Yf+2]]=0, S={Yf}*?T1*?T2, ?T2={Hf[Yf+2]} * ?T21 * ?T22,
avl(Hf,Hf[Yf+1],DL-1,?T1),
avl(Hf,Hf[Hf[Yf+2]+1],DL-2,?T21),
avl(Hf,Hf[Hf[Yf+2]+2],DL-2,?T22).

N11: ?T1->S11, ?T21->S12, ?T22->S2, eliminate ?T2
p(7,Hf,X,Yf,H2[Yf+2],Hf,Yf), Yf=H[X+1], H[Yf]=1,
    H1=<H,X,0>, H2=<H1,Yf,0>, H3=<H2,Yf+2,X>,
    Hf=<H3,X+1,H2[Yf+2]>,
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|=
Hf[Yf]=0, Hf[Hf[Yf+2]]=0, S={Yf}*S11*{Hf[Yf+2]} * S2 * S12,
avl(Hf,Hf[Yf+1],DL-1,S11),
avl(Hf,Hf[Hf[Yf+2]+1],DL-2,S12),
avl(Hf,Hf[Hf[Yf+2]+2],DL-2,S2).


-------------------------------------------------------------------------------

Prove: Hf[Yf]=0

Hf[Yf] = <H3,X+1,H2[H[X+1]+2]>[H[X+1]]
       = H3[H[X+1]]                  (since X+1 != H[X+1] since {X} * {H[X+1]})
       = <H2,H[X+1]+2,X>[H[X+1]]
       = H2[H[X+1]]                  (since H[X+1] != H[X+1]+2)
       = <H1,H[X+1],0>[H[X+1]] = 0

-------------------------------------------------------------------------------

Prove: Hf[Hf[Yf+2]]=0

Hf[Hf[H[X+1]+2]] = Hf[<H3,X+1,H2[H[X+1]+2]>[H[X+1]+2]]
                 = Hf[H3[H[X+1]+2]]  (since X+1 != H[X+1]+2 since {X}*{H[X+1]})
                 = Hf[<H2,H[X+1]+2,X>[H[X+1]+2]]
                 = Hf[X]
                 = <H3,X+1,H2[H[X+1]+2]>[X]
                 = H3[X]             (since X+1 != X)
                 = <H2,H[X+1]+2,X>[X]
                 = H2[X]             (since H[X+1]+2 != X since {X}*{H[X+1]})
                 = <H1,H[X+1],0>[X]
                 = H1[X]             (H[X+1]!=X since {X}*{H[X+1]})
                 = <H,X,0>[X] = 0

-------------------------------------------------------------------------------

Prove:
p(7,Hf,X,Yf,H2[Yf+2],Hf,Yf), Yf=H[X+1], H[Yf]=1,
    H1=<H,X,0>, H2=<H1,Yf,0>, H3=<H2,Yf+2,X>,
    Hf=<H3,X+1,H2[Yf+2]>,
    avl(H,H[X+2],DL-2,S2),
    avl(H,H[H[X+1]+1],DL-1,S11),
    avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|=
S={Yf}*S11*{Hf[Yf+2]} * S2 * S12

Simplify rhs:

S={H[X+1]}*S11*{<H3,X+1,<H1,Yf,0>[Yf+2]>[H[X+1]+2]} * S2 * S12

<=> S={H[X+1]}*S11*{H3[H[X+1]+2]} * S2 * S12 (since {X}*{H[X+1]})

<=> S={H[X+1]}*S11*{<H2,H[X+1]+2,X>[H[X+1]+2]} * S2 * S12 (since {X}*{H[X+1]})

<=> S={H[X+1]}*S11*{X} * S2 * S12   (AIP)

Implied by lhs

-------------------------------------------------------------------------------

Prove:
Yf=H[X+1], H[Yf]=1, H1=<H,X,0>, H2=<H1,Yf,0>, H3=<H2,Yf+2,X>,
Hf=<H3,X+1,H2[Yf+2]>, avl(H,H[H[X+1]+1],DL-1,S11),
S = {X} * {H[X+1]} * S2 * S11 * S12
|=
avl(Hf,Hf[Yf+1],DL-1,S11)

We perform the following right simplification steps:

avl(Hf,Hf[H[X+1]+1],DL-1,S11),

avl(Hf,<H3,X+1,H2[H[X+1]+2]>[H[X+1]+1],DL-1,S11)

avl(Hf,H3[H[X+1]+1],DL-1,S11)   (since X+1 != H[X+1]+1, since {X}*{H[X+1]})

avl(Hf,<H2,H[X+1]+2,X>[H[X+1]+1],DL-1,S11)

avl(Hf,H2[H[X+1]+1],DL-1,S11)   (since H[X+1]+2 != H[X+1]+1)

avl(Hf,<H1,H[X+1],0>[H[X+1]+1],DL-1,S11)

avl(Hf,H1[H[X+1]+1],DL-1,S11)   (since H[X+1] != H[X+1]+1)

avl(Hf,<H,X,0>[H[X+1]+1],DL-1,S11) 

avl(Hf,H[H[X+1]+1],DL-1,S11)    (since H[X+1]+1 != X since {X}*{H[X+1]})

avl(<H3,X+1,H2[H[X+1]+2]>,H[H[X+1]+1],DL-1,S11)

avl(H3,H[H[X+1]+1],DL-1,S11), X !in S11

avl(<H2,H[X+1]+2,X>,H[H[X+1]+1],DL-1,S11), X !in S11

avl(H2,H[H[X+1]+1],DL-1,S11), X !in S11, H[X+1] !in S11

avl(<H1,H[X+1],0>,H[H[X+1]+1],DL-1,S11), X !in S11, H[X+1] !in S11

avl(H1,H[H[X+1]+1],DL-1,S11), X !in S11, H[X+1] !in S11

avl(<H,X,0>,H[H[X+1]+1],DL-1,S11), X !in S11, H[X+1] !in S11

avl(H,H[H[X+1]+1],DL-1,S11), X !in S11, H[X+1] !in S11

avl(H,H[H[X+1]+1],DL-1,S11)
            (X !in S11 is true becayse {X}*S11,
             H[X+1] !in S11 is true because {H[X+1]}*S11)

Implied by LHS

-------------------------------------------------------------------------------

Prove:
Yf=H[X+1], H[Yf]=1, H1=<H,X,0>, H2=<H1,Yf,0>, H3=<H2,Yf+2,X>,
    Hf=<H3,X+1,H2[Yf+2]>, avl(H,H[X+2],DL-2,S2),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|=
avl(Hf,Hf[Hf[Yf+2]+2],DL-2,S2).

We perform the following right simplifications:

avl(Hf,Hf[<H3,X+1,H2[Yf+2]>[H[X+1]+2]+2],DL-2,S2)

avl(Hf,Hf[H3[H[X+1]+2]+2],DL-2,S2)    (since {X} * {H[X+1]})

avl(Hf,Hf[<H2,H[X+1]+2,X>[H[X+1]+2]+2],DL-2,S2)

avl(Hf,Hf[X+2],DL-2,S2)

avl(Hf,<H3,X+1,H2[H[X+1]+2]>[X+2],DL-2,S2)

avl(Hf,H3[X+2],DL-2,S2)       (since X+1 != X+2)

avl(Hf,<H2,H[X+1]+2,X>[X+2],DL-2,S2)

avl(Hf,H2[X+2],DL-2,S2)       (H[X+1]+2 != X+2 since {X} * {H[X+1]})

avl(Hf,<H1,H[X+1],0>[X+2],DL-2,S2)

avl(Hf,H1[X+2],DL-2,S2)       (since H[X+1] != X+2 since {X} * {H[X+1]})

avl(Hf,<H,X,0>[X+2],DL-2,S2)

avl(Hf,H[X+2],DL-2,S2)                (since X != X+2)

avl(<H3,X+1,H2[H[X+1]+2]>,H[X+2],DL-2,S2)

avl(H3,H[X+2],DL-2,S2), X !in S2

avl(<H2,H[X+1]+2,X>,H[X+2],DL-2,S2), X !in S2

avl(H2,H[X+2],DL-2,S2), X !in S2, H[X+1] !in S2

avl(<H1,H[X+1],0>,H[X+2],DL-2,S2), X !in S2, H[X+1] !in S2

avl(H1,H[X+2],DL-2,S2), X !in S2, H[X+1] !in S2

avl(<H,X,0>,H[X+2],DL-2,S2), X !in S2, H[X+1] !in S2

avl(H,H[X+2],DL-2,S2), X !in S2, H[X+1] !in S2
     (X !in S2 is true since {X} * S2,
      H[X+1] !in S2 is true since {H[X+1]} * S2

avl(H,H[X+2],DL-2,S2)

Implied by LHS

-------------------------------------------------------------------------------

Prove:
Yf=H[X+1], H[Yf]=1, H1=<H,X,0>, H2=<H1,Yf,0>, H3=<H2,Yf+2,X>,
    Hf=<H3,X+1,H2[Yf+2]>, avl(H,H[H[X+1]+2],DL-2,S12),
    S = {X} * {H[X+1]} * S2 * S11 * S12
|=
avl(Hf,Hf[Hf[Yf+2]+1],DL-2,S12)

We perform the following right simplifications:

avl(Hf,Hf[<H3,X+1,H2[H[X+1]+2]>[H[X+1]+2]+1],DL-2,S12)

avl(Hf,Hf[H3[H[X+1]+2]+1],DL-2,S12)   (since {X}*{H[X+1]})

avl(Hf,Hf[<H2,H[X+1]+2,X>[H[X+1]+2]+1],DL-2,S12)

avl(Hf,Hf[X+1],DL-2,S12)              (AIP)

avl(Hf,<H3,X+1,H2[H[X+1]+2]>[X+1],DL-2,S12)

avl(Hf,H2[H[X+1]+2],DL-2,S12)         (AIP)

avl(Hf,<H1,H[X+1],0>[H[X+1]+2],DL-2,S12)

avl(Hf,H1[H[X+1]+2],DL-2,S12)          (since H[X+1] != H[X+1]+2)

avl(Hf,<H,X,0>[H[X+1]+2],DL-2,S12)

avl(Hf,H[H[X+1]+2],DL-2,S12)   (since X != H[X+1]+2 since {X}*{H[X+1]})

avl(<H3,X+1,H2[H[X+1]+2]>,H[H[X+1]+2],DL-2,S12)

avl(H3,H[H[X+1]+2],DL-2,S12), X !in S12

avl(<H2,H[X+1]+2,X>,H[H[X+1]+2],DL-2,S12), X !in S12

avl(H2,H[H[X+1]+2],DL-2,S12), X !in S12, H[X+1] !in S12

avl(<H1,H[X+1],0>,H[H[X+1]+2],DL-2,S12), X !in S12, H[X+1] !in S12

avl(H1,H[H[X+1]+2],DL-2,S12), X !in S12, H[X+1] !in S12

avl(<H,X,0>,H[H[X+1]+2],DL-2,S12), X !in S12, H[X+1] !in S12

avl(H,H[H[X+1]+2],DL-2,S12), X !in S12, H[X+1] !in S12
          (X !in S12 is true since {X}*S12,
           H[X+1] !in S12 is true since {X}*S12)

avl(H,H[H[X+1]+2],DL-2,S12)

Implied by LHS