Code coverage for abstract_string.li

///////////////////////////////////////////////////////////////////////////////
//                             Lisaac Library                                //
//                                                                           //
//                   LSIIT - ULP - CNRS - INRIA - FRANCE                     //
//                                                                           //
//   This program is free software: you can redistribute it and/or modify    //
//   it under the terms of the GNU General Public License as published by    //
//   the Free Software Foundation, either version 3 of the License, or       //
//   (at your option) any later version.                                     //
//                                                                           //
//   This program is distributed in the hope that it will be useful,         //
//   but WITHOUT ANY WARRANTY; without even the implied warranty of          //
//   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the           //
//   GNU General Public License for more details.                            //
//                                                                           //
//   You should have received a copy of the GNU General Public License       //
//   along with this program.  If not, see <http://www.gnu.org/licenses/>.   //
//                                                                           //
//                     http://isaacproject.u-strasbg.fr/                     //
///////////////////////////////////////////////////////////////////////////////
Section Header

  + name    := ABSTRACT_STRING;

  - export  := STRING;

  - copyright   := "2003-2005 Jérome Boutet, 2003-2007 Benoit Sonntag";

  - comment := "Generic prototype for STRING and STRING_CONSTANT";

Section Inherit

  - parent_hashable:HASHABLE := HASHABLE;

  - parent_comparable:COMPARABLE := COMPARABLE;

Section Public  //ABSTRACT_STRING, ABSTRACT_ENTRY

  + storage:NATIVE_ARRAY(CHARACTER);
  // Collection containing characters

Section Public

  + count:INTEGER;
  // size

  - lower:INTEGER := 1;

  - upper:INTEGER <- count;
  // size

  - capacity:INTEGER <- count;
  // size

  //
  // Access.
  //

  - item index:INTEGER :CHARACTER <-
  // Character at position `index'.
  // * Require: index is valid
  [
    -? {valid_index index};
  ]
  (
    storage.item (index - 1)
  );

  - Self:SELF '@' Left 1 index:INTEGER :CHARACTER <-
  // Character at position `index'.
  (
    item index
  );

  //
  // Switch case :
  //

  - when value:ABSTRACT_STRING then block:{} :ABSTRACT_STRING <-
  // When `Self' equal `value', execute `block'
  (
    (Self ~= value).if block;
    Self
  );

  - when value1:ABSTRACT_STRING or value2:ABSTRACT_STRING then block:{} :ABSTRACT_STRING <-
  // When `Self' equal `value1' or `value2', execute `block'
  (
    ((Self ~= value1) || {Self ~= value2}).if block;
    Self
  );

  - case value:ABSTRACT_STRING then block:{} :ABSTRACT_STRING <-
  // * See: `when_then'
  ( + result :ABSTRACT_STRING;

    ((Self != ABSTRACT_STRING)    {Self ~= value}).if {
      block.value;
      result := ABSTRACT_STRING;
    } else {
      result := Self;
    };
    result
  );

  - case_if test:{BOOLEAN} then block:{} :ABSTRACT_STRING <-
  // If `test' is true then `block'
  ( + result :ABSTRACT_STRING;

    ((Self != ABSTRACT_STRING)    test).if {
      block.value;
      result := ABSTRACT_STRING;
    } else {
      result := Self;
    };
    result
  );

  - case_else block:{} <-
  // otherwise, execute `block'
  (
    (Self != ABSTRACT_STRING).if block;
  );

  //
  // Testing.
  //

  - valid_index index:INTEGER :BOOLEAN <-
  // True when `index' is valid (i.e., inside actual bounds).
  ( index.in_range lower to count );

  - is_empty : BOOLEAN <- count = 0;


  - hash_code: INTEGER <-
  // Return a hashcode
  ( + result:INTEGER;

    1.to count do { i:INTEGER;
      result := (5 * result) + (item i).code;
    };
    (result < 0).if	{
      result := ~ result;
    };
    result
  );

  - Self:SELF '<' other:SELF :BOOLEAN <- Self ~< other;

  - Self:SELF '~>' other:ABSTRACT_STRING :BOOLEAN <- other ~< Self;

  - Self:SELF '~<' other:ABSTRACT_STRING :BOOLEAN <-
  // Is Current less than `other' ?
  ( + i: INTEGER;
    + result: BOOLEAN;

    i := 1;
    {(count < i) || {other.count < i} || {item i != other.item i}}.until_do {
      i := i + 1;
    };
    (count < i).if {
      result := other.count >= i;
    } else {
      (other.count < i).if {
        result := FALSE;
      } else {
        result := item i < other.item i;
      };
    };
    result
  );

  - Self:SELF '!<' other:ABSTRACT_STRING :BOOLEAN <-
  // Is Current less than `other' ? But, the `upper' to `lower' comparaison
  ( + i1,i2: INTEGER;
    + result:BOOLEAN;

    i1 := upper;
    i2 := other.upper;
    {(i1 < lower) || {i2 < other.lower} || {item i1 != other.item i2}}.until_do {
      i1 := i1 - 1;
      i2 := i2 - 1;
    };
    (i1 < lower).if {
      result := i2 >= other.lower;
    } else {
      (i2 < other.lower).if {
        result := FALSE;
      } else {
        result := item i1 < other.item i2;
      };
    };
    result
  );

  - compare other:ABSTRACT_STRING :INTEGER <-
  // Compare alphabetically `Self' to `other'
  ( + i: INTEGER;
    + result:INTEGER;
    i := 1;
    {(count < i) || {other.count < i} || {item i != other.item i}}.until_do {
      i := i + 1;
    };
    (count < i).if {
      (other.count < i).if {
        result := 0;
      } else {
        result := -1;
      };
    } else {
      (other.count < i).if {
        result := 1;
      } else {
        (item i < other.item i).if {
          result := -1;
        } else {
          result := 1;
        };
      };
    };

    result
  );

  - same_as other:ABSTRACT_STRING :BOOLEAN <-
  // Case insensitive `=='.
  ( + s1, s2:NATIVE_ARRAY(CHARACTER);
    + i:INTEGER;
    + result:BOOLEAN;
    ? {other != NULL};

    i := count;
    (i = other.count).if {
      (storage.fast_memcmp (other.storage) until i).if {
        result:=TRUE;
      } else {
        i := i - 1;
        s1 := storage;
        s2 := other.storage;
        result:=TRUE;
        {(i!=0)    {result}}.while_do {
          result:=s1.item i.same_as (s2.item i);
          i:=i-1;
        };
      };
    };
    result
  );

  - Self:SELF '==' Left 40 other:E :BOOLEAN <-
  // Has Current the same text as `other' ?
  ( + same:ABSTRACT_STRING;
    same ?= other;
    (same != NULL)    {Self ~= same}
  );

  - Self:SELF '~=' Left 40 other:ABSTRACT_STRING :BOOLEAN <-
  // Has Current the same text as `other' ?
  ( + result:BOOLEAN;
    ? {other != NULL};
    (count = other.count).if {
      (count = 0).if {
        result := TRUE;
      } else {
        result:=storage.fast_memcmp (other.storage) until count;
      };
    };
    result
  );

  - item_code i:INTEGER :INTEGER <-
  // Code of character at position `i'.
  (
    ? { valid_index i};
    storage.item (i - 1).code
  );

  - index_of ch:CHARACTER since start_index:INTEGER :INTEGER <-
  // Index of first occurrence of `c' at or after `start_index',
  // result = count + 1, if none.
  ( + result:INTEGER;
    ? { start_index.in_range 1 to (count + 1)};

    result := start_index;

    {(result > count) || {ch = item result}}.until_do {
      result := result + 1;
    };

    result
  );

  - last_index_of ch:CHARACTER since start_index:INTEGER :INTEGER <-
  // Index of first occurrence of `c' at or before `start_index',
  // 0 if none.
  ( + result:INTEGER;
    ? {start_index.in_range 0 to upper};

    result := start_index;

    {(result < lower) || {ch = item result}}.until_do {
      result := result - 1;
    };

    ? {(result != 0) ->> {item result = ch}};
    result
  );

  - fast_index_of ch:CHARACTER :INTEGER <-
  // Gives the index of the first occurrence `ch' or
  // 0 if none.
  (+ result:INTEGER;
    result := 1 + storage.fast_index_of (ch,0) until (count - 1);
    ? {(result != count + 1) ->> {item result = ch}};
    result
  );

  - index_of ch:CHARACTER :INTEGER <-
  // Gives the index of the first occurrence of 'ch' or
  // 0 if none.
  (
    fast_index_of ch
  );

  - first_index_of c:CHARACTER :INTEGER <-
  // Index of first occurrence of `c' at index 1 or after index 1.
  (
    fast_index_of c
  );

  - fast_last_index_of ch:CHARACTER :INTEGER <-
  // Gives the index of the last occurrence `ch' or
  // 0 if none.
  (+ result:INTEGER;
    result := 1 + storage.fast_reverse_index_of ch from (upper-1);

    ? {(result != 0) ->> {item result = ch}};
    result
  );

  - last_index_of c:CHARACTER :INTEGER <-
  // Index of last occurrence of `c' at index upper or before index upper.
  (
    fast_last_index_of c
  );

  - first_difference_index other:ABSTRACT_STRING :INTEGER <-
  // First difference index with `other'.
  // if `other' is equal `Self', return `upper' + 1
  [ -? {other != NULL}; ]
  ( + result:INTEGER;

    (Self = other).if {
      result := upper + 1;
    } else {
      result := lower;
      {
        (result <= upper)   
        {result <= other.upper}   
        {item result = other.item result}
      }.while_do {
        result := result + 1;
      };
    };
    result
  );

  - has ch:CHARACTER :BOOLEAN <- storage.fast_has ch until (count - 1);
  // True if `ch' is in the STRING.

  - has_substring other:ABSTRACT_STRING :BOOLEAN <-
  // True if `other' is in the STRING.
  ( first_substring_index other != 0 );

  - occurrences c:CHARACTER :INTEGER <-
  // Number of times character `c' appears in the string.
  (
    storage.fast_occurrences c until (count - 1)
  );

  - has_suffix s:ABSTRACT_STRING :BOOLEAN <-
  // True if suffix of `Current' is `s'.
  (
    + result:BOOLEAN;
    + i1,i2:INTEGER;

    ? { s != NULL };

    (s.count <= count).if {
      i1 := count - s.count + 1;
      i2 := 1;
      { (i1 > count) || { i2 > s.count} || { item i1 != s.item i2}}.until_do {
        i1 := i1 + 1;
        i2 := i2 + 1;
      };
      result := i1 > count;
    };

    result
  );

  - has_prefix p:ABSTRACT_STRING :BOOLEAN <-
  // True if prefix of `Current' is `p'.
  [ ? { p != NULL }; ]
  (
    + result:BOOLEAN;
    + i:INTEGER;

    ( p.count <= count ).if {
      i := p.count;
      { (i = 0) || { item i != p.item i}}.until_do {
        i := i - 1;
      };
      result := i = 0;
    };

    result
  );

  // Testing and Conversion:

  - is_boolean:BOOLEAN <-
  // does self represent a BOOLEAN?
  // valid BOOLEANS are "TRUE" and "FALSE".
  (
    (Self == "TRUE") || { Self == "FALSE"}
  );

  - to_boolean:BOOLEAN <-
  // Boolean value;
  // "true" yields true, "false" yields false (what a surprise).
  (
    ?{ is_boolean };
    Self == "TRUE"
  );

  - is_bit:BOOLEAN <-
  // True when the contents is a sequence of bits (i.e., mixed
  // characters `0' and characters `1').
  ( + i:INTEGER;
    + result:BOOLEAN;
    i := count;
    result := TRUE;
    { (! result) || { i = 0}}.until_do {
      result := item i.is_bit;
      i := i - 1;
    };
    ? {result = (count = occurrences '0' + occurrences '1')};
    result
  );

  - is_integer:BOOLEAN <-
  // Does self represent an INTEGER?
  // `Result' is true if and only if the following two conditions hold:
  //
  // 1. In the following BNF grammar, the value of self can be
  // produced by "Integer_literal", if leading and trailing
  // separators are ignored:
  //
  // 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 self is within the
  // range that can be represented by an instance of type INTEGER.
  (
    + i, state, value: INTEGER;
    + negative: BOOLEAN;
    + result:BOOLEAN;
    + cc: CHARACTER;

    // state 0: nothing read.
    // state 1: "+" or "-" read.
    // state 2: in the number.
    // state 3: after the number.
    // state 4: error.

    i := 1;

    { (state = 4) || {i > count}}.until_do {
      cc := item i;
      ( state = 0).if {
        cc.is_separator.if {
        }.elseif {cc = '+'} then {
          state := 1;
        }.elseif {cc = '-'} then {
          negative := TRUE;
          state := 1;
        }.elseif {cc.is_digit} then {
          value := cc.decimal_value;
          state := 2;
        } else {
          state := 4;
        };
      }.elseif { state = 1} then {
        cc.is_digit.if {
          value := cc.decimal_value;
          negative.if {
            value := - value;
          };
          state := 2;
        } else {
          state := 4;
        };
      }.elseif { state = 2 } then {
        cc.is_digit.if {
          negative.if {
            value := 10 * value - cc.decimal_value;
          } else {
            value := 10 * value + cc.decimal_value;
          };
          // over/underflow check here
          ((negative    {value > 0}) || { ! negative    {value < 0}}).if {
            state := 4;
          };
        }.elseif {cc.is_separator} then {
          state := 3;
        } else {
          state := 4;
        };
      }.elseif { state = 3 } then {
        cc.is_separator.if {
        } else {
          state := 4;
        };
      };

      i := i + 1;
    };
    ( (state != 0)    { state != 4}).if {
      result := TRUE;
    };

    result
  );

  - is_integer_64:BOOLEAN <-
  // Does self represent an INTEGER_64?
  // `Result' is true if and only if the following two conditions hold:
  //
  // 1. In the following BNF grammar, the value of self can be
  // produced by "Integer_literal", if leading and trailing
  // separators are ignored:
  //
  // 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 self is within the
  // range that can be represented by an instance of type INTEGER_64.
  (
    + i, state: INTEGER;
    + value:INTEGER_64;
    + negative: BOOLEAN;
    + result:BOOLEAN;
    + cc: CHARACTER;

    // state 0: nothing read.
    // state 1: "+" or "-" read.
    // state 2: in the number.
    // state 3: after the number.
    // state 4: error.

    i := 1;

    { (state = 4) || {i > count}}.until_do {
      cc := item i;
      ( state = 0).if {
        cc.is_separator.if {
        }.elseif {cc = '+'} then {
          state := 1;
        }.elseif {cc = '-'} then {
          negative := TRUE;
          state := 1;
        }.elseif {cc.is_digit} then {
          value := cc.decimal_value;
          state := 2;
        } else {
          state := 4;
        };
      }.elseif { state = 1} then {
        cc.is_digit.if {
          value := cc.decimal_value;
          negative.if {
            value := - value;
          };
          state := 2;
        } else {
          state := 4;
        };
      }.elseif { state = 2 } then {
        cc.is_digit.if {
          negative.if {
            value := value * 10 - cc.decimal_value;
          } else {
            value := value * 10 + cc.decimal_value;
          };
          // over/underflow check here
          ((negative    {value > 0}) || { ! negative    {value < 0}}).if {
            state := 4;
          };
        }.elseif {cc.is_separator} then {
          state := 3;
        } else {
          state := 4;
        };
      }.elseif { state = 3 } then {
        cc.is_separator.if {
        } else {
          state := 4;
        };
      };

      i := i + 1;
    };
    ( (state != 0)    { state != 4}).if {
      result := TRUE;
    };

    result
  );

  - to_integer:INTEGER <-
  // self must look like an INTEGER.
  (
    + i, state:INTEGER;
    + cc: CHARACTER;
    + negative: BOOLEAN;
    + result:INTEGER;

    ? { is_integer };
    // state 0: nothing read.
    // state 1: "+" or "-" read.
    // state 2: in the number.
    // state 3: after the number.

    i := 1;

    { i > count }.until_do {
      cc := item i;

      (state = 0).if {
        cc.is_separator.if {
        }.elseif {cc = '+'} then {
          state := 1;
        }.elseif {cc = '-'} then {
          negative := TRUE;
          state := 1;
        } else { // cc.is_digit
          result := cc.decimal_value;
          state := 2;
        };
      }.elseif { state = 1 } then {
        // cc.is_digit
        result := cc.decimal_value;
        negative.if {
          result := - result;
        };
        state := 2;
      }.elseif { state = 2} then {
        cc.is_digit.if {
          negative.if {
            result := 10 * result - cc.decimal_value;
          } else {
            result := 10 * result + cc.decimal_value;
          };
        } else { // cc.is_separator
          state := 3;
        };
      }.elseif { state = 3 } then {
        // cc.is_separator
        i := count; // terminate the loop
      };

      i := i + 1;
    };

    result
  );

  - to_integer_64:INTEGER_64 <-
  // self must look like an INTEGER.
  (
    + i, state:INTEGER;
    + cc: CHARACTER;
    + negative: BOOLEAN;
    + result:INTEGER_64;

    ? { is_integer };
    // state 0: nothing read.
    // state 1: "+" or "-" read.
    // state 2: in the number.
    // state 3: after the number.

    i := 1;

    { i > count }.until_do {
      cc := item i;

      (state = 0).if {
        cc.is_separator.if {
        }.elseif {cc = '+'} then {
          state := 1;
        }.elseif {cc = '-'} then {
          negative := TRUE;
          state := 1;
        } else { // cc.is_digit
          result := cc.decimal_value;
          state := 2;
        };
      }.elseif { state = 1 } then {
        // cc.is_digit
        result := cc.decimal_value;
        negative.if {
          result := - result;
        };
        state := 2;
      }.elseif { state = 2} then {
        cc.is_digit.if {
          negative.if {
            result := result * 10 - cc.decimal_value;
          } else {
            result := result * 10 + cc.decimal_value;
          };
        } else { // cc.is_separator
          state := 3;
        };
      }.elseif { state = 3 } then {
        // cc.is_separator
        i := count; // terminate the loop
      };

      i := i + 1;
    };

    result
  );

  - is_hexadecimal :BOOLEAN <-
  ( + j:INTEGER;
    + result:BOOLEAN;
    (is_empty).if_false {
      j := lower;
      {(j > upper) || {! item j.is_hexadecimal_digit}}.until_do {
        j:=j+1;
      };
      result := j > upper;
    };
    result
  );

  - to_hexadecimal :INTEGER_64 <-
  ( + result:INTEGER_64;
    ? {is_hexadecimal};
    lower.to upper do { j:INTEGER;
      result := (result << 4) | item j.hexadecimal_value;
    };
    result
  );

  - is_octal :BOOLEAN <-
  ( + result:BOOLEAN;
    + j:INTEGER;
    (is_empty).if_false {
      j := lower;
      {(j > upper) || {! item j.is_octal_digit}}.until_do {
        j:=j+1;
      };
      result:= j > upper;
    };
    result
  );

  - to_octal:INTEGER_64 <-
  ( + result:INTEGER_64;
    ? {is_octal};

    lower.to upper do { j:INTEGER;
      result := (result << 3) | item j.octal_value;
    };
    result
  );

  - is_binary :BOOLEAN <-
  ( + result:BOOLEAN;
    + j:INTEGER;

    (is_empty).if_false {
      j := lower;
      { (j > upper) || {! item j.is_binary_digit} }.until_do {
        j := j + 1;
      };

      result := j > upper;
    };

    result
  );

  - to_binary :INTEGER_64 <-
  ( + result:INTEGER_64;
    ? {is_bit};

    lower.to upper do { j:INTEGER;
      result := result << 1;
      (item j = '1').if {
        result := result | 1;
      };
    };
    result
  );

  - is_real_16_16:BOOLEAN <-
  // Does self represent an REAl_16_16 ?
  // `Result' is true if and only if the following two conditions hold:
  //
  // 1. In the following BNF grammar, the value of self can be
  // produced by "real_literal", if leading and trailing
  // separators are ignored:
  //
  // Real_literal = [Sign] Integer [Point Integer]
  // Sign            = "+" | "-"
  // Point           = "."
  // Integer         = Digit | Digit Integer
  // Digit           = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
  //
  // 2. The numerical value represented by self is within the
  // range that can be represented by an instance of type REAL_16_16.
  (
    + i, state, value_int: INTEGER;
    + value:REAL_16_16;
    + negative: BOOLEAN;
    + result:BOOLEAN;
    + cc: CHARACTER;
    + d:INTEGER;

    // state 0: nothing read.
    // state 1: "+" or "-" read.
    // state 2: in the number before the point
    // state 3: in the number after the point
    // state 4: after the number.
    // state 5: error.

    i := 1;
    d := 1;

    { (state = 5) || {i > count}}.until_do {
      cc := item i;
      ( state = 0).if {
        cc.is_separator.if {
        }.elseif {cc = '+'} then {
          state := 1;
        }.elseif {cc = '-'} then {
          negative := TRUE;
          state := 1;
        }.elseif {cc.is_digit} then {
          value_int := cc.decimal_value;
          state := 2;
        } else {
          state := 5;
        };
      }.elseif { state = 1} then {
        cc.is_digit.if {
          value_int := cc.decimal_value;
          state := 2;
        } else {
          state := 5;
        };
      }.elseif { state = 2 } then {
        cc.is_digit.if {
          value_int := 10 * value_int + cc.decimal_value;
          (value_int < 0).if {
            state := 5;
          };
        }.elseif { cc = '.' } then {
          state := 3;
          value := value_int.to_real_16_16;
        }.elseif {cc.is_separator} then {
          state := 4;
        } else {
          state := 5;
        };
      }.elseif { state = 3 } then {
        cc.is_digit.if {
          d := d * 10;
          value := value + (cc.decimal_value.to_real_16_16) /# d;
        }.elseif {cc.is_separator} then {
          state := 4;
        } else {
          state := 5;
        };
      }.elseif { state = 4 } then {
        cc.is_separator.if {
        } else {
          state := 5;
        };
      };

      i := i + 1;
    };
    negative.if {
      value := - value;
    };
    ( (state != 0)    { state != 5}).if {
      result := TRUE;
    };

    result
  );

  - to_real_16_16:REAL_16_16 <-
  (
    + i, state, value_int: INTEGER;
    + value:REAL_16_16;
    + negative: BOOLEAN;
    + cc: CHARACTER;
    + d:INTEGER;

    // state 0: nothing read.
    // state 1: "+" or "-" read.
    // state 2: in the number before the point
    // state 3: in the number after the point
    // state 4: after the number.

    i := 1;
    d := 1;

    {i > count}.until_do {
      cc := item i;
      ( state = 0).if {
        cc.is_separator.if {
        }.elseif {cc = '+'} then {
          state := 1;
        }.elseif {cc = '-'} then {
          negative := TRUE;
          state := 1;
        }.elseif {cc.is_digit} then {
          value_int := cc.decimal_value;
          state := 2;
        };
      }.elseif { state = 1} then {
        cc.is_digit.if {
          value_int := cc.decimal_value;
          state := 2;
        };
      }.elseif { state = 2 } then {
        cc.is_digit.if {
          value_int := value_int * 10 + cc.decimal_value;
        }.elseif { cc = '.' } then {
          state := 3;
          value := value_int.to_real_16_16;
        } else {  // cc is separator
          value := value_int.to_real_16_16;
          state := 4;
        };
      }.elseif { state = 3 } then {
        cc.is_digit.if {
          d := d * 10;
          value := value + (cc.decimal_value.to_real_16_16) /# d;
        } else { // cc is separator
          state := 4;
        };
      }.elseif { state = 4 } then {
        // cc is separator
        i := count;  // terminate the loop
      };

      i := i + 1;
    };

    (state = 2).if {
      value := value_int.to_real_16_16;
    };

    negative.if {
      value := - value;
    };

    value
  );

  //
  // Modification:
  //

  - Self:SELF '+' other:ABSTRACT_STRING :STRING_BUFFER <-
  // Create a new STRING which is the concatenation of
  // `self' and `other'.
  [
    -? {other != NULL};
  ]
  ( + result:STRING_BUFFER;
    result:=STRING_BUFFER.create (count + other.count);
    result.append Self;
    result.append other;
    result
  )
  [
    +? {Result.count = Old count + other.count};
  ];

  - as_lower:STRING <-
  // New object with all letters in lower case.
  (
    + result:STRING;
    result := STRING.create capacity;
    result.copy Self;
    result.to_lower;
    result
  );

  - as_upper:STRING <-
  // New object with all letters in upper case.
  (
    + result:STRING;
    result := STRING.create capacity;
    result.copy Self;
    result.to_upper;
    result
  );

  // Other features:

  - first:CHARACTER <-
  // Access to the very `first' character.
  (
    + result:CHARACTER;
    //? {! is_empty};

    result := storage.item 0;

    //? { result == item 1};
    result
  );

  - last:CHARACTER <-
  // Access to the very `last' character.
  (
    + result:CHARACTER;
    ? {! is_empty};

    result := storage.item (count - 1);

    ? { result = item count};
    result
  );

  - substring start_index:INTEGER to end_index:INTEGER :STRING <-
  // New string consisting of items [`start_index'.. `end_index'].
  [
    -? { start_index >= 1 };
    -? { end_index <= count };
    -? { start_index <= end_index + 1 };
  ]
  ( + c:INTEGER;
    + result:STRING;


    c := end_index - start_index + 1;
    result := STRING.create c;
    result.set_count c;
    result.storage.slice_copy storage to 0 from (start_index - 1) to (end_index - 1);

    result
  )
  [
    +? { Result.count = end_index - start_index + 1 };
  ];

  - substring_begin start:INTEGER to_begin end:INTEGER :STRING <-
  (
    substring start to end
  );

  - substring_begin start:INTEGER to_end end:INTEGER :STRING <-
  (
    substring start to (upper-end-1)
  );

  - substring_end start:INTEGER to_end end:INTEGER :STRING <-
  (
    substring (upper-start-1) to (upper-end-1)
  );

  - substring_index (other:ABSTRACT_STRING,start_index:INTEGER) :INTEGER <-
  // Position of the first occurrence of `other' at or after 1
  // or 0 f none.
  ( + i,s,result:INTEGER;

    //? {! other.is_empty };
    ? { (start_index >=1)    { start_index <= count + 1 }};

    s := start_index;
    {(result != 0) || {(s + other.count - 1) > count }}.until_do {
      i := 1;
      {(i > other.count) || {item (s + i - 1) != other.item i}}.until_do {
        i := i + 1;
      };

      (i > other.count).if {
        result := s;
      } else {
        s := s + 1;
      };
    };

    result
  );

  - first_substring_index other:ABSTRACT_STRING :INTEGER <-
  // Position of the first occurrence of `other' at or after 1
  // or 0 if none.
  (
    ? {! other.is_empty };

    substring_index (other,1)
  );

  //
  // Splitting a STRING:
  //

  - partition sep:ABSTRACT_STRING from start_index:INTEGER :(STRING, STRING, STRING) <-
  [
    -? {sep != NULL};
    -? {valid_index start_index};
  ]
  ( + i, j:INTEGER;
    + head, sep, tail :STRING;
    i := substring_index (sep, start_index);
    (i = 0).if {
      // Not found
      head := to_string;
    } else {
      // Found
      j := i + sep.count;
      (i > lower).if {
        head := substring lower to (i-1);
      };
      sep  := substring i to j;
      (j < upper).if {
        tail := substring (j+1) to upper;
      };
    };
    head, sep, tail
  );

  - partition sep:ABSTRACT_STRING :(STRING, STRING, STRING) <-
  (
    partition sep from lower
  );

  - split_str sep:ABSTRACT_STRING :ARRAY(STRING) <-
  [
    -? {sep != NULL};
  ]
  ( + result:ARRAY(STRING);
    ( count > 0 ).if {
      split_buffer.clear;
      split_str sep in split_buffer;
      (! split_buffer.is_empty).if {
        result := ARRAY(STRING).create (split_buffer.lower) to (split_buffer.upper);
        result.copy split_buffer;
      };
    };

    result
  )
  [
    +? { (Result != NULL) ->> { ! Result.is_empty }};
  ];

  - split_str sep:ABSTRACT_STRING in words:COLLECTION(STRING) <-
  // Same jobs as `split_str' but result is appended in `words'.
  [
    -? {words != NULL};
    -? {sep != NULL};
  ]
  ( + i, j:INTEGER;
    // i    first character of the next word
    // j-1  last character of the next word
    // j    first character of the next separator

    i := 1;
    { j := substring_index(sep, i); j != 0 }.while_do {
      words.add_last (substring i to (j-1));
      i := j + sep.count;
    };
    words.add_last (substring i to upper);
  );

  - split:ARRAY(STRING) <-
  // Split the string into an array of words. Uses `is_separator' of
  // CHARACTER to find words. Gives Void or a non empty array.
  (
    + result:ARRAY(STRING);
    ( count > 0 ).if {
      split_buffer.clear;
      split_in split_buffer;
      (! split_buffer.is_empty).if {
        result := ARRAY(STRING).create (split_buffer.lower) to (split_buffer.upper);
        result.copy split_buffer;
      };
    };
    ? { (result != NULL) ->> { ! result.is_empty }};

    result
  );

  - split_in words:COLLECTION(STRING) <-
  // Same jobs as `split' but result is appended in `words'.
  (
    + state,old_count: INTEGER;
    // state = 0: waiting next word.
    // state = 1: inside a new word.
    + c: CHARACTER;

    ? { words != NULL};
    old_count := words.count;
    (count > 0).if {
      1.to upper do { i:INTEGER;
        c := item i;
        (state = 0).if {
          (! c.is_separator).if {
            string_buffer.clear;
            string_buffer.append_character c;
            state := 1;
          };
        } else {
          (! c.is_separator).if {
            string_buffer.append_character c;
          } else {
            words.add_last (string_buffer.twin);
            state := 0;
          };
        };
      };
      ( state = 1).if {
        words.add_last (string_buffer.twin);
      };
    };

    ? { (words.count) >= old_count };
  );

  - split_at sep:CHARACTER :ARRAY(STRING) <-
  // Split the string at characters `c' into an array of words.
  (
    + result:ARRAY(STRING);
    ( count > 0 ).if {
      split_buffer.clear;
      split_at sep in split_buffer;
      (! split_buffer.is_empty).if {
        result := ARRAY(STRING).create (split_buffer.lower) to (split_buffer.upper);
        result.copy split_buffer;
      };
    };

    result
  )
  [
    +? { (Result != NULL) ->> { ! Result.is_empty }};
  ];

  - split_at sep:CHARACTER in words:COLLECTION(STRING) <-
  // Same jobs as `split' but result is appended in `words'.
  (
    + state,old_count: INTEGER;
    // state = 0: waiting next word.
    // state = 1: inside a new word.
    + c: CHARACTER;

    ? { words != NULL};
    old_count := words.count;
    (count > 0).if {
      1.to upper do { i:INTEGER;
        c := item i;
        (state = 0).if {
          (c != sep).if {
            string_buffer.clear;
            string_buffer.append_character c;
            state := 1;
          };
        } else {
          (c != sep).if {
            string_buffer.append_character c;
          } else {
            words.add_last (string_buffer.twin);
            state := 0;
          };
        };
      };
      ( state = 1).if {
        words.add_last (string_buffer.twin);
      };
    };

    ? { (words.count) >= old_count };
  );

  /*
  - get_new_iterator:ITERATOR(CHARACTER) <-
  (
    ITERATOR_ON_STRING(CHARACTER).create Self
  );
  */

  - same_string other:ABSTRACT_STRING :BOOLEAN <-
  // Do self and other have the same character sequence?
  // Useful in proper descendants of STRING.
  (
    ? { other != NULL };
    Self == other.to_string
  );

  - to_string:STRING <-
  // New STRING having the same character sequence as self.
  // Useful in proper descendants of STRING.
  (
    STRING.create_from_string Self
  );

  - to_abstract_string :ABSTRACT_STRING <- Self;

  - string_buffer:STRING := STRING.create 256; // Private, temporary once buffer.

  - split_buffer:ARRAY(STRING) := ARRAY(STRING).create_with_capacity 4 lower 1;

  //
  // Display.
  //

  - print <-
  (
    IO.put_string Self;
  );

  -  printline <-
  (
    IO.put_string Self;
    IO.put_string "\n";
  );

  - fast_print <-
  (
    SYSTEM_IO.print_string Self;
  );

  - println <-
  (
    print;
    '\n'.print;
  );

  //
  // The guru section
  //

  - to_external:NATIVE_ARRAY(CHARACTER) <-
  // Gives C access to the internal `storage' (may be dangerous).
  // To be compatible with C, a null character is added at the end
  // of the internal `storage'. This extra null character is not
  // part of the Lisaac STRING.
  (
    deferred;
    NULL
  );