diff --git a/documentation/current/method/void-safe-programming-eiffel/converting-existing-software-void-safety/index.wiki b/documentation/current/method/void-safe-programming-eiffel/converting-existing-software-void-safety/index.wiki index 89f4d8c4..810a3f31 100644 --- a/documentation/current/method/void-safe-programming-eiffel/converting-existing-software-void-safety/index.wiki +++ b/documentation/current/method/void-safe-programming-eiffel/converting-existing-software-void-safety/index.wiki @@ -271,14 +271,14 @@ However, because these attributes are not exported, we may be able to leave them Those exported features which take arguments of the type ARRAY [STRING] which will serve as sequencing or segmenting control also require that the array contain at least one element. For example, the contract for feature segment_start contains these preconditions: - segment_start (nms: ARRAY [STRING_8]) - -- Place segment cursor on the first occurrence of a seqment of list which - -- begins at the current cursor position and - -- terminates in a sequence with names equivalent to and ordered the same as `nms'. - -- If no such sequence exists, then ensure exhausted - require - nms_valid: nms /= Void and then (nms.count > 0) - not_sequencing: not sequence_readable + segment_start (nms: ARRAY [STRING_8]) + -- Place segment cursor on the first occurrence of a seqment of list which + -- begins at the current cursor position and + -- terminates in a sequence with names equivalent to and ordered the same as `nms'. + -- If no such sequence exists, then ensure exhausted + require + nms_valid: nms /= Void and then (nms.count > 0) + not_sequencing: not sequence_readable Because the restriction always exists that a valid sequence_array or segment_array must contain at least one element, it is possible to redesign the implementation of the class such that an empty sequence_array and segment_array could serve the same purpose as a Void one does in the original design. @@ -291,6 +291,18 @@ So the invariant clauses that we saw above would now become: segment_traversal_convention: (segment_array.is_empty) = (not segment_readable) +We already have compiler errors (VJAR's) that point us to those places in which we have code that sets either sequence_array or segment_array to Void. Like this: + + + segment_array := Void + + +These instances need to be changed to attach an empty array, maybe like this: + + + create segment_array.make (1, 0) + + Additionally, some postconditions which reference the implementation features sequence_array and/or segment_array would have to be changed. Looking at the postcondition clauses for segment_start we see that segment_array is expected (or not) to be Void: @@ -317,7 +329,6 @@ To support the "empty array" design, segment_start's postcondition ===Using generic classes=== -===Using '''check''' blocks=== ==Transitioning steps== diff --git a/documentation/current/method/void-safe-programming-eiffel/creating-new-void-safe-project.wiki b/documentation/current/method/void-safe-programming-eiffel/creating-new-void-safe-project.wiki index 305181aa..5d4cc28e 100644 --- a/documentation/current/method/void-safe-programming-eiffel/creating-new-void-safe-project.wiki +++ b/documentation/current/method/void-safe-programming-eiffel/creating-new-void-safe-project.wiki @@ -54,7 +54,7 @@ This setting instructs the compiler to recheck inherited features in descendant As of EiffelStudio version 6.4, the majority of the libraries distributed with EiffelStudio are void-safe. -During a period of transition, there will be different Eiffel configuration files (.ecf's) for non-void-safe and void-safe projects. If you have set the '''Void-safe''' setting to check for void-safety, then when you add a library to your project in EiffelStudio, you will see the void-safe configurations by default. After the transition period, it is expected that there will be only one version of the configuration files for each library. The single configuration files will serve both non-void-safe and void-safe projects. +{{note|During a period of transition, there will be different Eiffel configuration files (.ecf's) for non-void-safe and void-safe projects (for example, base.ecf and base-safe.ecf). If you have set the '''Void-safe''' setting to check for void-safety, then when you add a library to your project in EiffelStudio, you will see only the void-safe configurations by default. After the transition period, it is expected that there will be only one version of each of the configuration files for each library. The single configuration files will serve both non-void-safe and void-safe projects. }} ==Using non-void-safe libraries==