#22 Recursive announce statements with old() expressions fail

[Robert Dyer]

Recursively announcing an event type which contains a contract with old() expressions does not work. The assertions will fail because only the last announcement in the chain will cache it's old expression results. This is due to the old fields in the Contract classes not being stacks. Example:

public void event E {
int c;

requires true
assumes {
establishes old(next.c()) > 3;
}
ensures true
}

public class C {
public static void main(String[] args) {
new H();
new C().m();
}
public void m() {
announce E(3);
}
}

public class H {
public H() {
register(this);
}
static boolean again = true;
public void handler(E next) throws Throwable {
refining establishes old(next.c()) > 3 {
next.invoke();
if (again) {
again = false;
announce E(5);
}
}
}
when E do handler;
}

Expected result: an assertion error (because old(c) > 3 is false based on the first announcement

Observed result: no assertion error (because old(c) > 3 is evaluated using the 2nd value of old(c), which is 5)

[Robert Dyer]

E.java

[Robert Dyer]

C.java

[Robert Dyer]

H.java