note description: "File name abstraction" library: "Free implementation of ELKS library" status: "See notice at end of class." legal: "See notice at end of class." date: "$Date: 2019-02-20 15:19:53 +0000 (Wed, 20 Feb 2019) $" revision: "$Revision: 102853 $" class interface FILE_NAME create make -- Create empty string. -- (from READABLE_STRING_GENERAL) ensure -- from READABLE_STRING_GENERAL empty: count = 0 area_allocated: capacity >= 0 make_from_string (s: READABLE_STRING_8) -- Initialize from the characters of s. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 string_exists: s /= Void ensure -- from READABLE_STRING_8 not_shared_implementation: Current /= s implies not shared_with (s) initialized: same_string (s) make_temporary_name -- Create a temporary filename. create {FILE_NAME} string_make (n: INTEGER_32) -- Allocate space for at least n characters. -- (from READABLE_STRING_8) require -- from READABLE_STRING_GENERAL non_negative_size: n >= 0 ensure -- from READABLE_STRING_GENERAL empty_string: count = 0 area_allocated: capacity >= n feature -- Initialization make -- Create empty string. -- (from READABLE_STRING_GENERAL) ensure -- from READABLE_STRING_GENERAL empty: count = 0 area_allocated: capacity >= 0 make_from_string (s: READABLE_STRING_8) -- Initialize from the characters of s. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 string_exists: s /= Void ensure -- from READABLE_STRING_8 not_shared_implementation: Current /= s implies not shared_with (s) initialized: same_string (s) feature -- Access string: STRING_8 -- New STRING_8 having same character sequence as Current. -- (from READABLE_STRING_8) ensure -- from READABLE_STRING_8 string_not_void: Result /= Void string_type: Result.same_type (create {STRING_8}.make_empty) first_item: count > 0 implies Result.item (1) = item (1) recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).string feature -- Comparison is_equal (other: FILE_NAME): BOOLEAN -- Is the path name equal to other? -- (from PATH_NAME) require -- from ANY other_not_void: other /= Void ensure -- from ANY symmetric: Result implies other ~ Current consistent: standard_is_equal (other) implies Result ensure then -- from COMPARABLE trichotomy: Result = (not (Current < other) and not (other < Current)) feature -- Status report is_directory_name_valid (dir_name: STRING_8): BOOLEAN -- Is dir_name a valid subdirectory part for the operating system? -- (from PATH_NAME) require -- from PATH_NAME exists: dir_name /= Void is_empty: BOOLEAN -- Is structure empty? -- (from FINITE) require -- from CONTAINER True require -- from READABLE_STRING_GENERAL True is_extension_valid (ext: STRING_8): BOOLEAN -- Is ext a valid extension for the operating system? is_file_name_valid (f_name: STRING_8): BOOLEAN -- Is f_name a valid file name part for the operating system? is_valid: BOOLEAN -- Is the file name valid for the operating system? is_volume_name_valid (vol_name: STRING_8): BOOLEAN -- Is vol_name a valid volume name for the operating system? -- (from PATH_NAME) require -- from PATH_NAME exists: vol_name /= Void prunable: BOOLEAN -- May items be removed? (Answer: yes.) -- (from STRING_8) feature -- Status setting add_extension (ext: STRING_8) -- Append the extension ext to the file name require string_exists: ext /= Void non_empty_extension: not ext.is_empty valid_extension: is_extension_valid (ext) extend (directory_name: STRING_8) -- Append the subdirectory directory_name to the path name. -- Was declared in PATH_NAME as synonym of set_subdirectory. -- (from PATH_NAME) require -- from PATH_NAME string_exists: directory_name /= Void valid_directory_name: is_directory_name_valid (directory_name) ensure -- from PATH_NAME valid_file_name: is_valid extend_from_array (directories: ARRAY [STRING_8]) -- Append the subdirectories from directories to the path name. -- (from PATH_NAME) require -- from PATH_NAME array_exists: directories /= Void and then not directories.is_empty ensure -- from PATH_NAME valid_file_name: is_valid reset (a_name: STRING_8) -- Reset content with a path starting with a_name -- (from PATH_NAME) require -- from PATH_NAME a_name_attached: a_name /= Void set_directory (directory_name: STRING_8) -- Set the absolute directory part of the path name to directory_name. -- (from PATH_NAME) require -- from PATH_NAME string_exists: directory_name /= Void valid_directory_name: is_directory_name_valid (directory_name) ensure -- from PATH_NAME valid_file_name: is_valid set_file_name (file_name: STRING_8) -- Set the value of the file name part. require string_exists: file_name /= Void valid_file_name: is_file_name_valid (file_name) ensure valid_file_name: is_valid set_subdirectory (directory_name: STRING_8) -- Append the subdirectory directory_name to the path name. -- Was declared in PATH_NAME as synonym of extend. -- (from PATH_NAME) require -- from PATH_NAME string_exists: directory_name /= Void valid_directory_name: is_directory_name_valid (directory_name) ensure -- from PATH_NAME valid_file_name: is_valid set_volume (volume_name: STRING_8) -- Set the volume part of the path name to volume_name. -- (from PATH_NAME) require -- from PATH_NAME string_exists: volume_name /= Void valid_volume_name: is_volume_name_valid (volume_name) empty_path_name: is_empty ensure -- from PATH_NAME valid_file_name: is_valid feature -- Removal wipe_out -- Remove all characters. -- (from STRING_8) require -- from STRING_GENERAL True require -- from COLLECTION prunable: prunable ensure -- from STRING_GENERAL is_empty: count = 0 same_capacity: capacity = old capacity ensure -- from COLLECTION wiped_out: is_empty feature -- Conversion frozen to_c: ANY -- A reference to a C form of current string. -- Useful only for interfacing with C software. -- (from STRING_8) require -- from STRING_8 not_is_dotnet: not {PLATFORM}.is_dotnet feature -- Duplication frozen twin: FILE_NAME -- New object equal to Current -- twin calls copy; to change copying/twinning semantics, redefine copy. -- (from ANY) ensure -- from ANY twin_not_void: Result /= Void is_equal: Result ~ Current feature -- Output out: STRING_8 -- New string containing terse printable representation -- of current object -- (from READABLE_STRING_8) require -- from ANY True ensure -- from ANY out_not_void: Result /= Void ensure then -- from READABLE_STRING_8 out_not_void: Result /= Void same_items: same_type ("") implies Result.same_string (Current) invariant -- from STRING_8 extendible: Extendible compare_character: not object_comparison -- from READABLE_STRING_8 area_not_void: area /= Void -- from COMPARABLE irreflexive_comparison: not (Current < Current) -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from READABLE_INDEXABLE consistent_boundaries: Lower <= count or else Lower = count + 1 -- from STRING_GENERAL mutable: not is_immutable -- from RESIZABLE increase_by_at_least_one: Minimal_increase >= 1 -- from BOUNDED valid_count: count <= capacity full_definition: full = (count = capacity) -- from FINITE empty_definition: is_empty = (count = 0) note copyright: "Copyright (c) 1984-2019, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 5949 Hollister Ave., Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com ]" end -- class FILE_NAME
Generated by ISE EiffelStudio