class interface UT_CANNOT_WRITE_TO_FILE_ERROR creation make (filename: STRING) -- Create a new error reporting that file -- filename cannot be opened in write mode. require filename_not_void: filename /= Void feature(s) from KL_SHARED_ARGUMENTS -- Access Arguments: KL_ARGUMENTS -- Command-line arguments ensure arguments_not_void: Result /= Void feature(s) from KL_IMPORTED_STRING_ROUTINES -- Access STRING_: KL_STRING_ROUTINES -- Routines that ought to be in class STRING ensure string_routines_not_void: Result /= Void feature(s) from KL_IMPORTED_ARRAY_ROUTINES -- Access ANY_ARRAY_: KL_ARRAY_ROUTINES[ANY] -- Routines that ought to be in class ARRAY ensure any_array_routines_not_void: Result /= Void INTEGER_ARRAY_: KL_ARRAY_ROUTINES[INTEGER] -- Routines that ought to be in class ARRAY ensure integer_array_routines_not_void: Result /= Void STRING_ARRAY_: KL_ARRAY_ROUTINES[STRING] -- Routines that ought to be in class ARRAY ensure string_array_routines_not_void: Result /= Void feature(s) from UT_ERROR -- Access message (a_template: STRING): STRING -- Error message built using a_template; -- Occurrences of "$N" or "${N}" (where N stands -- for [0-9]+) in the template are substituted by -- the entry N in parameters or left as "$N" -- or "${N}" if N is out of bounds, unless it is -- equal to 0 in which case it is substituted by -- the program name. The character '$' is escaped -- using "$$". Return a new string each time. require a_template_not_void: a_template /= Void ensure message_not_void: Result /= Void parameters: ARRAY[STRING] -- Parameters used for building the error message -- (See header comment of message for details.) default_message: STRING -- Default error message built using default_template ensure default_message_not_void: Result /= Void default_template: STRING -- Default template used to built the error message code: STRING -- Error code invariant -- dollar0: $0 = program name -- dollar1: $1 = filename parameters_not_void: parameters /= Void; no_void_parameter: not STRING_ARRAY_.has(parameters,Void); end of UT_CANNOT_WRITE_TO_FILE_ERROR