DEFINITIONS
  STRING_LENGTH(xxx) == length(xxx);
  EXTERNAL_FUNCTION_STRING_LENGTH == STRING --> INTEGER;
  STRING_APPEND(xxx,yyy) == append(xxx,yyy);
  EXTERNAL_FUNCTION_STRING_APPEND == (STRING*STRING) --> STRING;
  STRING_SPLIT(xxx,yyy) == split(xxx,yyy);
  EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->STRING));
  STRING_JOIN(xxx,yyy) == join(xxx,yyy);
  EXTERNAL_FUNCTION_STRING_JOIN == (((INTEGER<->STRING)*STRING) --> STRING);
  STRING_CHARS(xxx) == chars(xxx);
  EXTERNAL_FUNCTION_STRING_CHARS == (STRING --> (INTEGER<->STRING));
  STRING_CODES(xxx) == codes(xxx);
  EXTERNAL_FUNCTION_STRING_CODES == (STRING --> (INTEGER<->INTEGER));
  STRING_TO_INT(sss) == 0;
  EXTERNAL_FUNCTION_STRING_TO_INT == (STRING --> INTEGER);
  STRING_IS_INT(sss) == (1=1);
  EXTERNAL_PREDICATE_STRING_IS_INT == (STRING);
  EXTERNAL_FUNCTION_DEC_STRING_TO_INT == STRING * INTEGER --> INTEGER;
  DEC_STRING_TO_INT(decimal_string,precision) == 0;
   /* parametric function; cannot be represented as constant function : */
  STRING_TO_ENUM(sss) ==({}(1)); /* Note: you have to include the DEFINITION into your B file */
  EXTERNAL_FUNCTION_STRING_TO_ENUM(TO_ENUM_TYPE) == (STRING --> TO_ENUM_TYPE);
  INT_TO_STRING(sss) == "0";
  EXTERNAL_FUNCTION_INT_TO_STRING == (INTEGER --> STRING);
  TO_STRING(sss) == "0";
  EXTERNAL_FUNCTION_TO_STRING(TO_STRING_TYPE) == (TO_STRING_TYPE --> STRING);
  FORMAT_TO_STRING(MyFormatString,ListOfValues) == "0";
  EXTERNAL_FUNCTION_FORMAT_TO_STRING(FORMAT_TO_STRING_TYPE) == ((STRING*seq(FORMAT_TO_STRING_TYPE)) --> STRING);