search

pashapm / cofoja

Automatically exported from code.google.com/p/cofoja
GNU Lesser General Public License v3.0
0 stars 0 forks source link

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

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
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 reported on code.google.com by ckkohl79 on 6 Feb 2011 at 11:48

GoogleCodeExporter commented 9 years ago 
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.

Original comment by nhat.min...@gmail.com on 6 Feb 2011 at 2:36

GoogleCodeExporter commented 9 years ago 
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?

Original comment by ckkohl79 on 6 Feb 2011 at 3:09

GoogleCodeExporter commented 9 years ago 
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?

Original comment by nhat.min...@gmail.com on 6 Feb 2011 at 4:28

GoogleCodeExporter commented 9 years ago 
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.

Original comment by andreasl...@google.com on 6 Feb 2011 at 5:16

GoogleCodeExporter commented 9 years ago 
@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.

Original comment by ckkohl79 on 6 Feb 2011 at 5:28

GoogleCodeExporter commented 9 years ago 
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.<keyword> 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.

Original comment by nhat.min...@gmail.com on 6 Feb 2011 at 7:39

GoogleCodeExporter commented 9 years ago

Original comment by nhat.min...@gmail.com on 17 Aug 2014 at 9:26