Re: [Liberty-eiffel] locals in postcondition

[Cyril ADRIAN]

2014-08-27 22:12 GMT+02:00 Raphael Mack <address@hidden>:

is it allowed to access locals in a postcondition? I don't think it makes much sense...
If we have a closure in the postcondition we get warnings about using the same variable names:
(...)
is this what we want?

I don't know. I am of two minds here.

Obviously when I coded that I did not think of postconditions. On the other hand, even if this is forbidden maybe the local's scope is too "near"?

What do other people think?

Cheers,

Cyril