class interface P_SEPARATED_STRING

creation
   make (a_separator: STRING)
      --  Make separated string with specified separator.

      require
         not_void: a_separator /= Void

   make_space
      --  Make string separated by a single string.


feature(s) from P_SEPARATED_STRING
   --  Operation(s)

   add (a_string: STRING)
      --  Add a string (and separator if necessary).

      require
         not_void: a_string /= Void

   reset
      --  Reset.


feature(s) from P_SEPARATED_STRING
   --  Access

   as_string: STRING

invariant
   separator_not_void: separator /= Void;
   as_string_not_void: as_string /= Void;

end of P_SEPARATED_STRING