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