Class STRING: Changes from ELKS 2001 to ELKS 2002

January 2002:

• Refine the specification of 'as_lower', 'as_upper'
• Rename the precondition of infix "+"
• Change the assertion tag name in 2 features
• Change the assertion tag name in 5 features

• Fix a precedence error in 'three_way_comparison'

Proposal

   10 JANUARY 2002 VERSIONS:

   as_lower: like Current
      -- New object with all letters in lower case
      ensure
         as_lower_not_void: Result /= Void
         length: Result.count = count
         anchor: count > 0 implies Result.item(1) = item(1).as_lower
         recurse: count > 1 implies Result.substring(2, count)
                   .is_equal(substring(2, count).as_lower)

   as_upper: like Current
      -- New object with all letters in upper case
      ensure
         as_upper_not_void: Result /= Void
         length: Result.count = count
         anchor: count > 0 implies Result.item(1) = item(1).as_upper
         recurse: count > 1 implies Result.substring(2, count)
                   .is_equal(substring(2, count).as_upper)

Notes

Result

Proposal

   12 JANUARY 2002 VERSION:

   infix "+" (other: STRING): like Current
      -- New object which is a clone of `Current' extended
      -- by the characters of `other'.
      require
         other_not_void: other /= Void
      ensure
         result_not_void: Result /= Void
         result_count: Result.count = count + other.count
         initial: Result.substring (1, count).is_equal (Current)
         final: Result.substring (count + 1, count + other.count)
                 .same_string (other)

Notes

Result

Proposal

   27 JANUARY 2002 VERSION:

   insert_string (s: STRING; i: INTEGER)
      -- Insert `s' at index `i', shifting characters between ranks
      -- `i' and `count' rightwards.
      require
         s_not_void: s /= Void
         valid_insertion_index: 1 <= i and i <= count + 1
      ensure
         inserted: is_equal(old substring (1, i - 1)
          + old clone (s) + old substring (i, count))

   replace_substring(s: STRING; start_index, end_index: INTEGER)
      -- Replace the substring from `start_index' to `end_index',
      -- inclusive, with `s'.
      require
         s_not_void: s /= Void
         valid_start_index: 1 <= start_index
         valid_end_index: end_index <= count
         meaningful_interval: start_index <= end_index + 1
      ensure
         replaced: is_equal(old (substring(1, start_index - 1) +
                                 s +
                                 substring(end_index + 1, count)))

Notes

Result

Proposal

   28 JANUARY 2002 VERSION:

   is_boolean: BOOLEAN
      -- Does `Current' represent a BOOLEAN?
      ensure
         definition: Result = (same_string("true")
          or same_string("false"))

   (The tag was previously "is_boolean".)

   is_double: BOOLEAN
      -- Does `Current' represent a DOUBLE?
      ensure
         definition:
          -- Result is true if and only if the following two
          -- conditions are satisfied:
          --
          -- 1. In the following BNF grammar, the value of
          --    `Current' can be produced by "Real_literal":
          --
          -- Real_literal    = Mantissa [Exponent_part]
          -- Exponent_part   = "E" Exponent
          --                 | "e" Exponent
          -- Exponent        = Integer_literal
          -- Mantissa        = Decimal_literal
          -- Decimal_literal = Integer_literal ["." Integer]
          -- Integer_literal = [Sign] Integer
          -- Sign            = "+" | "-"
          -- Integer         = Digit | Digit Integer
          -- Digit           = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
          --
          -- 2. The numerical value represented by `Current'
          --    is within the range that can be represented
          --    by an instance of type DOUBLE.

   (The tag was previously "syntax_and_range".)

   is_integer: BOOLEAN
      -- Does `Current' represent an INTEGER?
      ensure
         definition:
          -- Result is true if and only if the following two
          -- conditions are satisfied:
          --
          -- 1. In the following BNF grammar, the value of
          --    `Current' can be produced by "Integer_literal":
          --
          -- Integer_literal = [Sign] Integer
          -- Sign            = "+" | "-"
          -- Integer         = Digit | Digit Integer
          -- Digit           = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
          --
          -- 2. The integer value represented by `Current'
          --    is within the (inclusive) range
          --    minimum_integer..maximum_integer
          --    where `minimum_integer' and `maximum_integer'
          --    are the constants defined in class PLATFORM.

   (The tag was previously "syntax_and_range".)

   is_real: BOOLEAN
      -- Does `Current' represent a REAL?
      ensure
         definition:
          -- Result is true if and only if the following two
          -- conditions are satisfied:
          --
          -- 1. In the following BNF grammar, the value of
          --    `Current' can be produced by "Real_literal":
          --
          -- Real_literal    = Mantissa [Exponent_part]
          -- Exponent_part   = "E" Exponent
          --                 | "e" Exponent
          -- Exponent        = Integer_literal
          -- Mantissa        = Decimal_literal
          -- Decimal_literal = Integer_literal ["." Integer]
          -- Integer_literal = [Sign] Integer
          -- Sign            = "+" | "-"
          -- Integer         = Digit | Digit Integer
          -- Digit           = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
          --
          -- 2. The numerical value represented by `Current'
          --    is within the range that can be represented
          --    by an instance of type REAL.

   (The tag was previously "syntax_and_range".)

   to_boolean: BOOLEAN
      -- Boolean value;
      -- "true" yields true, "false" yields false
      require
         represents_a_boolean: is_boolean
      ensure
         definition: Result = same_string("true")

   (The tag was previously "to_boolean".)

Result

Proposal

   5 FEBRUARY 2002 VERSION:

   three_way_comparison (other: like Current): INTEGER
      -- If current object equal to `other', 0;
      -- if smaller, -1; if greater, 1
      -- (Inherited from COMPARABLE.)
      require  -- from COMPARABLE
         other_exists: other /= Void
      ensure  -- from COMPARABLE
         equal_zero: (Result = 0) = is_equal (other)
         smaller_negative: (Result = -1) = (Current < other)
         greater_positive: (Result = 1) = (Current > other)

Notes

Result