Difference between revisions of "Void-safe migration guide"
(One intermediate revision by one other user not shown) | |||
Line 4: | Line 4: | ||
==Prepare migration using 6.3 or 6.4 with the compatibility option== | ==Prepare migration using 6.3 or 6.4 with the compatibility option== | ||
− | Compile your code using | + | Compile your code using either 6.3 or 6.4 in compatibility mode. Then apply the following refactorings: |
* Search for callers of <e>{CELL}.default_create</e> and replace it by calling <e>put</e> instead and providing a sensible default value. | * Search for callers of <e>{CELL}.default_create</e> and replace it by calling <e>put</e> instead and providing a sensible default value. | ||
* Search for callers of <e>{READABLE_STRING_8}.make_from_c</e> and <e>{READABLE_STRING_32}.make_from_c</e>. 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 <e>from_c</e>. | * Search for callers of <e>{READABLE_STRING_8}.make_from_c</e> and <e>{READABLE_STRING_32}.make_from_c</e>. 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 <e>from_c</e>. | ||
Line 10: | Line 10: | ||
== Compiling in void-safe mode with 6.4 == | == 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. |
Latest revision as of 11:02, 31 July 2009
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 callingput
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 tofrom_c
. - Search for callers of
{C_STRING}.share_from_pointer
and{C_STRING}.share_from_pointer_and_count
and replace them bymake_shared_from_pointer
andmake_shared_from_pointer_and_count
when used as creation procedure, otherwise although it is ok to leave them as is, we recommend usingset_shared_from_pointer
andset_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.