Void-safe migration guide

Migrating your code to be void-safe is quite easy if you follow the recommendations presented in this document.

Prepare migration using 6.3 or 6.4 with the compatibility option

Compile your code using either 6.3 or 6.4 in compatibility mode. Then apply the following refactorings:

• Search for callers of {CELL}.default_create and replace it by calling put instead and providing a sensible default value.
• Search for callers of {READABLE_STRING_8}.make_from_c and {READABLE_STRING_32}.make_from_c. If you are using them as part of a creation instruction or a creation expression then nothing to be done. Otherwise we recommend you to replace the call by a call to from_c.
• Search for callers of {C_STRING}.share_from_pointer and {C_STRING}.share_from_pointer_and_count and replace them by make_shared_from_pointer and make_shared_from_pointer_and_count when used as creation procedure, otherwise although it is ok to leave them as is, we recommend using set_shared_from_pointer and set_shared_from_pointer_and_count.

Compiling in void-safe mode with 6.4

Some suggestions for converting to void safe (incomplete)

1. Calls on void target:

It is true that the probability that a void target will escape into production is low (although not zero). But, if void safe Eiffel would work as advertised, all potential void target calls are caught at compile time. That is still a quantum leap from testing to proving. (However, to me it seems that there might still be a problem of runtime exceptions with an object test in a check instruction; see discussion below).

2. CELL[G]?

<<Issue: Attached types don't necessarily have default values, so we might end up duplicating some generic classes. For example we want CELL to have `default_create' as creation procedure when the actual generic parameter is detachable. But CELL cannot declare `default_create' as creation procedure anymore because the actual generic parameter might be attached. So we have to write a new class DETACHABLE_CELL where `item' is declared as 'detachable G' if we want to have `default_create' as creation procedure. The fear is that we will have to duplicate many generic classes like that to accommodate the cases of detachable and attached actual generic parameters.>>

We certainly don't want to have CELL[G] and DETACHABLE_CELL[G]. That would be a step backward in code reuse. The core of CELL[G] is

 class CELL[G] .... feature
    item: G assign put
    put (e: G)   do item := e end
 end

It is a very simple class. Polluting it with stable attributes and a lot of assertions is certainly not the goal. Let's assume for a moment that there is NO rule that requires a `default_create" clause. Then, a void safe version of CELL[G] might look as follows:

 class CELL[G] create put feature
    item: G  assign put
    put (e: G)  do item := e end
 end

and this version is usable for attached and detachable actual generics.

 cell: CELL[SOME_TYPE]
 ...
 create cell.put (some_value)

 cell: CELL[detachable SOME_TYPE]
 ...
 create cell.put (Void)

The above works in ES6.4.

[What about where you want CELL to be expanded? Currently ECMA requires all expanded classes to provide a default_create (this is how it is in ES6.4 currently as well, so far as I can see). If the class does not have a reasonable default_value (as in the case of CELL[G]) then the requirement to have a default_create becomes a liability. So the suggestion is to drop this requirement for a default_create in expanded classes and we can use the above pattern equal well for CELL reference as for CELL expanded!I am assuming that there is no problem in writing a compiler that can distinguish between where there is a default_create (and thus the object self-initializes) and one where it is missing and an explicit creation must be used.]

3. Static void safety or runtime exceptions?

I was originally under the impression that the CAPs in ECMA Eiffel would give us full static void safety as an improvement over "call on void target" exceptions at runtime But it seems that actual static void safety still requires a theorem prover. This is because in void safe Eiffel there remain assertions of the type

 v: detachable SOME_TYPE
 ...
 check {x: SOME_TYPE} v end
 x.some_feature

These type of check instructions cannot be switched off. They have to be checked at runtime and the runtime system has to throw an exception if the assertion is not valid (at least until we have an actual theorem prover).

It may be that such check instructions are rarely necessary and if they are necessary they actually have added value and are not clutter. But this requires some changed coding patterns and the use of detachable types only if absolutely necessary.

First of all consider that in non-void safe Eiffel each statement of the form

 v.some_feature

is actually

 check {x:SOME_TYPE} v end
 x.some_feature

[The above syntax is not yet supported in ES6.4]

The implicit runtime check has been made explicit for detachable entities or expressions. And yes, one has to admit that writing it explicitly is more typing than before.

A simple example of a necessary detachable type is a linked list.

 class LINKABLE[G]  inherit CELL[G] create put feature
   next: detachable like Current
   put_next (nxt: detachable like Current)  do next := nxt end
 end

 class LINKED_LIST[G] feature {NONE}
   first_cell: detachable LINKABLE[G]
 feature
   is_empty: BOOLEAN
      do Result := first_cell = Void  end
   count: INTEGER
   first: G
      require
         not is_empty
      do
         check {c: LINKABLE[G]} first_cell end  -- #1
         Result := c.item
      end
   item (i: INTEGER): G
      require
         0 <= i
         i < count
      local
         j: INTEGER
         c: detachable LINKABLE[G]
         from
            j := 0
            c := first_cell
         invariant
            0 <= j
            j <= i
            c /= Void
         until
            j = i
         loop
            check c /= Void end  -- #2
            c := c.next
            j := j + 1
         end
      end
   extend_front (e: G)
      local
         new_cell: LINKABLE[G]
      do
         create new_cell.put (e)
         new_cell.put_next (first_cell)
         first_cell := new_cell
         count := count + 1
      ensure
         count = old count + 1
         first ~ e
      end
 end

Good Eiffel programmers might not write the check instructions #1 and #2 in non void safe Eiffel. They know that they are true. One who is not so sure might write them thinking "I am pretty sure that they are true. But just in case that I am wrong I want the runtime to check it for me during testing".

Whatever the case, the above object test scenarios are not covered by CAPs and so one may still have runtime void target exceptions. Perhaps the compiler should warn any such object test that is not covered by a CAP!

It is true that void safe Eiffel requires us to make assumptions about "attachedness" explicit through proper check instructions. But theses check instruction are necessary only at the "transition points" between detachable and attached entities. If the first rule "Use attached types whenever possible" is followed, such transition points will not occur very often.

Summary:

1. Use attached types whenever possible.

2. Don't make `default_create' available if your class does not have a reasonable default value. For generic classes this is often the case if the actual generic can be attached or detachable.

3. Provide proper check instructions at the transition points between detachable and attached entities, but minimize these transition points.

4. Runtime checks are only necessary at the transition points (which is a small percentage of all feature calls). Therefore void safe Eiffel will lead to more reliable software. If the compiler issues a warning then that is even better.

5. There is a price to pay to get void safety. More explicit creations and some more check instructions than before.