XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Specifications: Pre-Conditions
What does a function require for correct execution?
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Refinement on the function's input type
Specifications: Post-Conditions
What does a function ensure about its result?
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Refinement on the function's output type
Refinement Types by Example
Specifications
Verification
Inference
Collections & HOFs
Refinements for Datatypes
Verification: Vector Sum
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Oops! What gives?
Verification: Vector Sum

Verification: Vector Sum

Verification Conditions
True⇒v=0⇒0≤v(A)0≤i∧n=vlen v∧i<n⇒v=i+1⇒0≤v(B)0≤i∧n=vlen v∧i<n⇒v=i⇒0≤v<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
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
True⇒v=0⇒K(v)(A)K(i)∧n=vlen v∧i<n⇒v=i+1⇒K(v)(B)K(i)∧n=vlen v∧i<n⇒v=i⇒0≤v<vlen v(C)
Inference: Vector Sum
Horn Constraints
True⇒v=0⇒K(v)(A)K(i)∧n=vlen v∧i<n⇒v=i+1⇒K(v)(B)K(i)∧n=vlen v∧i<n⇒v=i⇒0≤v<vlen v(C)
Synthesized Solution
K(v)=0≤v
Refinement Types by Example
Specifications
Verification
Inference
Collections & HOFs
Refinements for Datatypes
Collections & Higher-Order Functions
Composition >> Recursion!
Collections & Higher-Order Functions
Generic Sequences
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
(What's a good type for range
?)
Collections & Higher-Order Functions
Fold over Sequences
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Collections & Higher-Order Functions
"Wholemeal" Vector Sum
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Types make refinement inference "just work" ...
Refinement Types by Example
Specifications
Verification
Inference
Collections & HOFs
Refinements for Datatypes
Example: List average
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Yikes! average
requires non-empty lists!
Refinements for Datatypes
Lift (some) functions into specification logic:
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
which lets us define a type alias
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!)
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