built-in labels for \old

[davidcok]

the 2-argument \old expression includes a label and expression and means the value of the expression when evaluated in the state at that label. The label has to be in scope at the location of the expression.

The question here is whether it is useful to have some language-defined labels. 1) Should there be any such labels? (I vote yes) 2) How should they be spelled? In particular do they begin with a backslash? (I'm neutral) 3) What labels should there be?

I would advocate for at least \Pre (or Pre) -- the pre-stae of the enclosing method \Here or Here - the state at the position of the \old expression \Old or Old - pre-state of contract or innermost enclosing contract

Here are other candidates (cf ACSL): Post -- post-state of enclosing contract (only permitted in a postcondition clause) Init -- state before call to main (i.e. after static initialization) LoopEntry - state prior to first loop entry (but after loop initialization in for-statements) -- in scope for loop specifications LoopCurrent - state at the beginning of the current loop iteration (after the loop test and incrementing the loop variable) -- in scope for loop specifications

[mattulbrich]

Ad 1. I vote Yes

Ad 2. Also neutral. I notice the idea of using capital initial letters. Seems sensible. Backslash would be safer wrt. name clashes.

Ad 3. Pre seems redundant since that is the original meaning of \old. Here is very useful specially when nesting. LoopEntry and LoopCurrent definitely have their application cases. I do remember introducing ghost variables for exactly these purposes.

[leavens]

1. I also agree that having some pre-defined labels is a good idea.
2. I think we should go with the syntax that we would use for actual Java labels, such as PreState and Here, in the interest of regularity. The downside of that decision is that such labels might be confused with labels that the programmer chooses (particularly "Here"), but if desired, the specifier can add new labels to the code to clarify the situation.
3. I agree that a default label like PreState seems redundant if we have \pre().

We could always add other pre-defined labels if we need them. But for now I would leave the ones from ACSL out.

[davidcok]

But having Pre (or PreState) allows a uniform desugaring to 2-argument \old functions, even if redundant.

[leavens]

Yes, I agree, @davidcok, regularity would be nice in terms of being able to uniformly desugar these into the 2-argument form.

[mattulbrich]

class Here {} would not be a syntax error, but the class would take precedence over the label, right? I am happy with this. Sounds like a consensus modulo minor subtleties.

[davidcok]

labels are in a different namespace from other program names, so there is no conflict in MU's example. There is only potential conflict with Java labels the user might introduce. Using an initial uppercase for pre-defined labels should minimize that.

So, to start with: Here, Pre, Old and acknowledging that the meaning of \old is a change for KeY, per #46.

[mattulbrich]

On 07.01.22 14:45, David Cok wrote:

labels are in a different namespace from other program names, so there is no conflict in MU's example. There is only potential conflict with Java labels the user might introduce. Using an initial uppercase for pre-defined labels should minimize that.

Good to know!

So, to start with: Here, Pre, Old and acknowledging that the meaning of \old is a change for KeY, per #46.

We will feel better when we are with the standard once again.

[davidcok]

Sorry - per #36, not #46