Simple Refinement Types

























Simple Refinement Types


Refinement Types = Types + Predicates













Example: Integers equal to 0


{-@ type Zero = {v:Int | v = 0} @-}
{-@ zero :: Zero @-}
zero     =  0
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Refinement types via special comments {-@ ... @-}













Example: Natural Numbers


{-@ type Nat = {v:Int | 0 <= v} @-}
{-@ nats :: [Nat]               @-}
nats     =  [0, 1, 2, 3]
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX














Exercise: Positive Integers


{-@ type Pos = {v:Int | 0 <= v} @-}
{-@ poss :: [Pos]               @-}
poss     =  [0, 1, 2, 3]
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Q: First, can you fix Pos so poss is rejected?


Q: Next, can you modify poss so it is accepted?













Type Checking

{-@ type Pos = {v:Int | 0 < v} @-}

{-@ poss :: [Pos]               @-}
poss     =  [1, 2, 3]


Type Checking Via Implication Checking.

v = 1 => 0 < v 
v = 2 => 0 < v 
v = 3 => 0 < v 













SMT Automates Implication Checking


Eliminates boring proofs ... makes verification practical.














Contracts: Function Types

















Pre-Conditions


{-@ impossible :: {v:_ | false} -> a @-}
impossible msg = error msg
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


No value satisfies false \(\Rightarrow\) no valid inputs for impossible


Program type-checks \(\Rightarrow\) impossible never called at run-time













Exercise: Pre-Conditions


Let's write a safe division function


{-@ type NonZero = {v:Int | v /= 0} @-}
{-@ safeDiv :: Int -> Int -> Int   @-}
safeDiv _ 0 = impossible "divide-by-zero"
safeDiv x n = x `div` n
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Q: Yikes! Can you fix the type of safeDiv to banish the error?













Precondition Checked at Call-Site


avg2 x y   = safeDiv (x + y) 2
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Precondition

{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}


Verifies As

\[{(v = 2) \Rightarrow (v \not = 0)}\]













Precondition Checked at Call-Site


avg        :: [Int-> Int
avg xs     = safeDiv total n
  where
    total  = sum    xs
    n      = length xs         -- returns a Nat
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Rejected as n can be any Nat

\[0 \leq n \Rightarrow (v = n) \not \Rightarrow (v \not = 0)\]



How to talk about list length in logic?













Recap


Refinement Types Types + Predicates


Specify Properties

Via Refined Input- and Output- Types


Verify Properties

Via SMT based Implication Checking













Unfinished Business


How to describe non empty lists?


{-@ avg :: {v:[a]| 0 < length v } -> Pos @-}


Next: How to describe properties of structures [continue...]