Examples: Loop

int i = 0

list xs = Nil

while(*){

xs = Cons(i, xs)

i++

}

---

i = 0

xs = <0>

while (*) {

i++

xs = i ::xs

}

assert head.xs == i //returns AUnknown

(with head.xs and i: [0,∞) )

---

int n

list xs

while !isNil(xs){

xs = xs.tail

n++

}

assert n >= 0

case AUnknown: ATrue (run while loop) | AFalse (straight to assert)