#120 Allow \old in assertions meaning the pre-state of a method

[Gary T. Leavens]

As agreed in the jmlspecs-interest newsgroup, we are
changing JML to allow \old() to be used in assertions
and assumptions in the bodies of methods, etc.

Steps to implement this:

- documenting this syntax and semantics in the
reference manual
- create skipped test cases
- change the type checker
- change jmlc

[David Cok]

Logged In: YES
user_id=595682

I presume that you are also intending to allow \old in local
ghost variable declarations and in set statements.

[Gary T. Leavens]

Logged In: YES
user_id=633675

Yes, that seems reasonable as well.

[Gary T. Leavens]

Logged In: YES
user_id=633675

We agreed to the following in the jmlspecs-interest group.

Allow the use of \old(E) and the new, preferred syntax \pre(E)
to
refer to pre-state value of E in an assertion, loop invariant,
etc. inside method bodies (June 2003, 8 Jan 2004, 03 Aug
2004).
We also would add the syntax \old(E, L) to mean the value
of E
at the beginning of the statement labeled by the label L.

We now need someone to implement it... I will add to the
reference manual when I have time.

[Gary T. Leavens]

Logged In: YES
user_id=633675

Clyde Ruby has done the work for type checking and added the
syntax. The documentation has also been updated.

Now what is needed is to modify jmlrac so that it can deal
with both the \old(E) syntax inside method bodies, and also
so that it can deal with the new \old(E, L) and \pre(E)
syntax. These are documented in the reference manual.

[Gary T. Leavens]

Logged In: YES
user_id=633675

This feature request is now about completing the
implementation of using \old() and \pre() in in-line
assertions.

This is needed for the next release of the JML tools (as
it's already documented), so I'm increasing it's
priority. If anyone else can do it, feel free to take it,
as Yoonsik has been too busy to do this so far (although
he plans to do it eventually).