content: ---
  layout: post
  title: "Composing Specifications: Red Black Trees" 
  date: 2014-04-05 16:12
  author: Ranjit Jhala
  published: false 
  comments: true
  external-url:
  categories: measures, abstract-refinements, red-black 
  ---
  
  TODO: **Conjoining Specifications** lamport. 
  TODO: composing, and, for example, 
  TODO: red-black trees.
  
  [Red Black trees][RBTwiki] trees are a classic, cold-war era, 
  data structure used to efficiently represent sets, using trees
  whose nodes are labeled by the set's elements, and additionally, 
  are colored *red* or *black*. 
  
  The key to efficiency is that the the trees be *balanced*. 
  
  Of course, the easiest way to do this is to just add a *height* 
  label and check that the difference of heights at each node is 
  bounded (cf. [AVL trees][AVLTwiki]). But, back in the olden 
  days, every bit counted -- the super cunning thing about 
  Red-Black Trees is that they ensure balancedness, at the 
  throwaway price of a *single bit* per node.
  
  The catch is that the invariants are devilishly tricky.
  
  <!-- more -->
  
  1. **Order:** Each node's value is between those in its left and right subtrees,
  2. **Color:** Each red node's children are colored black,
  3. **Height:** Each root-to-leaf path has the same number of black nodes.
  
  There are ways to encode various subsets of these using 
  GADTs and such, but, like [Appel][RBTappel], I find the 
  encodings rather too clever as they require a variety 
  of different types and constructors to capture each 
  invariant. 
  
  One advantage of refinements is we fix the data type, 
  and can then *pick and choose* which invariants we want
  to verify, and *compose* them, quite trivially, via
  conjunction.
  
  Red Black Trees
  ---------------
  
  Lets start with the basic type describing trees.
  
  \begin{code}
  data RBTree a = Leaf 
                | Node Color a !(RBTree a) !(RBTree a)
                deriving (Show)
  \end{code}
  
  A tree is either a `Leaf` (an empty set) or a `Node c x l r` where:
  
  * `x` is the value at the node, 
  * `l` and `r` are the left and right subtrees, and
  * `c` is either `B` (black) or `R` (red). 
  
  \begin{code}
  data Color    = B -- ^ Black
                | R -- ^ Red
                deriving (Eq,Show)
  \end{code}
  
  Intuitively, the set denoted by a tree is the set of values at 
  the nodes of the tree.
  
  Over the next few posts, we will develop an implementation 
  ([based off this][coqRBT]) of a set library using the `RBTree` 
  datatype. In particular, we will implement the API:
  
  \begin{code} <div/>
  empty  :: RBTree a
  member :: a -> RBTree a -> Bool
  insert :: a -> RBTree a -> RBTree a
  delete :: a -> RBTree a -> RBTree a
  toList :: RBTree a -> [a] 
  \end{code}
  
  and will use LiquidHaskell to *directly* and *compositionally* 
  specify and enforce the various invariants.
  
  Continue to:
  
  * [Order][rbtOrder]
  
  Coming soon:
  
  * Color
  * Height
  * Compose
  
  [rbtOrder]   : /blog/2014/04/07/red-black-order.lhs/ 
  
  <!--
  
  * [Color][rbtColor]
  * [Height][rbtHeight]
  * [Compose][rbtAll]
  
  [rbtColor]   : /blog/2014/04/14/red-black-color.lhs/ 
  [rbtHeight]  : /blog/2014/04/21/red-black-height.lhs/ 
  [rbtCompose] : /blog/2014/04/28/red-black-compose.lhs/
  -->
  