From c04f788585755f2ee2ecc9aefc7c3359f86c04f4 Mon Sep 17 00:00:00 2001 From: halw Date: Wed, 20 May 2009 20:54:13 +0000 Subject: [PATCH] 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 --- .../index.wiki | 77 ++++++++++++++++++- 1 file changed, 76 insertions(+), 1 deletion(-) 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 8a728550..89f4d8c4 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 @@ -181,6 +181,11 @@ So the least impact to this routine will be to declare its type as detacha The same change is made in other routines that can return void by design, particularly including a routine called value_at_first, which gets our attention next. +The case of at_first offered us an opportunity to redesign (or not). We might have been able to leave at_first attached. After all, in void-safe software, the fewer detachables, the better. Maybe we could devise a way, possibly through preconditions and other queries, that would guarantee that at_first attempts to execute only when it can return a value. + +But at_first 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 at_first satisfies the VEVI issue in at_first, but it introduces a previously unseen conformance issue (VJAR) in the routine value_at_first: @@ -231,7 +236,77 @@ In this version tn need not be declared as a local variable. Rememb ===Both VEVI and VJAR errors=== -A design issue in class NVP_LIST 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 name attributes of a sequence of name/value pairs. +A design issue in class NVP_LIST 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, NVP_LIST has immediate functionality allowing an instance to traverse its contents in two different ways returning "sublists" based on recurring patterns of the name 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 NVP_LIST 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 {NVP}.name that guide traversal: + + +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 + + +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: + + + 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) + + +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 Void, we see conformance errors. + +Here we have another opportunity to redesign (or not). We could mark the two arrays as detachable, 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 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 + + +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. + +So the invariant clauses that we saw above would now become: + + + 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) + + +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: + + + 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)) + + +To support the "empty array" design, segment_start's postcondition clauses would be: + + + 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 patterns==