Escape mechanism for special keywords (Was: Prefix special keywords by @)

[nhatminhle]

From ckkohl79 on February 06, 2011 03:48:22

The keywords "old" and "result" can conflict with valid variable names. They should be prefixed by a special character that is not valid for variables.

I propose to use a syntax similar to the one in ModernJass, i.e. prefix with "@". See Chapter 5.4 of Johannes' Masters thesis: http://modernjass.sourceforge.net/docs/mastersthesis-johannes_rieken.pdf Examples: @Ensures("@result == @old(peek())")

or (if issue 8 gets through):

@Ensures("@result == @old.peek()")

Original issue: http://code.google.com/p/cofoja/issues/detail?id=9

[nhatminhle]

From nhat.min...@gmail.com on February 06, 2011 06:36:59

As discussed in issue 8 , this was intended and we had quite a bit of discussions about it (taking into account the fact that we started from Modern Jass' code base, we had that syntax at the beginning). It should be seen as a naming convention to honor. It was decided to prioritize the most common case (that is: when you follow the convention) and make it look cleaner rather than ensure that no clash would occur in any case. If this really becomes a problem for somebody (and not just on a theoretical level) and can't be worked around, I think we could think of a way to escape out of these keywords, but that would mean the current unprefixed keywords would remain, as they support the most common usage pattern, and another way to refer to the similarly-named identifiers would be added.

Status: WontFix
Cc: andreasl...@google.com

[nhatminhle]

From ckkohl79 on February 06, 2011 07:09:28

I think syntax consistency is a crucial factor for such a library, and any potential problem should be discussed and solved as soon as possible.

I do not want to find myself in a situation where I'd have to change half of the code because of a change in the future. Remember the problems that Java's "enum" keyword had caused?

[nhatminhle]

From nhat.min...@gmail.com on February 06, 2011 08:28:03

That makes sense. Then let me suggest something then. The problem is that either 'result' or 'old' may conflict with one of the following:

• a method of the current class (old);
• a field of the current class (result);
• a parameter of the current method (result).

The third case is easy to workaround by renaming the parameter; since it's not part of any public interface, that should not be a problem for anyone.

The first two ones could be worked around by enforcing that this.old() and this.result nullify the keywords. (This is not the case currently.) How does this sound?

Summary: Escape mechanism for special keywords (Was: Prefix special keywords by @)
Status: Accepted

[nhatminhle]

From andreasl...@google.com on February 06, 2011 09:16:44

Open source is nice! It is great to see that we start to get very constructive feedback already from the start.

Yeah, we did spend quite a few hours discussing this (; I agree with the resolution: the default case should be without the escape symbol.

If we had to prioritize, I would put things like a jar package higher on the list than this. There is a way to work around: just don't put a contract when there is a clash. This is of course not a good long term solution, but it is also not a show stopper that would prevent you using the framework at all.

[nhatminhle]

From ckkohl79 on February 06, 2011 09:28:41

@nhat. Yes, using "this." as a prefix sounds like a good solution. +1 (You should also allow class names for static references, e.g. MyClass.result)

On the other hand: can you guarantee that there will be no other keywords introduced at a later version?

If I would start using cofoja for a super-big, super-important library, I do not want to find myself trapped in a situation where my pre/post-conditions throw errors or, even worse, don't throw errors where they should.

Example:

@Ensures("!(exception instanceof RuntimeException)")

should be a valid statement if one of my method's arguments is called "exception".

But imagine "exception" becomes a magic keyword in a newer version of cofoja. You want to be able to ensure that no RuntimeException is thrown in that method (this is essentially a use case different from @ThrowEnsures), so the cofoja developers decide to add "exception" as a new keyword. Here the problems begin...

Of course this is a somewhat constructed example, but I am pretty sure that there will be demands to have more than just "old" and "result" as keywords, to be able to more precisely specify pre/post-conditions. Think of "response", "time", "input", "output", "memory", etc.

[nhatminhle]

From nhat.min...@gmail.com on February 06, 2011 11:39:44

This is a good point. While I can't guarantee that there won't be new keywords, the general stance of Cofoja is towards conservativeness in terms of features, so it's quite unlikely in the foreseeable future.

I don't think though that some new syntax would be welcome, but maybe a namespace thing, such as allowing people to use com.google.java.contract. in addition to letting them import it to use the short version, so that if you don't, your code stays valid in future versions of Cofoja.

[nhatminhle]

From nhat.min...@gmail.com on August 17, 2014 14:26:40

Status: WontFix
Cc: -andreasl...@google.com