53: {-@ divide :: Int -> {v:Int| v /= 0} -> Int @-} 54: (Int) -> {VV : (Int) | (VV /= 0)} -> (Int)divide (Int)n 0 = {x2 : [(Char)] | false} -> {x1 : (Int) | false}liquidError {x3 : [(Char)] | ((len x3) >= 0) && ((sumLens x3) >= 0)}"div-by-zero!" 55: divide n d = {x2 : (Int) | (x2 == n)}n x1:(Int) -> x2:(Int) -> {x6 : (Int) | (((x1 >= 0) && (x2 >= 0)) => (x6 >= 0)) && (((x1 >= 0) && (x2 >= 1)) => (x6 <= x1)) && (x6 == (x1 / x2))}`div` {x2 : (Int) | (x2 /= 0)}d

72: {-@ foo :: n:Nat -> {v:Nat | v < n} @-} 73: n:{VV : (Int) | (VV >= 0)} -> {VV : (Int) | (VV >= 0) && (VV < n)}foo {VV : (Int) | (VV >= 0)}n 74: | {x3 : (Int) | (x3 == n) && (x3 >= 0)}n x1:{x8 : (Int) | (x8 >= 0) && (x8 <= n)} -> x2:{x8 : (Int) | (x8 >= 0) && (x8 <= n)} -> {x2 : (Bool) | (((Prop x2)) <=> (x1 > x2))}> {x2 : (Int) | (x2 == (0 : int))}0 = {x3 : (Int) | (x3 == n) && (x3 >= 0)}n x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}- {x2 : (Int) | (x2 == (1 : int))}1 75: | otherwise = x1:{x5 : (Int) | (x5 >= 0)} -> {x3 : (Int) | (x3 >= 0) && (x3 < x1)}foo {x3 : (Int) | (x3 == n) && (x3 >= 0)}n

103: {- foo       :: n:Nat -> {v:Nat | v < n} -}
104: foo n   
105:   | n > 0     = n - 1
106:   | otherwise = foo n
107: 
108: explode = let z = 0
109:           in  (\x -> (2013 `divide` z)) (foo z)

In Java, ML, etc: program spins away, *never hits* divide-by-zero

Unsafe With Lazy Eval ---------------------

122: {- foo       :: n:Nat -> {v:Nat | v < n} -}
123: foo n   
124:   | n > 0     = n - 1
125:   | otherwise = foo n
126: 
127: explode = let z = 0
128:           in  (\x -> (2013 `divide` z)) (foo z)

In Haskell, program *skips* `(foo z)` & hits divide-by-zero! Problem: Divergence -------------------

What is denoted by `e :: {v:Int | 0 <= v}` ?

`e` evaluates to a `Nat`

or **diverges**!

Classical Floyd-Hoare notion of [partial correctness](http://en.wikipedia.org/wiki/Hoare_logic#Partial_and_total_correctness)

Problem: Divergence ------------------- Suppose `e :: {v:Int | 0 <= v}`
**Consider** `let x = e in body` With Eager Evaluation --------------------- Suppose `e :: {v:Int | 0 <= v}`
**Consider** `let x = e in body`

**Can** assume `x` is a `Nat` when checking `body`

But With Lazy Evaluation ------------------------ Suppose `e :: {v:Int | 0 <= v}`
**Consider** `let x = e in body`

**Cannot** assume `x` is a `Nat` when checking e!

Oops. Now what? --------------- **Solution** Only assign *non-trivial* refinements to *non-diverging* terms!

**Require A Termination Analysis** (Oh dear.)

Demo:Disable `"--no-termination" and see what happens! Recap ----- 1. **Refinements:** Types + Predicates 2. **Subtyping:** SMT Implication 3. **Measures:** Strengthened Constructors 4. **Abstract Refinements:* Decouple Invariants 5. **Lazy Evaluation:** Requires Termination 6.

**Termination:** Via Refinements!