So far
Abstract Refinements decouple invariants from functions
Next
Decouple invariants from data structures
33: module LiquidArray where 34: 35: import Language.Haskell.Liquid.Prelude (liquidAssume, liquidError) 36: 37: {-@ LIQUID "--no-termination" @-} 38: initialize :: Int -> Vec Int
For this talk, implemented as maps from Int to a
49: data Vec a = V (Int -> a)
Parameterize type with two abstract refinements:
63: {-@ data Vec a < dom :: Int -> Prop, 64: rng :: Int -> a -> Prop > 65: = V {a :: i:Int<dom> -> a <rng i>} @-}
dom: domain on which Vec is defined
rng: range and relationship with index
Diverse Vectors by instantiating dom and rng
An alias for segments between I and J
88: {-@ predicate Btwn I V J = I <= V && V < J @-}
Defined between [0..N) mapping each key to itself:
103: {-@ type IdVec N = Vec <{\v -> Btwn 0 v N}, 104: {\k v -> v = k}> 105: Int @-}
Defined between [0..N), with last element equal to 0:
121: {-@ type ZeroTerm N = 122: Vec <{\v -> Btwn 0 v N}, 123: {\k v -> k = N-1 => v = 0}> 124: Int @-}
A vector whose value at index k is either
0 (undefined), or,
kth fibonacci number
139: {-@ type FibV = 140: Vec <{\v -> true}, 141: {\k v -> v = 0 || v = fib k}> 142: Int @-}
empty
set
get
empty a Vector whose domain is false (defined at no key)
168: {-@ empty :: forall <p :: Int -> a -> Prop>. 169: Vec <{v:Int|false}, p> a @-} 170: 171: forall a <p :: GHC.Types.Int a -> Prop>. (Vec <false, \_ VV -> p> a)empty = x1:({v : Int | false} -> {VV : a | false}) -> {v : (Vec <false, \_ VV -> false> {VV : a | false}) | a v == x1}V (({v : Int | false} -> {VV : a | false}) -> (Vec <false, \_ VV -> false> a)) -> ({v : Int | false} -> {VV : a | false}) -> (Vec <false, \_ VV -> false> a)$ {v : Int | false} -> {VV : a | false}\_ -> [Char] -> {VV : a | false}error {v : [Char] | len v >= 0}"empty vector!"
get Key's ValueInput key in domain
Output value in range related with k
191: {-@ get :: forall a <d :: Int -> Prop, 192: r :: Int -> a -> Prop>. 193: key:Int <d> 194: -> vec:Vec <d, r> a 195: -> a<r key> @-} 196: 197: forall a <d :: GHC.Types.Int -> Prop, r :: GHC.Types.Int a -> Prop>. x1:{VV : Int<d> | true} -> (Vec <d, \_ VV -> r> a) -> {VV : a<r x1> | true}get {VV : Int | papp1 d VV}k (V f) = x1:{v : Int | papp1 d v} -> {VV : a | papp2 r VV x1}f {v : Int | papp1 d v && v == k}k
set Key's Valuekey in domain
val in range related with key
vec defined at domain except at key
key
set Key's Value216: {-@ set :: forall a <d :: Int -> Prop, 217: r :: Int -> a -> Prop>. 218: key: Int<d> -> val: a<r key> 219: -> vec: Vec<{v:Int<d>| v /= key},r> a 220: -> Vec <d, r> a @-} 221: 222: forall a <d :: GHC.Types.Int -> Prop, r :: GHC.Types.Int a -> Prop>. x1:{VV : Int<d> | true} -> {VV : a<r x1> | true} -> (Vec <d & VV /= x1, \_ VV -> r> a) -> (Vec <d, \_ VV -> r> a)set {VV : Int | papp1 d VV}key {VV : a | papp2 r VV key}val (V f) = x1:(x2:{v : Int | papp1 d v} -> {VV : a | papp2 r VV x2}) -> {v : (Vec <papp1 d v, \x5 VV -> papp2 r VV x5> a) | a v == x1}V ((x5:{v : Int | papp1 d v} -> {VV : a | papp2 r VV x5}) -> (Vec <papp1 d v, \x11 VV -> papp2 r VV x11> a)) -> (x5:{v : Int | papp1 d v} -> {VV : a | papp2 r VV x5}) -> (Vec <papp1 d v, \x11 VV -> papp2 r VV x11> a)$ \{VV : Int | papp1 d VV}k -> if {v : Int | papp1 d v && v == k}k x1:Int -> x2:Int -> {v : Bool | Prop v <=> x1 == v}== {v : Int | papp1 d v && v == key}key 223: then {VV : a | papp2 r VV key && VV == val}val 224: else x1:{v : Int | papp1 d v && v /= key} -> {VV : a | papp2 r VV x1}f {v : Int | papp1 d v && v == k}k
Loop over vector, setting each key i equal to i:
242: {-@ initialize :: n:Nat -> IdVec n @-} 243: x1:{v : Int | v >= 0} -> (Vec <VV < x1 && 0 <= VV, \k4 VV -> VV == k4> Int)initialize {v : Int | v >= 0}n = x1:{v : Int | v >= 0 && 0 <= v && v <= n} -> (Vec <v >= 0 && v < n && v < x1, \x19 VV -> v == x19 && v >= 0 && v < n && v < x1> Int) -> (Vec <v >= 0 && v < n && 0 <= v, \x8 VV -> v == x8 && v >= 0 && v < n> Int)loop {v : Int | v == (0 : int)}0 (Vec <false, \_ VV -> false> Int)empty 244: where 245: x1:{v : Int | v >= 0 && 0 <= v && v <= n} -> (Vec <v >= 0 && v < n && v < x1, \x19 VV -> v == x19 && v >= 0 && v < n && v < x1> Int) -> (Vec <v >= 0 && v < n && 0 <= v, \x8 VV -> v == x8 && v >= 0 && v < n> Int)loop {VV : Int | VV >= 0 && 0 <= VV && VV <= n}i (Vec <VV >= 0 && VV < n && VV < i, \x1 VV -> VV == x1 && VV >= 0 && VV < n && VV < i> Int)a 246: | {v : Int | v == i && v >= 0 && 0 <= v && v <= n}i x1:Int -> x2:Int -> {v : Bool | Prop v <=> x1 < v}< {v : Int | v == n && v >= 0}n = let (Vec <v >= 0 && v < n && v <= i, \x8 VV -> v == x8 && v >= 0 && v < n && v <= i> {v : Int | v == i && v >= 0 && v < n && 0 <= v})a' = x1:{v : Int | v >= 0 && v < n && v <= i} -> {v : Int | v == x1 && v == i && v >= 0 && v < n && 0 <= v && v <= i} -> (Vec <v /= x1 && v >= 0 && v < n && v <= i, \x25 VV -> v == x25 && v >= 0 && v < n && v <= i> {v : Int | v == i && v >= 0 && v < n && 0 <= v}) -> (Vec <v >= 0 && v < n && v <= i, \x8 VV -> v == x8 && v >= 0 && v < n && v <= i> {v : Int | v == i && v >= 0 && v < n && 0 <= v})set {v : Int | v == i && v >= 0 && 0 <= v && v <= n}i {v : Int | v == i && v >= 0 && 0 <= v && v <= n}i {v : (Vec <v >= 0 && v < n && v < i, \x9 VV -> v == x9 && v >= 0 && v < n && v < i> Int) | v == a}a 247: in 248: x1:{VV : Int | VV >= 0 && 0 <= VV && VV <= n} -> (Vec <VV >= 0 && VV < n && VV < x1, \x2 VV -> VV == x2 && VV >= 0 && VV < n && VV < x1> Int) -> (Vec <VV >= 0 && VV < n && 0 <= VV, \x1 VV -> VV == x1 && VV >= 0 && VV < n> Int)loop ({v : Int | v == i && v >= 0 && 0 <= v && v <= n}ix1:Int -> x2:Int -> {v : Int | v == x1 + x2}+{v : Int | v == (1 : int)}1) {v : (Vec <v >= 0 && v < n && v <= i, \x9 VV -> v == x9 && v >= 0 && v < n && v <= i> {v : Int | v == i && v >= 0 && v < n && 0 <= v}) | v == a'}a' 249: | otherwise = {v : (Vec <v >= 0 && v < n && v < i, \x9 VV -> v == x9 && v >= 0 && v < n && v < i> Int) | v == a}a
Created a Vec (Array) container
Decoupled domain and range invariants from data
Enabled analysis of array segments
Custom array segment program analyses:
Encoded in (abstract) refinement typed API.