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
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

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'.
			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)
			create Result.make (start_pos, end_pos)
			if start_pos <= end_pos then
				Result.subcopy (Current, start_pos, end_pos, start_pos)
			lower: Result.lower = start_pos
			upper: Result.upper = end_pos
To Reproduce
See above.
Problem Report Interactions
From:alexk_es    Date:2018/09/04    Status: Closed    Download   
Fixed in rev#101778 of EiffelStudio 18.07 release.