PR# 15079 First precondition of {ARRAY}.subarray appears to be wrong

Problem Report Summary
Submitter: jsostroff
Category: EiffelBase
Priority: Medium
Date: 2008/11/26
Class: Bug
Severity: Serious
Number: 15079
Release: Latest ES6.3
Confidential: No
Status: Closed
Responsible:
Environment: Mozilla/4.0 (compatible; MSIE 7.0; Windows NT 6.0; GTB5; SLCC1; .NET CLR 2.0.50727; Media Center PC 5.0; .NET CLR 3.0.04506; InfoPath.2; .NET CLR 3.5.21022)
Synopsis: First precondition of {ARRAY}.subarray appears to be wrong

Description
The first precondition of {ARRAY}.subarray appears to be wrong.

The third precondition allows for an array of size zero where the end_position < start_position.

However, the first precondition asserts that the index must be valid i.e. between lower and upper, which will be false for an array of size zero. 

Thus it does not allow subarrays of size zero (which it should).

==
subarray (start_pos, end_pos: INTEGER_32): ARRAY [G]
			-- Array made of items of current array within
			-- bounds `start_pos' and `end_pos'.
		require
			valid_start_pos: valid_index (start_pos)
			valid_end_pos: end_pos <= upper
			valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
		do
			create Result.make (start_pos, end_pos)
			if start_pos <= end_pos then
				Result.subcopy (Current, start_pos, end_pos, start_pos)
			end
		ensure
			lower: Result.lower = start_pos
			upper: Result.upper = end_pos
		end
To Reproduce
See above.
Problem Report Interactions
From:alexk_es    Date:2018/09/04    Status: Closed    Download