Refine feature substring

Proposal

class STRING: change the specification of substring to the following:

   substring (start_index, end_index: INTEGER): like Current
         -- Create a substring containing all characters
         -- from start_index to end_index inclusive.
      require
         valid_start_index: 1 <= start_index
         valid_end_index: end_index <= count
         meaningful_interval: start_index <= end_index + 1
      ensure
         result_count: Result.count = end_index - start_index + 1
         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))

Rationale

Make the specification rigorous.
Weaken the precondition to allow end_index to be one less than start_index, in which case an empty STRING is returned.

History

An ELKS 1995-compatible version of substring is implemented by every vendor. ISE appears to be the only vendor already compatible with the weaker precondition of this proposal.

Impact of proposed change

Low.

Result

The proposal was accepted into the ELKS 2000 draft on 19 November 1999.

Votes cast at egroups:

Strongly accept the proposal
                jcm@mstr.hgc.edu
Accept the proposal
                sergei_ivanov@object-tools.com
                ericb@gobosoft.com
                franck.arnaud@omgroup.com
                saunders@wchat.on.ca
                kwaxer@aha.ru
Don't mind (happy either way)
                tking@insystems.com

Votes cast by email:

Accept the proposal
genepi@sympatico.ca