Flow Typing and Loop Invariants

[DavePearce]

The following fails because of flow typing:

function create(nat size, nat value) -> nat[]:
    int[] r = [0; size]
    nat i = 0
    while i < |r| where r is nat[]:
        r[i] = value
        i = i + 1
    return r