Support Loop Invariants and Old() Syntax

[DavePearce]

(see also #60, #126)

Currently, support for loop invariants with old() syntax is broken. The minimal test case is something like this:

public export method test():
    &int p = new 1
    //
    for i in 0..1
    where *p == old(*p):
        *p = *p
    //
    assert *p == 1

Observe however, that this variation does pass:

method test(&int p):
    int n = *p
    //
    for i in 0..1
    where *p == old(*p):
        *p = *p
    //
    assert *p == n

The reason is that old(e) when used in loop invariants inside Boogie refers to the heap on entry to the method!

[DavePearce]

Does this variation make sense?

method f(&int p):
    int n = *p
    //
    for i in 0..1
    where *p > old(*p):
        *p = *p + 1
    //
    assert *p > n

[utting]

Isn't that invariant false upon entry to the loop, before *p is updated?

[DavePearce]

Hey Mark,

Yeah, that's what I'm pondering. What is the semantic and how do I say what I want about (i.e. that it increases on every iteration). But, I think you are right here ... the invariant probably doesn't make sense here.