Author:halw

Date:2009-05-20T20:54:13.000000Z


git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@223 abb3cda0-5349-4a8f-a601-0c33ac3a8c38

documentation/current/method/void-safe-programming-eiffel/converting-existing-software-void-safety/index.wiki

@@ -181,6 +181,11 @@ So the least impact to this routine will be to declare its type as <code>detacha
 
 The same change is made in other routines that can return void by design, particularly including a routine called <code>value_at_first</code>, which gets our attention next.
 
+The case of <code>at_first</code> offered us an opportunity to redesign (or not). We might have been able to leave <code>at_first</code> attached. After all, in void-safe software, the fewer <code>detachable</code>s, the better. Maybe we could devise a way, possibly through preconditions and other queries, that would guarantee that <code>at_first</code> attempts to execute only when it can return a value. 
+
+But <code>at_first</code> is an exported query, so a consequence of such a change in the class design is that it would affect the class interface in such a way that existing clients would have to be modified to comply. In other words, it would be a "breaking" change. 
+
+
 ===Source of assignment does not conform to target===
 
 The change to <code>at_first</code> satisfies the VEVI issue in <code>at_first</code>, but it introduces a previously unseen conformance issue (VJAR) in the routine <code>value_at_first</code>:
@@ -231,7 +236,77 @@ In this version <code>tn</code> need not be declared as a local variable. Rememb
 
 ===Both VEVI and VJAR errors===
 
-A design issue in class <code>NVP_LIST</code> causes issues of both conformance and initialization. In the original design, an instance of the class NVP_LIST could traverse its contents NVP-by-NVP with inherited functionality.  But it also could traverse its contents returning "sublists" based on recurring patterns of the <code>name</code> attributes of a sequence of name/value pairs. 
+A design issue in class <code>NVP_LIST</code> causes both conformance and initialization compiler errors. In the original design, an instance of the class NVP_LIST could traverse its contents NVP-by-NVP with inherited functionality.  Additionally, <code>NVP_LIST</code> has immediate functionality allowing an instance to traverse its contents in two different ways returning "sublists" based on recurring patterns of the <code>name</code> attributes of a sequence of name/value pairs. 
+
+These two traversal methods are referred to as "sequencing" and "segmenting". It's not important that you understand the details of what these traversals do. But it is important to know that a valid instance of <code>NVP_LIST</code> can either be in the process of sequencing or in the process of segmenting, or neither. It is invalid to be both sequencing ''and'' segmenting. 
+
+Two class attributes are maintained to store the recurring patterns of values of <code>{NVP}.name</code> that guide traversal:
+
+<code>
+feature {NONE} -- Implementation
+
+    sequence_array: ARRAY [STRING]
+            -- The current array of names being used for
+            --  sequence traversal
+
+    segment_array: ARRAY [STRING]
+            -- The current array of names being used to determine
+            --  the termination of list segments
+</code>
+
+In the original class design, each of these attributes would be void unless their corresponding traversal was active. So the class contains the following clauses in its invariant:
+
+<code>
+	not_sequencing_and_segmenting: not (segment_readable and sequence_readable)
+	sequence_traversal_convention: (sequence_array = Void) = (not sequence_readable)
+	segment_traversal_convention: (segment_array = Void) = (not segment_readable)
+</code>
+
+Of course by default these attributes are considered to be attached. So, because they are not initialized during creation, we see initialization errors. Because elements of the class intentionally set them to <code>Void</code>, we see conformance errors. 
+
+Here we have another opportunity to redesign (or not). We could mark the two arrays as <code>detachable</code>, recompile and fix any problems this causes (in fact, it causes eight errors: six Target rule violations, and two conformance issues). 
+
+However, because these attributes are not exported, we may be able to leave them attached and make changes to the implementation design without making breaking changes to the interface. 
+
+Those exported features which take arguments of the type <code>ARRAY [STRING]</code> which will serve as sequencing or segmenting control also require that the array contain at least one element. For example, the contract for feature <code>segment_start</code> contains these preconditions:
+
+<code>
+	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
+</code>
+
+Because the restriction always exists that a valid <code>sequence_array</code> or <code>segment_array</code> must contain at least one element, it is possible to redesign the implementation of the class such that an empty <code>sequence_array</code> and <code>segment_array</code> could serve the same purpose as a <code>Void</code> one does in the original design.
+
+So the invariant clauses that we saw above would now become:
+
+<code>
+	not_sequencing_and_segmenting: not (segment_readable and sequence_readable)
+	sequence_traversal_convention: (sequence_array.is_empty) = (not sequence_readable)
+	segment_traversal_convention: (segment_array.is_empty) = (not segment_readable)
+</code>
+
+Additionally, some postconditions which reference the implementation features <code>sequence_array</code> and/or <code>segment_array</code> would have to be changed. Looking at the postcondition clauses for <code>segment_start</code> we see that <code>segment_array</code> is expected (or not) to be <code>Void</code>:
+
+<code>
+    ensure
+        started: (not exhausted) implies (segment_readable and (segment_array /= Void) and (last_segment_element_index > 0))
+        not_started: exhausted implies ((not segment_readable) and (segment_array = Void) and (last_segment_element_index = 0))
+</code>
+
+To support the "empty array" design, <code>segment_start</code>'s postcondition clauses would be:
+
+<code>
+    ensure
+        started: (not exhausted) implies (segment_readable and (not segment_array.is_empty) and (last_segment_element_index > 0))
+        not_started: exhausted implies ((not segment_readable) and (segment_array.is_empty) and (last_segment_element_index = 0))
+</code>
+
 
 
 ==Code patterns==