13_RedBlack.lhs


Red-Black Trees
===============


<div class="hidden">

\begin{code}
{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--diff"           @-}

module RBTree (ok, bad1, bad2) where

import Language.Haskell.Liquid.Prelude

ok, bad1, bad2 :: RBTree Int

---------------------------------------------------------------------------
-- | Specifications -------------------------------------------------------
---------------------------------------------------------------------------

-- | Red-Black Trees
{-@ type RBT a    = {v: RBTree a | isRB v && isBH v } @-}

{-@ measure isRB        :: RBTree a -> Prop
    isRB (Leaf)         = true
    isRB (Node c x l r) = isRB l && isRB r && (c == R => (IsB l && IsB r))
  @-}

-- | Almost Red-Black Trees
{-@ type ARBT a    = {v: RBTree a | isARB v && isBH v} @-}

{-@ measure isARB        :: (RBTree a) -> Prop
    isARB (Leaf)         = true 
    isARB (Node c x l r) = (isRB l && isRB r)
  @-}

-- | Color of a tree
{-@ measure col         :: RBTree a -> Color
    col (Node c x l r)  = c
    col (Leaf)          = B
  @-}

{-@ measure isB        :: RBTree a -> Prop
    isB (Leaf)         = false
    isB (Node c x l r) = c == B 
  @-}

{-@ predicate IsB T = not (col T == R) @-}

-- | Black Height
{-@ measure isBH        :: RBTree a -> Prop
    isBH (Leaf)         = true
    isBH (Node c x l r) = (isBH l && isBH r && bh l = bh r)
  @-}

{-@ measure bh        :: RBTree a -> Int
    bh (Leaf)         = 0
    bh (Node c x l r) = bh l + if (c == R) then 0 else 1 
  @-}


-- | Binary Search Ordering
{-@ data RBTree a = Leaf
      | Node { c     :: Color
             , key   :: a
             , left  :: RBTree ({v:a | v < key})
             , right :: RBTree ({v:a | key < v}) } @-}
\end{code}

</div>



 {#asdad}
---------

<img src="../img/RedBlack.png" height=300px>

+ <div class="fragment">**Color Invariant:** `Red` nodes have `Black` children</div>
+ <div class="fragment">**Height Invariant:** Number of `Black` nodes equal on *all paths*</div>
+ <div class="fragment">**Order Invariant:** Left keys < root < Right keys </div>


Basic Type 
----------

\begin{code}
data Color = R | B

data RBTree a = Leaf
              | Node { c     :: Color
                     , key   :: a
                     , left  :: RBTree a 
                     , right :: RBTree a }
\end{code}


1. Color Invariant 
------------------

`Red` nodes have `Black` children

<div class="fragment">
\begin{spec}
measure isRB        :: Tree a -> Prop
isRB (Leaf)         = true
isRB (Node c x l r) = c == R => (isB l && isB r)
                      && isRB l && isRB r
\end{spec}
</div>

<div class="fragment">
where 
\begin{spec}
measure isB         :: Tree a -> Prop 
isB (Leaf)          = true
isB (Node c x l r)  = c == B
\end{spec}
</div>


1. *Almost* Color Invariant 
---------------------------

<br>

Color Invariant **except** at root. 

<br>

<div class="fragment">
\begin{spec}
measure isAlmost        :: RBTree a -> Prop
isAlmost (Leaf)         = true
isAlmost (Node c x l r) = isRB l && isRB r
\end{spec}
</div>

<!-- BEGIN CUT END CUT -->

2. Height Invariant
-------------------

Number of `Black` nodes equal on **all paths**

<div class="fragment">
\begin{spec} 
measure isBH        :: RBTree a -> Prop
isBH (Leaf)         =  true
isBH (Node c x l r) =  bh l == bh r 
                    && isBH l && isBH r 
\end{spec}
</div>

<div class="fragment">

where

\begin{spec}
measure bh        :: RBTree a -> Int
bh (Leaf)         = 0
bh (Node c x l r) = bh l 
                  + if c == R then 0 else 1
\end{spec}
</div>

3. Order Invariant
------------------

**Binary Search Ordering**

\begin{spec}
data RBTree a
  = Leaf
  | Node { c     :: Color
         , key   :: a
         , left  :: RBTree {v:a | v < key}
         , right :: RBTree {v:a | key < v}
         }
\end{spec}


Valid Red-Black Trees
---------------------

<br>

**Conjoining Specifications**

<br>

\begin{spec}
-- | Red-Black Trees
type RBT a  = {v:RBTree a|isRB v && isBH v}

-- | Almost Red-Black Trees
type ARBT a = {v:RBTree a|isAlmost v && isBH v}
\end{spec}

<br>

[Details](https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/RBTree.hs)

Ex: Satisfies Invariants
-------------------------

<img src="../img/rbtree-ok.png" height=200px>

<br>

\begin{code}
{-@ ok   :: RBT Int @-}
ok = Node R 2 
          (Node B 1 Leaf Leaf)
          (Node B 3 Leaf Leaf)
\end{code}


Ex: Violates Order Invariant
----------------------------

<img src="../img/rbtree-bad1.png" height=200px>

<br>

\begin{code}
{-@ bad1 :: RBT Int @-}
bad1 = Node R 1
          (Node B 2 Leaf Leaf)
          (Node B 3 Leaf Leaf)
\end{code}

Ex: Violates Color Invariant
----------------------------

<img src="../img/rbtree-bad2.png" height=200px>

<br>

\begin{code}
{-@ bad2 :: RBT Int @-}
bad2 = Node  R 2
         (Node R 1 Leaf Leaf)
         (Node B 3 Leaf Leaf)
\end{code}


Verified Red-Black Operations 
-----------------------------

<br>

**Types Verify Correctness of**

<br>

+ Insertion

+ Deletion

+ Lookup ...

<br>

**In presence of rotation & rebalancing** [[details]](https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/RBTree.hs)