Refine feature occurrences

Proposal

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

   occurrences (c: CHARACTER): INTEGER
         -- Number of times c appears in the string
      ensure
         zero_if_empty: count = 0 implies Result = 0
         simple_recurse:
          (count > 0 and then item (1) /= c) implies
          Result = substring (2, count).occurrences (c)
         recurse_and_add:
          (count > 0 and then item (1) = c) implies
          Result = 1 + substring (2, count).occurrences (c)

Rationale

Make the specification rigorous, without changing the semantics.

History

Every vendor already implements a version of occurrences that is compatible with this specification.

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
                franck.arnaud@omgroup.com
Accept the proposal
                sergei_ivanov@object-tools.com
                jcm@mstr.hgc.edu
                ericb@gobosoft.com
                genepi@sympatico.ca
                saunders@wchat.on.ca
                kwaxer@aha.ru
Don't mind (happy either way)
                tking@insystems.com
Reject the proposal
                joachim.durchholz@halstenbach.de

Amendment

The following amendment was proposed by Joachim Durchholz on 19 November 1999, and seconded by Scott Steinman and James McKim. It was unopposed, and has been incorporated into the ELKS 2000 draft without a formal vote.

Rename the postconditions, yielding the following set:

   zero_if_empty: count = 0 implies Result = 0
   recurse_if_not_found_at_first_position:
    (count > 0 and then item (1) /= c) implies
    Result = substring (2, count).occurrences (c)
   recurse_if_found_at_first_position:
    (count > 0 and then item (1) = c) implies
    Result = 1 + substring (2, count).occurrences (c)

This proposed amendment was unopposed, and has been incorporated into the ELKS 2000 draft without a formal vote.