Class CHARACTER: Changes from ELKS 95 to ELKS 2002

February 2001:

• Refine the specification of infix "<"

• Add features as_lower and as_upper

• Refine the specification of as_lower and as_upper

Proposal

   19 FEBRUARY 2001 VERSION

   infix "<" (other: like Current): BOOLEAN
      -- Is 'other' greater than current character?
      -- (Inherited from COMPARABLE.)
      require  -- from COMPARABLE
         other_exists: other /= Void
      ensure  -- from COMPARABLE
         asymmetric: Result implies not (other < Current)
      ensure then
         definition: result = (code < other.code)

Notes

A set of parentheses was inserted into the "definition" postcondition (after the call to vote) to correct an undisputed precedence error.

Result

The proposal was accepted.

Proposal

   08 MARCH 2001 19:15 version

   as_lower: CHARACTER
      -- Lower case equivalent.
      converted:
         ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").has(Current)
          implies Result = ("abcdefghijklmnopqrstuvwxyz").item(
          ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").index_of(Current, 1))
      unchanged:
         not ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").has(Current)
          implies Result = Current

   as_upper: CHARACTER
      -- Upper case equivalent.
      converted:
         ("abcdefghijklmnopqrstuvwxyz").has(Current)
          implies Result = ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").item(
          ("abcdefghijklmnopqrstuvwxyz").index_of(Current, 1))
      unchanged:
         not ("abcdefghijklmnopqrstuvwxyz").has(Current)
          implies Result = Current

Notes

The "ensure" keyword (missing in this proposal) was added to the proposed class text after the call-to-vote.

Result

The proposal was accepted.

Proposal

   25 SEPTEMBER 2001 VERSION

   as_lower: like Current
      -- Lower case equivalent
      ensure
         non_void_result:
            Result /= Void
         converted:
            ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").has(item)
             implies Result.item = ("abcdefghijklmnopqrstuvwxyz").item(
             ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").index_of(item, 1))
         unchanged:
            not ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").has(item)
             implies Result = Current

   as_upper: like Current
      -- Upper case equivalent
      ensure
         non_void_result:
            Result /= Void
         converted:
            ("abcdefghijklmnopqrstuvwxyz").has(item)
             implies Result.item = ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").item(
             ("abcdefghijklmnopqrstuvwxyz").index_of(item, 1))
         unchanged:
            not ("abcdefghijklmnopqrstuvwxyz").has(item)
             implies Result = Current

Notes

• The result type is changed from "CHARACTER" to "like Current"
• "Result.item" is used instead of "Result", and "item" is used instead of "Current", in several places
• A new postcondition asserts that the result is not void

Result

The proposal was accepted.