Bounded Refinement Types



Relating Abstract Refinements



















Verification of QuickSort (I)

{-@ qsort1 :: xs:[a] -> IList a  @-}
qsort1 []     = []
qsort1 (x:xs) = append1 listLess (x:listGEq)   
  where
    listLess  = qsort1 [y | y <- xs, y <  x]  
           -- :: IList {y:a | y <  x}
    listGEq   = qsort1 [z | z <- xs, z >= x]  
           -- :: IList {y:a | y <  x}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


append1 :: [a] -> [a] -> [a]
append1 []     ys = ys
append1 (x:xs) ys = x:append1 xs ys 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX












Ghost Variables




Good: Bring info in scope for verification!

Bad: Modification of run-time code.


Ugly: Pollute the code.













Verification of append

{-@ append :: x:a 
           -> IList {hd:a | hd < x} 
           -> IList {tl:a | x <= tl} 
           -> IList a                  @-}
append _ []     ws = ws 
append x (y:ys) ws = y:append x ys ws 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Verification requirement:

hdProp  = \hd -> hd < x      -- property of head elements
tlProp  = \tl -> x <= tl     -- property of tail elements
----------------------------------------------------------
recProp = \hd tl -> hd <= tl -- recursive (sorted) list



Abstracting over Properties:

forall hd tl. hdProp hd => tlProp tl => recProp hd tl



Note: Abstract requirement is independent of x!

















Bounds on Abstract Refinements

Turn Requirement: 

forall hd tl. hdProp hd => tlProp tl => recProp hd tl


Into a Bound: Haskell function that relates abstract refinements

{-  bound recProp @-}
recProp hdProp tlProp recProp 
  = \hd tl -> hdProp hd ==> tlProp tl ==> recProp hd tl 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

















Bound Abstraction


{-@ (++) :: forall < hdprop :: a -> Bool
                   , tlprop :: a -> Bool
                   , p :: a -> a -> Bool>.
        {hd :: a < hdprop >|- a< tlprop > <: a < p hd >} 
        [a< hdprop >]< p > -> [a< tlprop >]< p > -> [a]< p > @-}
(++) []      ys = ys
(++) (x:xs) ys = x:(xs ++ ys)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Bound RecProp combines

  • the recursive property p
  • the property of each head hdprop
  • the property of tail elements tlprop















Bound Instantiations

{-@ qsort :: xs:[a] -> IList a  @-}
qsort []     = []
qsort (x:xs) = listLess ++ (x:listGEq)           
          -- :: IList a == [a]<{\hd tl -> hd <= tl}>
  where
    listLess = qsort [y | y <- xs, y < x ]   
          -- :: IList {y:a | y <  x}
    listGEq  = qsort [z | z <- xs, z >= x]   
          -- :: IList {z:a | x <= z}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Abstract Refinement Instantiation: 
recProp = \hd tl -> hd <= tl -- recursive (sort) property
hdProp  = \hd -> hd < x      -- property of head elements
tlProp  = \tl -> x <= tl     -- property of tail elements



Bound Instantiation:

recProp 
  = \hd tl -> hd < x  ==> x <= tl ==>  hd <= tl





















Recap



  1. Refinements: Types + Predicates
  2. Subtyping: SMT Implication
  3. Measures: Specify Properties of Data
  4. Abstract Refinements: Decouple properties from code
  5. Bounded Refinements: Relating Abstract Refinements