Invariants of Data Structures


So far

Properties of basic values

e.g. {v:Int | lo <= v && v < hi}

Properties of structures

e.g. {v:[Int] | length v == 1 + length xs}

Invariants of Data Structures


So far

Properties of basic values

e.g. {v:Int | lo <= v && v < hi}

Properties of structures

e.g. {v:[Int] | length v == 1 + length xs}


Next

Invariants of structures

e.g. a Date is valid or a List is sorted

Recall: Properties of Structures




Refined Constructor Types

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

Recall: Properties of Structures


Refined Constructor Types

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

Generalize Properties during Construction

i.e. applying type of [] and (:)


Instantiate Properties during Pattern-Matching

i.e. unapplying type of [] and (:)

Strategy: Encode Invariants in Constructors




Reuse the idea for properties!

Verification works out exactly as before

Strategy: Encode Invariants in Constructors


Reuse the idea for properties!

Verification works out exactly as before


Generalize Invariant during Construction

i.e. applying type of [] and (:)


Instantiate Invariant during Pattern-Matching

i.e. unapplying type of [] and (:)

Invariant: Ordered Pairs

Lets write a type for ordered pairs

data OrdPair = OP {opX :: Int, opY :: Int} -- | Constructing Pairs okPair = OP 2 4 -- legal badPair = OP 4 2 -- illegal -- | Destructing Pairs checkPair (OP a b) | a < b = True | otherwise = impossible "illegal OrdPair!" -- | Refine `OrdPair` to only allow legal pairs where opX < opY {-@ data OrdPair = OP { opX :: Int, opY :: Int} @-}

Exercise: Refine OrdPair to only allow legal pairs where opX < opY

Invariant via Refined Constructors




Reuse Strategy: Refinements Strengthen Constructors!

              OP :: opX:Int -> opY:{v:Int|opX < v} -> OrdPair

Invariant via Refined Constructors



Reuse Strategy: Refinements Strengthen Constructors!

              OP :: opX:Int -> opY:{v:Int|opX < v} -> OrdPair

Invariant Checked At Construction

By applying constructor pre-condition

Invariant via Refined Constructors


Reuse Strategy: Refinements Strengthen Constructors!

              OP :: opX:Int -> opY:{v:Int|opX < v} -> OrdPair

Invariant Checked At Construction

By applying constructor pre-condition


Invariant Instantiated At Pattern-Matching

By unapplying constructor pre-condition

Refined Data: CSV Tables


A datatype to represent Comma-Separated-Value Tables


data Csv = Csv { hdrs :: [String] , rows :: [[Int]] } scores = Csv { hdrs = ["Id", "Midterm", "Final"] , rows = [[ 1 , 25 , 88] ,[ 2 , 27 , 83] ,[ 3 , 19 , 93]] }


A Legal CSV table has rows without missing values


badScores = Csv { hdrs = ["Id", "Midterm", "Final"] , rows = [[ 1 , 88] ,[ 2 , 27 , 83] ,[ 3 , 19 ]] } {-@ data Csv = Csv { hdrs :: [String] , rows :: [[Int]] } @-}

Exercise: Refine Csv so badScores is rejected.

Ordered Lists





Define a list type whose legal values are ordered

Ordered Lists


Define a list type whose legal values are ordered

data OList a = Emp | (:<) { oHd :: a, oTl :: OList a } okList :: OList Int okList = 1 :< 2 :< 3 :< Emp -- legal badList :: OList Int badList = 1 :< 3 :< 2 :< Emp -- illegal {-@ data OList a = Emp | (:<) {oHd :: a, oTl :: OList a} @-}

Exercise: Refine OList so (only) badList is rejected.

Recap: Invariant via Refined Constructors




      OP   :: opX:Int -> opY:{v:Int |opX < v} -> OrdPair  
  
      Csv  :: hdrs:[String] -> [{row:[Int]|len row = len hdrs}] -> Csv
  
      Emp  :: OList a
      (:<) :: oHd:a -> OList {v:a |oHd < v} -> OList a

Recap: Invariant via Refined Constructors


      OP   :: opX:Int -> opY:{v:Int |opX < v} -> OrdPair  
  
      Csv  :: hdrs:[String] -> [{row:[Int]|len row = len hdrs}] -> Csv
  
      Emp  :: OList a
      (:<) :: oHd:a -> OList {v:a |oHd < v} -> OList a

Invariant Checked at Construction and Instantiated at Pattern-Matching

Simply by applying and un-applying refined constructor type!