liquidhaskell-0.7.0.0: docs/slides/plpv14/lhs/03_HigherOrderFunctions.lhs.markdown
{#hofs}
=========
<div class="hidden">
<pre><span class=hs-linenum> 6: </span><span class='hs-keyword'>module</span> <span class='hs-conid'>Loop</span> <span class='hs-layout'>(</span>
<span class=hs-linenum> 7: </span> <span class='hs-varid'>listSum</span>
<span class=hs-linenum> 8: </span> <span class='hs-layout'>,</span> <span class='hs-varid'>listNatSum</span>
<span class=hs-linenum> 9: </span> <span class='hs-layout'>)</span> <span class='hs-keyword'>where</span>
<span class=hs-linenum>10: </span>
<span class=hs-linenum>11: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Prelude</span>
<span class=hs-linenum>12: </span>
<span class=hs-linenum>13: </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>14: </span><span class='hs-definition'>listNatSum</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyglyph'>[</span><span class='hs-conid'>Int</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span>
<span class=hs-linenum>15: </span><span class='hs-definition'>add</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-keyglyph'>-></span> <span class='hs-conid'>Int</span>
</pre>
</div>
Higher-Order Specifications
---------------------------
Types scale to *Higher-Order* Specifications
<br>
<div class="fragment">
+ map
+ fold
+ visitors
+ callbacks
+ ...
</div>
<br>
<div class="fragment">Very difficult with *first-order program logics*</div>
Higher Order Specifications
===========================
Example: Higher Order Loop
--------------------------
<pre><span class=hs-linenum>48: </span><span class='hs-definition'>loop</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-keyglyph'>-></span> <span class='hs-varid'>α</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>α</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>α</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>α</span>
<span class=hs-linenum>49: </span><a class=annot href="#"><span class=annottext>forall a.
lo:{VV : (Int) | (VV == 0) && (VV >= 0)}
-> hi:{VV : (Int) | (VV >= 0) && (VV >= lo)}
-> a
-> ({VV : (Int) | (VV >= 0) && (VV >= lo) && (VV < hi)} -> a -> a)
-> a</span><span class='hs-definition'>loop</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV == 0) && (VV >= 0)}</span><span class='hs-varid'>lo</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= lo)}</span><span class='hs-varid'>hi</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-varid'>base</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= lo) && (VV < hi)} -> a -> a</span><span class='hs-varid'>f</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 >= 0) && (x4 >= lo) && (x4 <= hi)} -> a -> a</span><span class='hs-varid'>go</span></a> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == 0) && (x4 == lo) && (x4 >= 0)}</span><span class='hs-varid'>lo</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == base)}</span><span class='hs-varid'>base</span></a>
<span class=hs-linenum>50: </span> <span class='hs-keyword'>where</span>
<span class=hs-linenum>51: </span> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= lo) && (VV <= hi)} -> a -> a</span><span class='hs-varid'>go</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= lo) && (VV <= hi)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-varid'>acc</span></a>
<span class=hs-linenum>52: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>x1:{x12 : (Int) | (x12 >= 0) && (x12 >= i) && (x12 >= lo) && (x12 <= hi)}
-> x2:{x12 : (Int) | (x12 >= 0) && (x12 >= i) && (x12 >= lo) && (x12 <= hi)}
-> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}</span><span class='hs-varop'><</span></a> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == hi) && (x4 >= 0) && (x4 >= lo)}</span><span class='hs-varid'>hi</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= lo) && (VV <= hi)} -> a -> a</span><span class='hs-varid'>go</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}</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-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-layout'>)</span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 >= 0) && (x4 >= lo) && (x4 < hi)} -> a -> a</span><span class='hs-varid'>f</span></a> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == acc)}</span><span class='hs-varid'>acc</span></a><span class='hs-layout'>)</span>
<span class=hs-linenum>53: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == acc)}</span><span class='hs-varid'>acc</span></a>
</pre>
<br>
LiquidHaskell infers `f` called with values `(Btwn lo hi)`
Example: Summing Lists
----------------------
<pre><span class=hs-linenum>65: </span><a class=annot href="#"><span class=annottext>forall a. (Num a) => [a] -> a</span><span class='hs-definition'>listSum</span></a> <a class=annot href="#"><span class=annottext>[a]</span><span class='hs-varid'>xs</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{x12 : (Int) | (x12 == 0) && (x12 >= 0)}
-> x2:{x9 : (Int) | (x9 >= 0) && (x9 >= x1)}
-> a
-> ({x6 : (Int) | (x6 >= 0) && (x6 >= x1) && (x6 < x2)} -> a -> a)
-> a</span><span class='hs-varid'>loop</span></a> <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>{x3 : (Int) | (x3 == n) && (x3 == (len xs))}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-num'>0</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 >= 0) && (x3 < n)} -> a -> a</span><span class='hs-varid'>body</span></a>
<span class=hs-linenum>66: </span> <span class='hs-keyword'>where</span>
<span class=hs-linenum>67: </span> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV < n)} -> a -> a</span><span class='hs-varid'>body</span></a> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>\</span><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV < n)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-varid'>acc</span></a> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == acc)}</span><span class='hs-varid'>acc</span></a> <a class=annot href="#"><span class=annottext>x1:a -> x2:a -> {VV : a | (VV == (x1 + x2))}</span><span class='hs-varop'>+</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x4 : [a] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs</span></a> <a class=annot href="#"><span class=annottext>x1:[a] -> {x3 : (Int) | (x3 < (len x1)) && (0 <= x3)} -> a</span><span class='hs-varop'>!!</span></a> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == i) && (x4 >= 0) && (x4 < n)}</span><span class='hs-varid'>i</span></a><span class='hs-layout'>)</span>
<span class=hs-linenum>68: </span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (len xs))}</span><span class='hs-varid'>n</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:[a] -> {x2 : (Int) | (x2 == (len x1))}</span><span class='hs-varid'>length</span></a> <a class=annot href="#"><span class=annottext>{x4 : [a] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs</span></a>
</pre>
<br>
- <div class="fragment">*Function subtyping:* `body` called on `i :: Btwn 0 (llen xs)`</div>
- <div class="fragment">Hence, indexing with `!!` is safe.</div>
<div class="fragment">
<a href="http://goto.ucsd.edu:8090/index.html#?demo=Loop.hs" target= "_blank">Demo:</a> Tweak `loop` exit condition?
</div>
Example: Summing `Nat`s
-----------------------
<br>
<pre><span class=hs-linenum>87: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>listNatSum</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyglyph'>[</span><span class='hs-conid'>Nat</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nat</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>88: </span><a class=annot href="#"><span class=annottext>[{VV : (Int) | (VV >= 0)}] -> {VV : (Int) | (VV >= 0)}</span><span class='hs-definition'>listNatSum</span></a> <a class=annot href="#"><span class=annottext>[{VV : (Int) | (VV >= 0)}]</span><span class='hs-varid'>xs</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{x20 : (Int) | (x20 == 0) && (x20 >= 0)}
-> x2:{x17 : (Int) | (x17 >= 0) && (x17 >= x1)}
-> {x14 : (Int) | (x14 >= 0)}
-> ({x12 : (Int) | (x12 >= 0) && (x12 >= x1) && (x12 < x2)}
-> {x14 : (Int) | (x14 >= 0)} -> {x14 : (Int) | (x14 >= 0)})
-> {x14 : (Int) | (x14 >= 0)}</span><span class='hs-varid'>loop</span></a> <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>{x3 : (Int) | (x3 == n) && (x3 == (len xs))}</span><span class='hs-varid'>n</span></a> <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>{x8 : (Int) | (x8 >= 0) && (x8 < n)}
-> x2:{x5 : (Int) | (x5 >= 0)}
-> {x3 : (Int) | (x3 >= 0) && (x3 >= x2)}</span><span class='hs-varid'>body</span></a>
<span class=hs-linenum>89: </span> <span class='hs-keyword'>where</span>
<span class=hs-linenum>90: </span> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV < n)}
-> acc:{VV : (Int) | (VV >= 0)}
-> {VV : (Int) | (VV >= 0) && (VV >= acc)}</span><span class='hs-varid'>body</span></a> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>\</span><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV < n)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>acc</span></a> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == acc) && (x3 >= 0)}</span><span class='hs-varid'>acc</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> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x4 : [{x7 : (Int) | (x7 >= 0)}] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs</span></a> <a class=annot href="#"><span class=annottext>x1:[{x9 : (Int) | (x9 >= 0)}]
-> {x5 : (Int) | (x5 < (len x1)) && (0 <= x5)}
-> {x9 : (Int) | (x9 >= 0)}</span><span class='hs-varop'>!!</span></a> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == i) && (x4 >= 0) && (x4 < n)}</span><span class='hs-varid'>i</span></a><span class='hs-layout'>)</span>
<span class=hs-linenum>91: </span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (len xs))}</span><span class='hs-varid'>n</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:[{x6 : (Int) | (x6 >= 0)}] -> {x2 : (Int) | (x2 == (len x1))}</span><span class='hs-varid'>length</span></a> <a class=annot href="#"><span class=annottext>{x4 : [{x7 : (Int) | (x7 >= 0)}] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs</span></a>
</pre>
<br>
<div class="fragment" align="center">
---- ---- ---------------------------------------
(+) `::` `x:Int -> y:Int -> {v:Int| v=x+y}`
`<:` `Nat -> Nat -> Nat`
---- ---- ---------------------------------------
</div>
Example: Summing `Nat`s
-----------------------
<br>
<pre><span class=hs-linenum>109: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>listNatSum</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyglyph'>[</span><span class='hs-conid'>Nat</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nat</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>110: </span><span class='hs-definition'>listNatSum</span> <span class='hs-varid'>xs</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>loop</span> <span class='hs-num'>0</span> <span class='hs-varid'>n</span> <span class='hs-num'>0</span> <span class='hs-varid'>body</span>
<span class=hs-linenum>111: </span> <span class='hs-keyword'>where</span>
<span class=hs-linenum>112: </span> <span class='hs-varid'>body</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>\</span><span class='hs-varid'>i</span> <span class='hs-varid'>acc</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>acc</span> <span class='hs-varop'>+</span> <span class='hs-layout'>(</span><span class='hs-varid'>xs</span> <span class='hs-varop'>!!</span> <span class='hs-varid'>i</span><span class='hs-layout'>)</span>
<span class=hs-linenum>113: </span> <span class='hs-varid'>n</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>length</span> <span class='hs-varid'>xs</span>
</pre>
<br>
Hence, verified by *instantiating* `α` of `loop` with `Nat`
<div class="fragment">`Int -> Int -> Nat -> (Int -> Nat -> Nat) -> Nat`</div>
Example: Summing `Nat`s
-----------------------
<br>
<pre><span class=hs-linenum>126: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>listNatSum</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyglyph'>[</span><span class='hs-conid'>Nat</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nat</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>127: </span><span class='hs-definition'>listNatSum</span> <span class='hs-varid'>xs</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>loop</span> <span class='hs-num'>0</span> <span class='hs-varid'>n</span> <span class='hs-num'>0</span> <span class='hs-varid'>body</span>
<span class=hs-linenum>128: </span> <span class='hs-keyword'>where</span>
<span class=hs-linenum>129: </span> <span class='hs-varid'>body</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>\</span><span class='hs-varid'>i</span> <span class='hs-varid'>acc</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>acc</span> <span class='hs-varop'>+</span> <span class='hs-layout'>(</span><span class='hs-varid'>xs</span> <span class='hs-varop'>!!</span> <span class='hs-varid'>i</span><span class='hs-layout'>)</span>
<span class=hs-linenum>130: </span> <span class='hs-varid'>n</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>length</span> <span class='hs-varid'>xs</span>
</pre>
<br>
+ Parameter `α` corresponds to *loop invariant*
+ Instantiation corresponds to invariant *synthesis*
Instantiation And Inference
---------------------------
+ <div class="fragment">Polymorphic instantiation happens *everywhere*</div>
+ <div class="fragment">Automatic inference is crucial</div>
+ <div class="fragment">*Cannot use* unification (unlike indexed approaches)</div>
+ <div class="fragment">*Can reuse* [SMT/predicate abstraction.](http://goto.ucsd.edu/~rjhala/papers/liquid_types.html)</div>
Iteration Dependence
--------------------
**Cannot** use parametric polymorphism to verify:
<br>
<pre><span class=hs-linenum>161: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>add</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-varid'>m</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Nat</span><span class='hs-keyword'>|v=m+n}</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>162: </span><a class=annot href="#"><span class=annottext>n:{VV : (Int) | (VV >= 0)}
-> m:{VV : (Int) | (VV >= 0)}
-> {VV : (Int) | (VV == (m + n)) && (VV >= 0)}</span><span class='hs-definition'>add</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>m</span></a> <span class='hs-keyglyph'>=</span> <span class=hs-error><a class=annot href="#"><span class=annottext>x1:{x24 : (Int) | (x24 == 0) && (x24 >= 0)}
-> x2:{x21 : (Int) | (x21 >= 0) && (x21 >= x1)}
-> {x18 : (Int) | (x18 >= 0) && (x18 >= n)}
-> ({x15 : (Int) | (x15 >= 0) && (x15 >= x1) && (x15 < x2)}
-> {x18 : (Int) | (x18 >= 0) && (x18 >= n)}
-> {x18 : (Int) | (x18 >= 0) && (x18 >= n)})
-> {x18 : (Int) | (x18 >= 0) && (x18 >= n)}</span><span class='hs-varid'>loop</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == m) && (x3 >= 0)}</span><span class='hs-varid'>m</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == n) && (x3 >= 0)}</span><span class='hs-varid'>n</span></a></span><span class=hs-error> </span><span class=hs-error><span class='hs-layout'>(</span></span><span class=hs-error><a class=annot href="#"><span class=annottext>{x11 : (Int) | (x11 >= 0) && (x11 < m)}
-> x2:{x8 : (Int) | (x8 >= 0) && (x8 >= n)}
-> {x5 : (Int) | (x5 > 0) && (x5 > x2) && (x5 > n) && (x5 >= 0)}</span><span class='hs-keyglyph'>\</span></a></span><span class=hs-error><span class='hs-keyword'>_</span></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= n)}</span><span class='hs-varid'>i</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><a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == i) && (x4 >= 0) && (x4 >= n)}</span><span class='hs-varid'>i</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (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>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a></span><span class=hs-error><span class='hs-layout'>)</span></span>
</pre>
<br>
- <div class="fragment">As property only holds after **last** loop iteration...</div>
- <div class="fragment">... cannot instantiate `α` with `{v:Int | v = n + m}`</div>
<div class="fragment">**Problem:** Need *iteration-dependent* invariants...</div>