PR# 12837 Repeated postcondition in STRING_8.substring

Problem Report Summary
Submitter: peter_gummer
Category: EiffelBase
Priority: Medium
Date: 2007/05/22
Class: Bug
Severity: Non-critical
Number: 12837
Release: 6.0.6.8510
Confidential: No
Status: Closed
Responsible:
Environment: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.8.1.3) Gecko/20070309 Firefox/2.0.0.3
Synopsis: Repeated postcondition in STRING_8.substring

Description
This postcondition appears in STRING_8:

recurse: Result.count > 0 implies Result.substring (2, Result.count).is_equal (substring (start_index + 1, end_index))

Exactly the same appears in STRING_GENERAL. There's no reason for this, is there?

Also, note that first_item appears in both, although the implementation is a bit different. In STRING_GENERAL, first_item ought to be called first_code.
To Reproduce
ensure -- from STRING_GENERAL
	substring_not_void: Result /= Void
	substring_count: Result.count = end_index - start_index + 1 or Result.count = 0
	first_item: Result.count > 0 implies Result.code (1) = code (start_index)
	recurse: Result.count > 0 implies Result.substring (2, Result.count).is_equal (substring (start_index + 1, end_index))
ensure then
	first_item: Result.count > 0 implies Result.item (1) = item (start_index)
	recurse: Result.count > 0 implies Result.substring (2, Result.count).is_equal (substring (start_index + 1, end_index))
end
Problem Report Interactions
From:manus_eiffel    Date:2007/05/23    Status: Closed    Download   
Thanks for finding this. It will be fixed in the next release. Note that this is now part of FreeELKS.