semantic of having to declare an attached local into detachable attribute with mandatory check

Question

As far as I understood the check with then is mandatory.

So what is the semantic of having to declare a local to avoid compiling error (object could be void)?

detachable dog: DOG

take_a_walk
    do
        check
            attached_dog: attached dog as l_dog
        then
            leash (l_dog) -- why not just leash (dog)?
            walk
        end
    end     

Answer 1

There are 2 major reasons why an attribute of a detachable type cannot be used after its voidness test as attached:

1. As soon as a sequence of calls after the voidness test involves more than just a single call, it becomes next to impossible to figure out whether the attribute is still attached or not. Here is an example with an attribute x:

   if attached x then
       foo
       x.bar
   end
   

   The call to foo can assign Void to attribute x. Therefore, the call x.bar is now unsafe (can lead to the call on Void target). In language terms, x should be considered as detachable regardless of the earlier voidness test. (Compare this to the use when x is a local variable: the call to foo cannot change x, and the call x.bar is fine.)

2. In a multi-threaded environment, the value of an attribute could be changed under the hood. Let's consider the following example with an attribute x:

   if attached x then
       x.bar
   end
   

   Here is an execution sequence that leads to the problem:

   • Attribute x is tested for voidness and attached x gives True.
   • Another thread gets control and executes x := Void.
   • The control is returned to the original thread, and the call x.bar is performed on Void target.

As in example 1, if x were a local variable, the code would be just fine.

All the reasoning above assumes that an attribute can be assigned Void. What if this is false, i.e. when such assignments are impossible? In such a case the attribute can be marked as stable:

x: detachable FOO
    note
        option: stable
    attribute
    end

Then, in terms of void safety, the attribute behaves as a local variable, all the code snippets above become valid and compile without an error.