What's the point of the local variable in Eiffel's attached-statement?

In Eiffel, Void Safety is a way to statically prevent dereferencing uninitialised ("null") objects. The way it works is that first, the object has to be declared as detachable, and then you need to check in an if-block whether the object is actually attached (i.e. has some value) before you can use it.

This is how I have been using it until now:

some_object: detachable TYPE

...

if attached some_object then
  some_object.method
end

Works perfectly fine: Without the attached-check, compiling fails with an "Target of the Object_call might be void" error. However, after actually reading the documentation on Void Safety, I learned that this is actually how it's supposed to look like:

some_object: detachable TYPE

...

if attached some_object as l_some_object then
  l_some_object.method
end

In this form, l_some_object is a variable local to the if-block which points to the same object as some_object but is statically guaranteed to be non-void.

However, I don't see the reason for the existence of this as-clause. As I pointed out above, apparently the original some_object is already statically guaranteed to be non-void within the if-block, so what's the point of introducing another variable?

What are the differences between some_object and l_some_object, apart from the scope?

Solution

Short answer

If some_object is a local variable, there is no point to introduce an object test local l_some_object.

Long answer

The general form of an object test is

attached {SOME_TYPE} expr as var

where {SOME_TYPE} and var are optional. When type ({SOME_TYPE} in the example above) is not used, the object test just checks whether expr is attached or not and assigns its value to var when it is attached.

In theory something like the following could be expected to be void-safe:

if attached expr then
    expr.do_something
end

However this is not allowed in general case because expr might have side effects, so that the second time it is computed, a different value is returned, and this value might be void making the code void-unsafe:

if attached foo then -- On first call function foo returns non-void value.
    foo.do_something -- On second call function foo returns void: BOOM!
end

Another possibility is an intermediate call that changes value of the expression, for example,

if attached attr then -- Attribute attr is attached here.
    bar               -- bar sets attr to Void.
    attr.do_something -- BOOM!
end

If bar sets attribute attr to void (this can be done indirectly), the code is void-unsafe again.

Finally in a multithreading environment another thread may change the value of attr after the check and before its use inside "then" part even without any intermediate feature call:

if attached attr then -- Attribute attr is attached here.
                      -- Another thread sets attr to Void.
    attr.do_something -- BOOM!
end

To prevent these situations, the var part is used. This object test local is read-only and is not affected by an evaluation of the same expression, by any intermediate feature call or by another thread. In other words it is always attached.

Still in some situations an object tests expression is not affected by these factors:

Arguments are read-only, so it is always sufficient to use the short form
```
attached arg
```
and it makes no sense to introduce an object test local because it will always be equal to the argument.
Local variables and Result may only become Void if they are assigned a detachable expression. If there is no such an assignment, the same
```
attached local_var
```
is just fine. However as soon as the local is assigned a detachable expression, it is not considered attached anymore:
```
if attached local_var then
    ... -- OK to use local_var as attached.
    local_var := detachable_expression
    ... -- No guarantees about local_var attachment status.
end
```
If this scenario is not desired, the long form of the object test can be used
```
attached local_var as attached_local_var
```
and it guarantees that attached_local_var is always attached.