Question regarding UC_UTF8_ROUTINES.character_byte_count

The code of UC_UTF8_ROUTINES.character_byte_count reads:

	character_byte_count (c: CHARACTER): INTEGER is
			-- Number of bytes needed to encode character
			-- `c' with the UTF-8 encoding
		local
			a_code: INTEGER
		do
			if c <= byte_127 then
					-- 2^7
					-- 0xxxxxxx
				Result := 1
			elseif c <= byte_255 then
					-- 110xxxxx 10xxxxxx
				Result := 2
			else
				a_code := c.code
				if a_code < 2048 then
						-- 2^11
						-- 110xxxxx 10xxxxxx
					Result := 2
				elseif a_code < 65536 then
						-- 2^16
						-- 1110xxxx 10xxxxxx 10xxxxxx
					Result := 3
				else
					Result := 4
				end
			end
		ensure
			character_byte_count_large_enough: Result >= 1
			character_byte_count_small_enough: Result <= 4
		end


But the `else' part is useless since it is guaranteed to never execute this code.
Should it be simply implemented as:

	character_byte_count (c: CHARACTER): INTEGER is
			-- Number of bytes needed to encode character
			-- `c' with the UTF-8 encoding
		do
			Result := code_byte_count (c.code)
		ensure
			character_byte_count_large_enough: Result >= 1
			character_byte_count_small_enough: Result <= 4
		end
?

Thanks,
Manu

------------------------------------------------------------------------  
Eiffel Software	
805-685-1006	
http://www.eiffel.com	
Customer support: http://support.eiffel.com	
User group: http://groups.eiffel.com/join	
------------------------------------------------------------------------  




-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/