Abstract Refinements {#data} ============================ Recap ----- **So far** Decouple invariants from *functions* <br> <div class="fragment"> **Next** Decouple invariants from *data structures* </div> Decouple Invariants From Data {#vector} ======================================= Example: Vectors ---------------- <div class="hidden"> <pre><span class=hs-linenum>28: </span><span class='hs-keyword'>module</span> <span class='hs-conid'>LiquidArray</span> <span class='hs-keyword'>where</span> <span class=hs-linenum>29: </span> <span class=hs-linenum>30: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Language</span><span class='hs-varop'>.</span><span class='hs-conid'>Haskell</span><span class='hs-varop'>.</span><span class='hs-conid'>Liquid</span><span class='hs-varop'>.</span><span class='hs-conid'>Prelude</span> <span class='hs-layout'>(</span><span class='hs-varid'>liquidAssume</span><span class='hs-layout'>,</span> <span class='hs-varid'>liquidError</span><span class='hs-layout'>)</span> <span class=hs-linenum>31: </span> <span class=hs-linenum>32: </span><span class='hs-keyword'>{-@</span> <span class='hs-conid'>LIQUID</span> <span class='hs-str'>"--no-termination"</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>33: </span> <span class=hs-linenum>34: </span><span class='hs-definition'>fibMemo</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Vec</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-conid'>Vec</span> <span class='hs-conid'>Int</span><span class='hs-layout'>,</span> <span class='hs-conid'>Int</span><span class='hs-layout'>)</span> <span class=hs-linenum>35: </span><span class='hs-definition'>fastFib</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class=hs-linenum>36: </span><span class='hs-definition'>idv</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Vec</span> <span class='hs-conid'>Int</span> <span class=hs-linenum>37: </span><span class='hs-definition'>axiom_fib</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Bool</span> <span class=hs-linenum>38: </span><a class=annot href="#"><span class=annottext>i:(Int) -> {v : (Bool) | (((Prop v)) <=> ((fib i) == (if (i <= 1) then 1 else ((fib (i - 1)) + (fib (i - 2))))))}</span><span class='hs-definition'>axiom_fib</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall a. a</span><span class='hs-varid'>undefined</span></a> <span class=hs-linenum>39: </span> <span class=hs-linenum>40: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>predicate</span> <span class='hs-conid'>AxFib</span> <span class='hs-conid'>I</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>(</span><span class='hs-varid'>fib</span> <span class='hs-conid'>I</span><span class='hs-layout'>)</span> <span class='hs-varop'>==</span> <span class='hs-layout'>(</span><span class='hs-keyword'>if</span> <span class='hs-conid'>I</span> <span class='hs-varop'><=</span> <span class='hs-num'>1</span> <span class='hs-keyword'>then</span> <span class='hs-num'>1</span> <span class='hs-keyword'>else</span> <span class='hs-varid'>fib</span><span class='hs-layout'>(</span><span class='hs-conid'>I</span><span class='hs-comment'>-</span><span class='hs-num'>1</span><span class='hs-layout'>)</span> <span class='hs-varop'>+</span> <span class='hs-varid'>fib</span><span class='hs-layout'>(</span><span class='hs-conid'>I</span><span class='hs-comment'>-</span><span class='hs-num'>2</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <span class='hs-keyword'>@-}</span> </pre> </div> <div class="fragment"> Implemented as maps from `Int` to `a` <br> <pre><span class=hs-linenum>51: </span><span class='hs-keyword'>data</span> <span class='hs-conid'>Vec</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>V</span> <span class='hs-layout'>(</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> </pre> </div> Abstract *Domain* and *Range* ----------------------------- Parameterize type with *two* abstract refinements: <br> <pre><span class=hs-linenum>65: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>data</span> <span class='hs-conid'>Vec</span> <span class='hs-varid'>a</span> <span class='hs-varop'><</span> <span class='hs-varid'>dom</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span><span class='hs-layout'>,</span> <span class=hs-linenum>66: </span> <span class='hs-varid'>rng</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span> <span class='hs-varop'>></span> <span class=hs-linenum>67: </span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>V</span> <span class='hs-layout'>{</span><span class='hs-varid'>a</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>i</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span><span class='hs-varop'><</span><span class='hs-varid'>dom</span><span class='hs-varop'>></span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span> <span class='hs-varop'><</span><span class='hs-varid'>rng</span> <span class='hs-varid'>i</span><span class='hs-varop'>></span><span class='hs-layout'>}</span> <span class='hs-keyword'>@-}</span> </pre> <br> - `dom`: *domain* on which `Vec` is *defined* - `rng`: *range* and relationship with *index* Abstract *Domain* and *Range* ----------------------------- Diverse `Vec`tors by *instantiating* `dom` and `rng` <br> <div class="fragment"> A quick alias for *segments* between `I` and `J` <br> <pre><span class=hs-linenum>90: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>predicate</span> <span class='hs-conid'>Seg</span> <span class='hs-conid'>V</span> <span class='hs-conid'>I</span> <span class='hs-conid'>J</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>(</span><span class='hs-conid'>I</span> <span class='hs-varop'><=</span> <span class='hs-conid'>V</span> <span class='hs-varop'>&&</span> <span class='hs-conid'>V</span> <span class='hs-varop'><</span> <span class='hs-conid'>J</span><span class='hs-layout'>)</span> <span class='hs-keyword'>@-}</span> </pre> </div> Ex: Identity Vectors -------------------- Defined between `[0..N)` mapping each key to itself: <br> <div class="fragment"> <pre><span class=hs-linenum>105: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>IdVec</span> <span class='hs-conid'>N</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>Vec</span> <span class='hs-varop'><</span><span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-conid'>Seg</span> <span class='hs-varid'>v</span> <span class='hs-num'>0</span> <span class='hs-conid'>N</span><span class='hs-layout'>)</span><span class='hs-layout'>}</span><span class='hs-layout'>,</span> <span class=hs-linenum>106: </span> <span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>k</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>v</span><span class='hs-keyglyph'>=</span><span class='hs-varid'>k</span><span class='hs-layout'>}</span><span class='hs-varop'>></span> <span class=hs-linenum>107: </span> <span class='hs-conid'>Int</span> <span class='hs-keyword'>@-}</span> </pre> </div> Ex: Identity Vectors -------------------- Defined between `[0..N)` mapping each key to itself: <br> <pre><span class=hs-linenum>120: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>idv</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>n</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-conid'>IdVec</span> <span class='hs-varid'>n</span><span class='hs-layout'>)</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>121: </span><a class=annot href="#"><span class=annottext>n:{VV : (Int) | (VV >= 0)} -> (Vec <(VV < n) && (0 <= VV), \k4 VV -> (VV == k4)> (Int))</span><span class='hs-definition'>idv</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>n</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall <rng :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, dom :: (GHC.Types.Int)-> Bool>. (i:{x13 : (Int)<dom> | true} -> {x12 : (Int)<rng i> | (x12 > 0) && (x12 >= 0) && (x12 < n)}) -> (Vec <dom, rng> {x12 : (Int) | (x12 > 0) && (x12 >= 0) && (x12 < n)})</span><span class='hs-conid'>V</span></a> <span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV < n)}</span><span class='hs-varid'>k</span></a> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>if</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a> <a class=annot href="#"><span class=annottext>x1:{x12 : (Int) | (x12 >= 0) && (x12 < n) && (0 <= x12) && (x12 <= k)} -> x2:{x12 : (Int) | (x12 >= 0) && (x12 < n) && (0 <= x12) && (x12 <= k)} -> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}</span><span class='hs-varop'><</span></a> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == k) && (x4 >= 0) && (x4 < n)}</span><span class='hs-varid'>k</span></a> <a class=annot href="#"><span class=annottext>x1:(Bool) -> x2:(Bool) -> {x2 : (Bool) | (((Prop x2)) <=> (((Prop x1)) && ((Prop x2))))}</span><span class='hs-varop'>&&</span></a> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == k) && (x4 >= 0) && (x4 < n)}</span><span class='hs-varid'>k</span></a> <a class=annot href="#"><span class=annottext>x1:{x12 : (Int) | (x12 >= 0) && (x12 >= k) && (0 <= x12) && (x12 <= n)} -> x2:{x12 : (Int) | (x12 >= 0) && (x12 >= k) && (0 <= x12) && (x12 <= n)} -> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}</span><span class='hs-varop'><</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == n) && (x3 >= 0)}</span><span class='hs-varid'>n</span></a> <span class=hs-linenum>122: </span> <span class='hs-keyword'>then</span> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == k) && (x4 >= 0) && (x4 < n)}</span><span class='hs-varid'>k</span></a> <span class=hs-linenum>123: </span> <span class='hs-keyword'>else</span> <a class=annot href="#"><span class=annottext>{x2 : [(Char)] | false} -> {x1 : (Int) | false}</span><span class='hs-varid'>liquidError</span></a> <span class=hs-error><a class=annot href="#"><span class=annottext>{x3 : [(Char)] | ((len x3) >= 0) && ((sumLens x3) >= 0)}</span><span class='hs-str'>"eeks"</span></a></span><span class='hs-layout'>)</span> </pre> <br> <div class="fragment"> <a href="http://goto.ucsd.edu:8090/index.html#?demo=Array.hs" target="_blank">Demo:</a>Whats the problem? How can we fix it? </div> Ex: Zero-Terminated Vectors --------------------------- Defined between `[0..N)`, with *last* element equal to `0`: <br> <div class="fragment"> <pre><span class=hs-linenum>142: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>ZeroTerm</span> <span class='hs-conid'>N</span> <span class='hs-keyglyph'>=</span> <span class=hs-linenum>143: </span> <span class='hs-conid'>Vec</span> <span class='hs-varop'><</span><span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-conid'>Seg</span> <span class='hs-varid'>v</span> <span class='hs-num'>0</span> <span class='hs-conid'>N</span><span class='hs-layout'>)</span><span class='hs-layout'>}</span><span class='hs-layout'>,</span> <span class=hs-linenum>144: </span> <span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>k</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>k</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>N</span><span class='hs-comment'>-</span><span class='hs-num'>1</span> <span class='hs-keyglyph'>=></span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>=</span> <span class='hs-num'>0</span><span class='hs-layout'>)</span><span class='hs-layout'>}</span><span class='hs-varop'>></span> <span class=hs-linenum>145: </span> <span class='hs-conid'>Int</span> <span class='hs-keyword'>@-}</span> </pre> </div> Ex: Fibonacci Table ------------------- A vector whose value at index `k` is either - `0` (undefined), or, - `k`th fibonacci number <pre><span class=hs-linenum>161: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>FibV</span> <span class='hs-keyglyph'>=</span> <span class=hs-linenum>162: </span> <span class='hs-conid'>Vec</span> <span class='hs-varop'><</span><span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>true</span><span class='hs-layout'>}</span><span class='hs-layout'>,</span> <span class=hs-linenum>163: </span> <span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>k</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>v</span> <span class='hs-keyglyph'>=</span> <span class='hs-num'>0</span> <span class='hs-varop'>||</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>(</span><span class='hs-varid'>fib</span> <span class='hs-varid'>k</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span><span class='hs-layout'>}</span><span class='hs-varop'>></span> <span class=hs-linenum>164: </span> <span class='hs-conid'>Int</span> <span class='hs-keyword'>@-}</span> </pre> Accessing Vectors ----------------- Next: lets *abstractly* type `Vec`tor operations, *e.g.* <br> - `empty` - `set` - `get` Ex: Empty Vectors ----------------- `empty` returns Vector whose domain is `false` <br> <pre><span class=hs-linenum>190: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>empty</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyword'>forall</span> <span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span><span class='hs-varop'>>.</span> <span class=hs-linenum>191: </span> <span class='hs-conid'>Vec</span> <span class='hs-varop'><</span><span class='hs-keyword'>{v:</span><span class='hs-conid'>Int</span><span class='hs-keyword'>|false}</span><span class='hs-layout'>,</span> <span class='hs-varid'>p</span><span class='hs-varop'>></span> <span class='hs-varid'>a</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>192: </span> <span class=hs-linenum>193: </span><a class=annot href="#"><span class=annottext>forall a <p :: (GHC.Types.Int)-> a-> Bool>. (Vec <false, \_ VV -> p> a)</span><span class='hs-definition'>empty</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>({x4 : (Int) | false} -> {VV : a | false}) -> (Vec <false, \_ VV -> false> {VV : a | false})</span><span class='hs-conid'>V</span></a> <a class=annot href="#"><span class=annottext>(({x9 : (Int) | false} -> {VV : a | false}) -> (Vec <false, \_ VV -> false> {VV : a | false})) -> ({x9 : (Int) | false} -> {VV : a | false}) -> (Vec <false, \_ VV -> false> {VV : a | false})</span><span class='hs-varop'>$</span></a> <a class=annot href="#"><span class=annottext>{x1 : (Int) | false} -> {VV : a | false}</span><span class='hs-keyglyph'>\</span></a><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>[(Char)] -> {VV : a | false}</span><span class='hs-varid'>error</span></a> <a class=annot href="#"><span class=annottext>{x3 : [(Char)] | ((len x3) >= 0) && ((sumLens x3) >= 0)}</span><span class='hs-str'>"empty vector!"</span></a> </pre> <br> <div class="fragment"> <a href="http://goto.ucsd.edu:8090/index.html#?demo=Array.hs" target="_blank">Demo:</a> What would happen if we changed `false` to `true`? </div> Ex: `get` Key's Value --------------------- - *Input* `key` in *domain* - *Output* value in *range* related with `k` <pre><span class=hs-linenum>211: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>get</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyword'>forall</span> <span class='hs-varid'>a</span> <span class='hs-varop'><</span><span class='hs-varid'>d</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span><span class='hs-layout'>,</span> <span class=hs-linenum>212: </span> <span class='hs-varid'>r</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span><span class='hs-varop'>>.</span> <span class=hs-linenum>213: </span> <span class='hs-varid'>key</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-varop'><</span><span class='hs-varid'>d</span><span class='hs-varop'>></span> <span class=hs-linenum>214: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>vec</span><span class='hs-conop'>:</span><span class='hs-conid'>Vec</span> <span class='hs-varop'><</span><span class='hs-varid'>d</span><span class='hs-layout'>,</span> <span class='hs-varid'>r</span><span class='hs-varop'>></span> <span class='hs-varid'>a</span> <span class=hs-linenum>215: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>r</span> <span class='hs-varid'>key</span><span class='hs-varop'>></span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>216: </span> <span class=hs-linenum>217: </span><a class=annot href="#"><span class=annottext>forall a <d :: (GHC.Types.Int)-> Bool, r :: (GHC.Types.Int)-> a-> Bool>. key:{VV : (Int)<d> | true} -> (Vec <d, \_ VV -> r> a) -> {VV : a<r key> | true}</span><span class='hs-definition'>get</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | ((papp1 d VV))}</span><span class='hs-varid'>k</span></a> <span class='hs-layout'>(</span><span class='hs-conid'>V</span> <span class='hs-varid'>f</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{x2 : (Int) | ((papp1 d x2))} -> {VV : a | ((papp2 r VV x1))}</span><span class='hs-varid'>f</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | ((papp1 d x3)) && (x3 == k)}</span><span class='hs-varid'>k</span></a> </pre> Ex: `set` Key's Value --------------------- - <div class="fragment">Input `key` in *domain*</div> - <div class="fragment">Input `val` in *range* related with `key`</div> - <div class="fragment">Input `vec` defined at *domain except at* `key`</div> - <div class="fragment">Output domain *includes* `key`</div> Ex: `set` Key's Value --------------------- <pre><span class=hs-linenum>236: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>set</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyword'>forall</span> <span class='hs-varid'>a</span> <span class='hs-varop'><</span><span class='hs-varid'>d</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span><span class='hs-layout'>,</span> <span class=hs-linenum>237: </span> <span class='hs-varid'>r</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span><span class='hs-varop'>>.</span> <span class=hs-linenum>238: </span> <span class='hs-varid'>key</span><span class='hs-conop'>:</span> <span class='hs-conid'>Int</span><span class='hs-varop'><</span><span class='hs-varid'>d</span><span class='hs-varop'>></span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>val</span><span class='hs-conop'>:</span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>r</span> <span class='hs-varid'>key</span><span class='hs-varop'>></span> <span class=hs-linenum>239: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>vec</span><span class='hs-conop'>:</span> <span class='hs-conid'>Vec</span><span class='hs-varop'><</span><span class='hs-keyword'>{v:</span><span class='hs-conid'>Int</span><span class='hs-varop'><</span><span class='hs-varid'>d</span><span class='hs-varop'>></span><span class='hs-keyword'>| v /= key}</span><span class='hs-layout'>,</span><span class='hs-varid'>r</span><span class='hs-varop'>></span> <span class='hs-varid'>a</span> <span class=hs-linenum>240: </span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Vec</span> <span class='hs-varop'><</span><span class='hs-varid'>d</span><span class='hs-layout'>,</span> <span class='hs-varid'>r</span><span class='hs-varop'>></span> <span class='hs-varid'>a</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>241: </span><a class=annot href="#"><span class=annottext>forall a <d :: (GHC.Types.Int)-> Bool, r :: (GHC.Types.Int)-> a-> Bool>. key:{VV : (Int)<d> | true} -> {VV : a<r key> | true} -> (Vec <d & (VV /= key), \_ VV -> r> a) -> (Vec <d, \_ VV -> r> a)</span><span class='hs-definition'>set</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | ((papp1 d VV))}</span><span class='hs-varid'>key</span></a> <a class=annot href="#"><span class=annottext>{VV : a | ((papp2 r VV key))}</span><span class='hs-varid'>val</span></a> <span class='hs-layout'>(</span><span class='hs-conid'>V</span> <span class='hs-varid'>f</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <span class=hs-error><a class=annot href="#"><span class=annottext>({x6 : (Int) | ((papp1 d x6))} -> {VV : a | ((papp2 r VV key))}) -> (Vec <((papp1 d x3)), \_ VV -> ((papp2 r VV key))> {VV : a | ((papp2 r VV key))})</span><span class='hs-conid'>V</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>(({x13 : (Int) | ((papp1 d x13))} -> {VV : a | ((papp2 r VV key))}) -> (Vec <((papp1 d x10)), \_ VV -> ((papp2 r VV key))> {VV : a | ((papp2 r VV key))})) -> ({x13 : (Int) | ((papp1 d x13))} -> {VV : a | ((papp2 r VV key))}) -> (Vec <((papp1 d x10)), \_ VV -> ((papp2 r VV key))> {VV : a | ((papp2 r VV key))})</span><span class='hs-varop'>$</span></a></span><span class=hs-error> </span><span class=hs-error><span class='hs-keyglyph'>\</span></span><span class=hs-error><a class=annot href="#"><span class=annottext>{VV : (Int) | ((papp1 d VV))}</span><span class='hs-varid'>k</span></a></span><span class=hs-error> </span><span class=hs-error><span class='hs-keyglyph'>-></span></span><span class=hs-error> </span><span class=hs-error><span class='hs-keyword'>if</span></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x3 : (Int) | ((papp1 d x3)) && (x3 == k)}</span><span class='hs-varid'>k</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>x1:{x6 : (Int) | ((papp1 d x6))} -> x2:{x6 : (Int) | ((papp1 d x6))} -> {x2 : (Bool) | (((Prop x2)) <=> (x1 == x2))}</span><span class='hs-varop'>==</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x3 : (Int) | ((papp1 d x3)) && (x3 == key)}</span><span class='hs-varid'>key</span></a></span><span class=hs-error> </span> <span class=hs-linenum>242: </span> <span class=hs-error><span class='hs-keyword'>then</span></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{VV : a | ((papp2 r VV key)) && (VV == val)}</span><span class='hs-varid'>val</span></a></span><span class=hs-error> </span><span class=hs-error> </span><span class=hs-linenum>243: </span> <span class=hs-error><span class='hs-keyword'>else</span></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>x1:{x3 : (Int) | ((papp1 d x3)) && (x3 /= key)} -> {VV : a | ((papp2 r VV x1))}</span><span class='hs-varid'>f</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x3 : (Int) | ((papp1 d x3)) && (x3 == key)}</span><span class='hs-varid'>key</span></a></span> </pre> <br> <div class="fragment"> <a href="http://goto.ucsd.edu:8090/index.html#?demo=Array.hs" target="_blank">Demo:</a> Help! Can you spot and fix the errors? </div> <!-- INSERT tests/pos/vecloop.lhs here AFTER FIXED --> Using the Vector API -------------------- Memoized Fibonacci ------------------ Use `Vec` API to write a *memoized* fibonacci function <br> <div class="fragment"> Using the fibonacci table: <pre><span class=hs-linenum>267: </span><span class='hs-keyword'>type</span> <span class='hs-conid'>FibV</span> <span class='hs-keyglyph'>=</span> <span class=hs-linenum>268: </span> <span class='hs-conid'>Vec</span> <span class='hs-varop'><</span><span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>true</span><span class='hs-layout'>}</span><span class='hs-layout'>,</span> <span class=hs-linenum>269: </span> <span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>k</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-varid'>v</span> <span class='hs-keyglyph'>=</span> <span class='hs-num'>0</span> <span class='hs-varop'>||</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>(</span><span class='hs-varid'>fib</span> <span class='hs-varid'>k</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span><span class='hs-layout'>}</span><span class='hs-varop'>></span> <span class=hs-linenum>270: </span> <span class='hs-conid'>Int</span> </pre> </div> <br> <div class="fragment"> But wait, what is `fib` ? </div> Specifying Fibonacci -------------------- `fib` is *uninterpreted* in the refinement logic <br> <pre><span class=hs-linenum>289: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>measure</span> <span class='hs-varid'>fib</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyword'>@-}</span> </pre> <br> Specifying Fibonacci -------------------- We *axiomatize* the definition of `fib` in SMT ... <br> <pre><span class=hs-linenum>300: </span><span class='hs-definition'>predicate</span> <span class='hs-conid'>AxFib</span> <span class='hs-conid'>I</span> <span class='hs-keyglyph'>=</span> <span class=hs-linenum>301: </span> <span class='hs-layout'>(</span><span class='hs-varid'>fib</span> <span class='hs-conid'>I</span><span class='hs-layout'>)</span> <span class='hs-varop'>==</span> <span class='hs-keyword'>if</span> <span class='hs-conid'>I</span> <span class='hs-varop'><=</span> <span class='hs-num'>1</span> <span class=hs-linenum>302: </span> <span class='hs-keyword'>then</span> <span class='hs-num'>1</span> <span class=hs-linenum>303: </span> <span class='hs-keyword'>else</span> <span class='hs-varid'>fib</span><span class='hs-layout'>(</span><span class='hs-conid'>I</span><span class='hs-comment'>-</span><span class='hs-num'>1</span><span class='hs-layout'>)</span> <span class='hs-varop'>+</span> <span class='hs-varid'>fib</span><span class='hs-layout'>(</span><span class='hs-conid'>I</span><span class='hs-comment'>-</span><span class='hs-num'>2</span><span class='hs-layout'>)</span> </pre> Specifying Fibonacci -------------------- Finally, lift axiom into LiquidHaskell as *ghost function* <br> <pre><span class=hs-linenum>314: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>axiom_fib</span> <span class='hs-keyglyph'>::</span> <span class=hs-linenum>315: </span> <span class='hs-varid'>i</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-keyword'>_</span><span class='hs-keyword'>|((Prop v) <=> (AxFib i))}</span> <span class='hs-keyword'>@-}</span> </pre> <br> <div class="fragment"> **Note:** Recipe for *escaping* SMT limitations 1. *Prove* fact externally 2. *Use* as ghost function call </div> Fast Fibonacci -------------- An efficient fibonacci function <br> <pre><span class=hs-linenum>336: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>fastFib</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>n</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-keyword'>_</span> <span class='hs-keyword'>| v = (fib n)}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>337: </span><a class=annot href="#"><span class=annottext>n:(Int) -> {v : (Int) | (v == (fib n))}</span><span class='hs-definition'>fastFib</span></a> <a class=annot href="#"><span class=annottext>(Int)</span><span class='hs-varid'>n</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>((Vec <false, \x10 VV -> ((x9 == 0) || (x9 == (fib x10)))> (Int)), {x13 : (Int) | (x13 == (fib n))}) -> {x2 : (Int) | (x2 == (fib n))}</span><span class='hs-varid'>snd</span></a> <a class=annot href="#"><span class=annottext>(((Vec <false, \x24 VV -> ((x23 == 0) || (x23 == (fib x24)))> (Int)), {x27 : (Int) | (x27 == (fib n))}) -> {x16 : (Int) | (x16 == (fib n))}) -> ((Vec <false, \x24 VV -> ((x23 == 0) || (x23 == (fib x24)))> (Int)), {x27 : (Int) | (x27 == (fib n))}) -> {x16 : (Int) | (x16 == (fib n))}</span><span class='hs-varop'>$</span></a> <a class=annot href="#"><span class=annottext>(Vec <True, \x18 VV -> ((x17 == 0) || (x17 == (fib x18)))> (Int)) -> x2:(Int) -> ((Vec <True, \x8 VV -> ((x7 == 0) || (x7 == (fib x8)))> (Int)), {x11 : (Int) | (x11 == (fib x2))})</span><span class='hs-varid'>fibMemo</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>forall <rng :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, dom :: (GHC.Types.Int)-> Bool>. (i:{x15 : (Int)<dom> | true} -> {x14 : (Int)<rng i> | ((x14 == 0) || (x14 == (fib n))) && (x14 == 0) && (x14 >= 0)}) -> (Vec <dom, rng> {x14 : (Int) | ((x14 == 0) || (x14 == (fib n))) && (x14 == 0) && (x14 >= 0)})</span><span class='hs-conid'>V</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>(Int) -> {x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-keyglyph'>\</span></a><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == n)}</span><span class='hs-varid'>n</span></a> </pre> <br> <div class="fragment"> - `fibMemo` *takes* a table initialized with `0` - `fibMemo` *returns* a table with `fib` values upto `n`. </div> Memoized Fibonacci ------------------ <pre><span class=hs-linenum>353: </span><a class=annot href="#"><span class=annottext>(Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> (Int)) -> i:(Int) -> ((Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> (Int)), {VV : (Int) | (VV == (fib i))})</span><span class='hs-definition'>fibMemo</span></a> <a class=annot href="#"><span class=annottext>(Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> (Int))</span><span class='hs-varid'>t</span></a> <a class=annot href="#"><span class=annottext>(Int)</span><span class='hs-varid'>i</span></a> <span class=hs-linenum>354: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == i)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x2 : (Bool) | (((Prop x2)) <=> (x1 <= x2))}</span><span class='hs-varop'><=</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a> <span class=hs-linenum>355: </span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall a b <p2 :: a-> b-> Bool>. x1:a -> x2:{VV : b<p2 x1> | true} -> {x3 : (a, b)<p2> | ((fst x3) == x1) && ((snd x3) == x2)}</span><span class='hs-layout'>(</span></a><a class=annot href="#"><span class=annottext>{x2 : (Vec <True, \x7 VV -> ((x6 == 0) || (x6 == (fib x7)))> (Int)) | (x2 == t)}</span><span class='hs-varid'>t</span></a><span class='hs-layout'>,</span> <a class=annot href="#"><span class=annottext>x1:(Bool) -> {x8 : (Int) | (x8 == 1) && (x8 > 0) && (x8 >= i)} -> {x8 : (Int) | ((Prop x1)) && (x8 == 1) && (x8 > 0) && (x8 >= i)}</span><span class='hs-varid'>liquidAssume</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>x1:(Int) -> {x2 : (Bool) | (((Prop x2)) <=> ((fib x1) == (if (x1 <= 1) then 1 else ((fib (x1 - 1)) + (fib (x1 - 2))))))}</span><span class='hs-varid'>axiom_fib</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == i)}</span><span class='hs-varid'>i</span></a><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a><span class='hs-layout'>)</span> <span class=hs-linenum>356: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class=hs-linenum>357: </span> <span class='hs-keyglyph'>=</span> <span class='hs-keyword'>case</span> <a class=annot href="#"><span class=annottext>forall <r :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, d :: (GHC.Types.Int)-> Bool>. x1:{x7 : (Int)<d> | true} -> (Vec <d, \x5 VV -> r x5> (Int)) -> {x6 : (Int)<r x1> | true}</span><span class='hs-varid'>get</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == i)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Vec <True, \x7 VV -> ((x6 == 0) || (x6 == (fib x7)))> (Int)) | (x2 == t)}</span><span class='hs-varid'>t</span></a> <span class='hs-keyword'>of</span> <span class=hs-linenum>358: </span> <span class='hs-num'>0</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>let</span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{VV : (Vec <True, \x1 VV -> ((VV == 0) || (VV == (fib x1)))> (Int)) | (VV == t1)}</span><span class='hs-varid'>t1</span></a><span class='hs-layout'>,</span><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV == n1)}</span><span class='hs-varid'>n1</span></a><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>(Vec <True, \x18 VV -> ((x17 == 0) || (x17 == (fib x18)))> (Int)) -> x2:(Int) -> ((Vec <True, \x8 VV -> ((x7 == 0) || (x7 == (fib x8)))> (Int)), {x11 : (Int) | (x11 == (fib x2))})</span><span class='hs-varid'>fibMemo</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Vec <True, \x7 VV -> ((x6 == 0) || (x6 == (fib x7)))> (Int)) | (x2 == t)}</span><span class='hs-varid'>t</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == i)}</span><span class='hs-varid'>i</span></a><a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}</span><span class='hs-comment'>-</span></a><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a><span class='hs-layout'>)</span> <span class=hs-linenum>359: </span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{VV : (Vec <(VV /= i), \x1 VV -> ((VV == 0) || (VV == (fib x1)))> (Int)) | (VV == t2)}</span><span class='hs-varid'>t2</span></a><span class='hs-layout'>,</span><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV == n2)}</span><span class='hs-varid'>n2</span></a><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>(Vec <True, \x18 VV -> ((x17 == 0) || (x17 == (fib x18)))> (Int)) -> x2:(Int) -> ((Vec <True, \x8 VV -> ((x7 == 0) || (x7 == (fib x8)))> (Int)), {x11 : (Int) | (x11 == (fib x2))})</span><span class='hs-varid'>fibMemo</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Vec <True, \x8 VV -> ((x7 == 0) || (x7 == (fib x8)))> (Int)) | (x3 == t1) && (x3 == t1)}</span><span class='hs-varid'>t1</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == i)}</span><span class='hs-varid'>i</span></a><a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}</span><span class='hs-comment'>-</span></a><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (2 : int))}</span><span class='hs-num'>2</span></a><span class='hs-layout'>)</span> <span class=hs-linenum>360: </span> <a class=annot href="#"><span class=annottext>(Int)</span><span class='hs-varid'>n</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:(Bool) -> (Int) -> {x2 : (Int) | ((Prop x1))}</span><span class='hs-varid'>liquidAssume</span></a> <span class=hs-linenum>361: </span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>x1:(Int) -> {x2 : (Bool) | (((Prop x2)) <=> ((fib x1) == (if (x1 <= 1) then 1 else ((fib (x1 - 1)) + (fib (x1 - 2))))))}</span><span class='hs-varid'>axiom_fib</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == i)}</span><span class='hs-varid'>i</span></a><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == n1) && (x3 == n1)}</span><span class='hs-varid'>n1</span></a><a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}</span><span class='hs-varop'>+</span></a><a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == n2) && (x3 == n2)}</span><span class='hs-varid'>n2</span></a><span class='hs-layout'>)</span> <span class=hs-linenum>362: </span> <span class='hs-keyword'>in</span> <a class=annot href="#"><span class=annottext>forall a b <p2 :: a-> b-> Bool>. x1:a -> x2:{VV : b<p2 x1> | true} -> {x3 : (a, b)<p2> | ((fst x3) == x1) && ((snd x3) == x2)}</span><span class='hs-layout'>(</span></a><a class=annot href="#"><span class=annottext>forall <r :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, d :: (GHC.Types.Int)-> Bool>. x1:{x13 : (Int)<d> | true} -> {x12 : (Int)<r x1> | true} -> (Vec <d & (x8 /= x1), \x10 VV -> r x10> (Int)) -> (Vec <d, \x4 VV -> r x4> (Int))</span><span class='hs-varid'>set</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == i)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == n)}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Vec <(x5 /= i), \x9 VV -> ((x8 == 0) || (x8 == (fib x9)))> (Int)) | (x3 == t2) && (x3 == t2)}</span><span class='hs-varid'>t2</span></a><span class='hs-layout'>,</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == n)}</span><span class='hs-varid'>n</span></a><span class='hs-layout'>)</span> <span class=hs-linenum>363: </span> <span class='hs-varid'>n</span> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>{x2 : ({x7 : (Vec <True, \x12 VV -> ((x11 == 0) || (x11 == (fib x12)))> (Int)) | (x7 == t)}, {x16 : (Int) | (x16 == (fib i)) && (x16 /= 0)})<\_ VV -> (x16 == (fib i)) && (x16 /= 0)> | ((fst x2) == t)}</span><span class='hs-layout'>(</span></a><a class=annot href="#"><span class=annottext>{x2 : (Vec <True, \x7 VV -> ((x6 == 0) || (x6 == (fib x7)))> (Int)) | (x2 == t)}</span><span class='hs-varid'>t</span></a><span class='hs-layout'>,</span> <a class=annot href="#"><span class=annottext>{x3 : (Int) | ((x3 == 0) || (x3 == (fib i)))}</span><span class='hs-varid'>n</span></a><span class='hs-layout'>)</span> </pre> Memoized Fibonacci ------------------ - `fibMemo` *takes* a table initialized with `0` - `fibMemo` *returns* a table with `fib` values upto `n`. <br> <pre><span class=hs-linenum>375: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>fibMemo</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>FibV</span> <span class=hs-linenum>376: </span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>i</span><span class='hs-conop'>:</span><span class='hs-conid'>Int</span> <span class=hs-linenum>377: </span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-conid'>FibV</span><span class='hs-layout'>,</span><span class='hs-keyword'>{v:</span><span class='hs-conid'>Int</span> <span class='hs-keyword'>| v = (fib i)}</span><span class='hs-layout'>)</span> <span class='hs-keyword'>@-}</span> </pre> Recap ----- Created a `Vec` container Decoupled *domain* and *range* invariants from *data* <br> <div class="fragment"> Previous, special purpose program analyses - [Gopan-Reps-Sagiv, POPL 05](link) - [J.-McMillan, CAV 07](link) - [Logozzo-Cousot-Cousot, POPL 11](link) - [Dillig-Dillig, POPL 12](link) - ... Encoded as instance of abstract refinement types! </div>