\old \pre \before

[davidcok]

The Shonan JML workshop added \pre and o\old with a label to JML (and \past, which is discussed in #26). These expressions can be used in method contracts, block (statement) contracts, specification statements (e.g. assert), and in loop specifications. We need to resolve their semantics.

\pre -- always means the pre-state of the enclosing method (i.e. the state just before the first statement of the body)

\old -- in a method contract means the pre-state -- (OpenJML) in a block contract, means the pre-state of that contract -- (OpenJML) in a specification statement, means the pre-state of the innermost enclosing block or method contract -- loop contract: ???

\before -- This is a KeY construct -- I'll let a KeY person define it

\old with a label -- always means the state at that label. See issue #37 about labels

[mattulbrich]

According to the jmlrefman: 12.4.2:

An expression of the form \old(Expr) refers to the value that the expression Expr had in the pre-state of a method.

An expression of the form \pre(Expr ) also refers to the value that the expression Expr had in the pre-state of a method. Expressions of this form may only be used in assertions that appear in the bodies of methods (i.e., in assert and assume statements, and in loop invariants and variant functions). That is, such expressions may not be used in specifica- tion cases, and hence may not appear in normal or exceptional postconditions, in history constraints, or in duration and working space clauses.

KeY parses \pre and treats it as a synonym for \old (w/o label).

@flo2702 can probably explain \before best.

[davidcok]

This text was not fully updated when \pre was adopted. The point was to have a distinction between \pre, which always referred to the pre-state of the enclosing method and \old which, when in a contract (including block contracts/refinining contracts/loop specs), referred to the pre-state of the contract.

\old in statements (like assert) refers to the pre-state, but with the addition of block specifications it is convenient to say that it means the pre-state of the enclosing contract.

[flo2702]

@flo2702 can probably explain \before best.

\before is supported on block/loop contracts and on assertions/assumptions by KeY and does exactly what \old is supposed to do according to David's post, whereas \old currently does what \pre is supposed to do.

If this suggestion is adopted, it would thus be very easy for us to rename our \old to \pre and our \before to \old.

[leavens]

David wrote:

This text [section 12.4.2 of the JML Reference Manual] was not fully updated when \pre was adopted. The point was to have a distinction between \pre, which always referred to the pre-state of the enclosing method and \old which, when in a contract (including block contracts/refining contracts/loop specs), referred to the pre-state of the contract.

\old in statements (like assert) refers to the pre-state, but with the addition of block specifications it is convenient to say that it means the pre-state of the enclosing contract.

It does seem more useful to have a distinction between \pre and \old. The distinction given seems sensible to me (and probably also did at the time of the Shonan JML workshop, although my memory is not that good).

[mattulbrich]

It seems that KeY has reinvented that distinction anyway, so we are happy with a unifying naming convention.

Candidate:

• \pre -- always means the pre-state of the enclosing method (i.e. the state just before the first statement of the body)
• \old -- in a method contract means the pre-state, in a block contract, means the pre-state of that contract, in a specification statement, means the pre-state of the innermost enclosing block, loop or method contract.
• \old with a label -- always means the state at that label. See issue #37 about labels
• \before -- This is a KeY construct and will be retired since it coincides with \old then.