Processing math: 100%

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Refinement Types by Example


Specifications


Property: In-bounds Array Access

Refinement Types by Example


Specifications


Property: In-bounds Array Access

{-@ measure vlen :: Vector a -> Int @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Specifications: Pre-Conditions


What does a function require for correct execution?


{-@ at :: vec:Vector a -> {i:Nat| i < vlen vec} -> a @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Refinement on the function's input type

Specifications: Post-Conditions


What does a function ensure about its result?


{-@ size :: v:Vector a -> {n:Int | n == vlen v} @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Refinement on the function's output type

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Verification: Vector Sum


sum :: Vector Int -> Int
sum v = loop 0
  where
    {-@ loop :: Nat -> Int @-}
    loop i
      | i <= size v = at v i + loop (i + 1)
      | otherwise   = 0
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Oops! What gives?

Verification: Vector Sum

Verification: Vector Sum

Verification Conditions

Truev=00v(A)0in=vlen vi<nv=i+10v(B)0in=vlen vi<nv=i0v<vlen v(C)

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Inference


The more interesting your types get,
the less fun it is to write them down.

                   -- Benjamin Pierce

Inference: Vector Sum


sum' :: Vector Int -> Int
sum' v = loop 0
  where
    {-@ loop :: _ -> _ @-}
    loop i
      | i < size v = at v i + loop (i + 1)
      | otherwise  = 0
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Inference: Vector Sum


Not magic, just Abstract Interpretation

Inference: Vector Sum


Not magic, just Abstract Interpretation

Represent unknown refinements with K() variables ...

... Solve resulting Horn Constraints


[PLDI 2008]

Inference: Vector Sum

Inference: Vector Sum

Horn Constraints

Truev=0K(v)(A)K(i)n=vlen vi<nv=i+1K(v)(B)K(i)n=vlen vi<nv=i0v<vlen v(C)

Inference: Vector Sum


Horn Constraints

Truev=0K(v)(A)K(i)n=vlen vi<nv=i+1K(v)(B)K(i)n=vlen vi<nv=i0v<vlen v(C)


Synthesized Solution

K(v)=0v

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Collections & Higher-Order Functions


Composition >> Recursion!

Collections & Higher-Order Functions


Generic Sequences

range lo hi
  | lo < hi   = lo : range (lo + 1) hi
  | otherwise = []
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

(What's a good type for range?)

Collections & Higher-Order Functions


Fold over Sequences

foldr :: (a -> b -> b-> b -> [a-> b
foldr f b []     = b
foldr f b (x:xs) = f x (foldr f b xs)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Collections & Higher-Order Functions


"Wholemeal" Vector Sum

sum''   :: Vector Int -> Int
sum'' v = foldr add 0 is
  where
    add = \i n -> n + at v i
    is  = range 0 (size v)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Types make refinement inference "just work" ...

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Example: List average

{-@ average :: [Int] -> Int @-}
average xs  = total `div` n
  where
    total   = foldr (+) 0 xs
    n       = length xs
length        :: [a-> Int
length []     = 0
length (_:xs) = 1 + length xs
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Yikes! average requires non-empty lists!

Refinements for Datatypes

Lift (some) functions into specification logic:

{-@ measure length @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

which lets us define a type alias

{-@ type ListNE a = {v:[a] | 0 < length v} @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Now lets go back and fix average ...

Measures Yield Refined Constructors

Lift (some) functions into specification logic:

data [a] where
  []  :: {v:[a] | length v = 0}
  (:) :: a
      -> t:[a]
      -> {v:[a] | length v = 1 + length t}

Where length is uninterpreted in refinement Logic

Example: map over Lists

What's the problem here? (Lets fix it!)

{-@ hwAverage :: ListNE (a, Int) -> Int @-}
hwAverage nxs = average (map snd nxs)
{-@ map :: (a -> b) -> [a] -> [b] @-}
map f []     = []
map f (x:xs) = f x : map f xs
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Refinements for Datatypes


Measures

Specify properties as functions over datatypes

Refinements for Datatypes


Measures

Specify properties as functions over datatypes


Refined Constructors

Instantiate constraints at fold (C ...) & unfold (case-of)

Refinements for Datatypes


Measures

Specify properties as functions over datatypes


Refined Constructors

Instantiate constraints at fold (C ...) & unfold (case-of)


Automate verification of data types

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

loading