SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/lang/improved void safety

Improved void safety

General remarks

ECMA Eiffel introduced void safety into the language. The ECMA Eiffel language standard made the promise to eradicate void calls.

The basic idea: There are attached and detachable types. All entities declared with an attached type can never be a void reference. Detachable type entities can be void references, but no call is possible on an entity of detachable type.

The conformance rules guarantee, that the content of a detachable entity cannot be attached to an attached entity.

Before making feature calls on detachable enities, a test of non voidness is necessary (the so called object test).

  t: detachable T
  ...
  if attached t as u then  -- object test local `u' only
                           -- useable within the branch of
                           -- the if statement
     u.some_feature
  else
     ...
  end
 

Before using a detachable entity, an object test has to be made. The object test is a transition point from the "detachable world" to the "attached world". Once in the "attached world", all features can be called.

Usage in linked structures

In many cases, detachable entities can be avoided. However to implement linked structures, detachable entities are necessary.

The following example is a simplified version of a linked list:

  LINKED_LIST
  first_cell    ----->  LINKABLE
                        item
                        next     ---->   LINKABLE
                                         item
                                         next      ---->x

If the reference to `first_cell' of the linked list is void, then the list is empty. Otherwise `first_cell' points to a linkable which contains an element and a (possibly void) reference to the next cell.

  class LINKABLE[G]  feature
      item: G
      next: detachable like Current
      put_next (o: detachable like Current) ...
  end
 
  class LINKED_LIST[G]
  feature {NONE}
     first_cell: detachable LINKABLE[G]
  feature
     is_empty: BOOLEAN
         do
            Result := first_cell = Void
         end
     first: G
         require 
            not is_empty  -- precondition already implies
                          -- that `first_cell' is not void
         do
            check
                attached first_cell as fc -- extra object test necessary
            end
            Result := fc.item
         end
     ...
   end
 

Unneeded verbosity

Due to the rules of void safety much verbosity is used in the feature `first' of LINKED_LIST. Some even argue that this is against the idea of design by contract. In pre void safe Eiffel, the feature `first' looks like

  class LINKED_LIST[G]  feature
     ..
     first: G
         require 
            not is_empty
         do
            Result := first_cell.item
         end
     ...
   end
 

The advantages of the `simpler' version:

Some other critique

Void safety claims to eradicate void calls. And indeed, no "call on void target" exceptions can happen in void safe Eiffel anymore.

However there are many check instructions necessary as in the above example of a linked list. Therefore the "call on void target" exception has been replaced by another exception (remember: the check instructions with an object test cannot be switched off). Therefore the question arised: Is void safe Eiffel really a step forward?

To summarize the critique of void safe Eiffel:

And indeed the ECMA standard promised too much. Void safety cannot be guaranteed at compile time (at least not with standard compiling techniques).

Why void safe Eiffel is a step forward

As pointed out above, void safety cannot be guaranteed at compile time. It is still possible to get exceptions at runtime which are related to void references, even if no "call on void target" can be thrown at runtime any more.

But despite that, void safe Eiffel is a step forward.

Therefore the critique for changing just one type of exception by another one is not justified.

But there remains the critique of unneeded verbosity.

How to overcome unneeded verbosity? The radical solution.

The fundamental question: If void safety cannot be guaranteed at compile time, why should we disallow feature calls on detachable type entities?

We can keep the distinction between attached and detachable types and instruct the runtime

Since we can reduce detachable entities a lot. We can work in the majority of cases with attached entities. If structures need detachable entities, we can still use them but we should restrict its use to the cases where void references are absolutely necessary.

With that solution we get all advantages of void safety and can reduce the unneeded verbosity.

I.e. we treat

   t: detachable T
   ...
   t.some_feature
 

as a shorthand for

   t: detachable T
   ...
   check
      attached t as tt
   end
   tt.some_feature
 

or

   t_det: detachable T
   t_att: T
   ...
   t_att := t_det
 

as a shorthand for

   t_det: detachable T
   t_att: T
   ...
   check
      attached t_det as tt
   end
   t_att := tt
 

The short forms are clear and concise and the "void safe" versions are somewhat difficult to read because of their verbosity and the extra variable.

But there is also a disadvantage of that solution:

The compiler should help us to detect errors as much as possible. The above short versions do not highlight the locations where exceptions can happen. We might use detachable entities without being aware that they can be void references. And the compiler cannot help us, because call on detachable entities are possible with the implicit assertion that they are not void.

How to overcome unneeded verbosity? The intermediate solution.

Let us adopt the radical solution a little bit to get more help from the compiler.

We could allow feature calls on detachable entities only if we give the compiler an assertion that we are sure that they are not void. But we want the assertion to be less verbose than the clumsy check instruction used in ECMA Eiffel. We could e.g. use

   t: detachable T
   ...
   t.attached.some_feature
 

as a shorthand for

   t: detachable T
   ...
   check
      attached t as tt
   end
   tt.some_feature
 

or

   t_det: detachable T
   t_att: T
   ...
   t_att := t_det.attached
 

as a shorthand for

   t_det: detachable T
   t_att: T
   ...
   check
      attached t_det as tt
   end
   t_att := tt
 
 

With that solution the above linked list example looks like

  class LINKABLE[G]  feature
      item: G
      next: detachable like Current
      put_next (o: detachable like Current) ...
  end
 
  class LINKED_LIST[G]
  feature {NONE}
     first_cell: detachable LINKABLE[G]
  feature
     is_empty: BOOLEAN
         do
            Result := first_cell = Void
         end
     first: G
         require 
            not is_empty
         do
            Result := first_cell.attached.item
         end
     ...
   end
 

This code has nearly the same level of verbosity and conciseness as the "non void safe" version, but still enough elements to highlight the transition points between the "detachable world" and the "attached world" and therefore have all advantages of void safe Eiffel without its unneeded verbosity.

This solution can be used in cases of downcast

    t: T
    d: DT   -- DT is a descendant of T
    ...
    d := t.attached {DT}
 

which would read in ECMA Eiffel

    t: T
    d: DT   -- DT is a descendant of T
    ...
    check
       attached {DT} t as dt
    end
    d := dt
 

Discussion

Feel free to comment on that topic at http://sourceforge.net/projects/tecomp/forums/forum/1034481.

 Local Variables: 
 mode: outline
 coding: iso-latin-1
 fill-column: 60
 outline-regexp: "=\\(=\\)*"
 End:
Table of contents

- General remarks

- Usage in linked structures

- Unneeded verbosity

- Some other critique

- Why void safe Eiffel is a step forward

- How to overcome unneeded verbosity? The radical solution.

- How to overcome unneeded verbosity? The intermediate solution.

- Discussion


ip-location