indexing
description: "Directory name abstraction"
legal: "See notice at end of class."
status: "See notice at end of class."
date: "$Date: 2006-01-22 18:25:44 -0800 (Sun, 22 Jan 2006) $"
revision: "$Revision: 56675 $"
class interface
DIRECTORY_NAME
create
make
PATH_NAME
make_from_string (p: STRING_8)
`p'
PATH_NAME
require PATH_NAME
path_not_void: p /= Void
ensure PATH_NAME
valid_file_name: is_valid
create {DIRECTORY_NAME}
string_make (n: INTEGER_32)
`n'
STRING_8
require STRING_8
non_negative_size: n >= 0
ensure STRING_8
empty_string: count = 0
area_allocated: capacity >= n
feature
make
PATH_NAME
make_from_string (p: STRING_8)
`p'
PATH_NAME
require PATH_NAME
path_not_void: p /= Void
ensure PATH_NAME
valid_file_name: is_valid
feature {ANY}
string: STRING_8
`Current'
STRING_8
ensure STRING_8
string_not_void: Result /= Void
string_type: Result.same_type ("")
first_item: count > 0 implies Result.item (1) = item (1)
recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).string)
feature
is_equal (other: like Current): BOOLEAN
`other'
PATH_NAME
require ANY
other_not_void: other /= Void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
ensure then COMPARABLE
trichotomy: Result = (not (Current < other) and not (other < Current))
feature
is_directory_name_valid (dir_name: STRING_8): BOOLEAN
`dir_name'
PATH_NAME
require PATH_NAME
exists: dir_name /= Void
is_volume_name_valid (vol_name: STRING_8): BOOLEAN
`vol_name'
PATH_NAME
require PATH_NAME
exists: vol_name /= Void
feature {ANY}
is_empty: BOOLEAN
FINITE
require CONTAINER
True
require STRING_GENERAL
True
prunable: BOOLEAN
STRING_8
feature
extend (directory_name: STRING_8)
`directory_name'
PATH_NAMEset_subdirectory
PATH_NAME
require PATH_NAME
string_exists: directory_name /= Void
valid_directory_name: is_directory_name_valid (directory_name)
ensure PATH_NAME
valid_file_name: is_valid
extend_from_array (directories: ARRAY [STRING_8])
`directories'
PATH_NAME
require PATH_NAME
array_exists: directories /= Void and then not (directories.is_empty)
ensure PATH_NAME
valid_file_name: is_valid
set_directory (directory_name: STRING_8)
`directory_name'
PATH_NAME
require PATH_NAME
string_exists: directory_name /= Void
valid_directory_name: is_directory_name_valid (directory_name)
ensure PATH_NAME
valid_file_name: is_valid
set_subdirectory (directory_name: STRING_8)
`directory_name'
PATH_NAMEextend
PATH_NAME
require PATH_NAME
string_exists: directory_name /= Void
valid_directory_name: is_directory_name_valid (directory_name)
ensure PATH_NAME
valid_file_name: is_valid
set_volume (volume_name: STRING_8)
`volume_name'
PATH_NAME
require PATH_NAME
string_exists: volume_name /= Void
valid_volume_name: is_volume_name_valid (volume_name)
empty_path_name: is_empty
ensure PATH_NAME
valid_file_name: is_valid
feature {ANY}
wipe_out
STRING_8
require COLLECTION
prunable: prunable
ensure COLLECTION
wiped_out: is_empty
ensure then STRING_8
is_empty: count = 0
empty_capacity: capacity = 0
feature {ANY}
frozen to_c: ANY
STRING_8
require STRING_8
not_is_dotnet: not {PLATFORM}.is_dotnet
feature {ANY}
frozen twin: like Current
`Current'
twincopycopy
ANY
ensure ANY
twin_not_void: Result /= Void
is_equal: Result.is_equal (Current)
feature
is_valid: BOOLEAN
feature {ANY}
out: STRING_8
STRING_8
require ANY
True
ensure then STRING_8
out_not_void: Result /= Void
same_items: same_type ("") implies Result.same_string (Current)
invariant
STRING_8
extendible: extendible
compare_character: not object_comparison
index_set_has_same_count: index_set.count = count
area_not_void: area /= Void
COMPARABLE
irreflexive_comparison: not (Current < Current)
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
INDEXABLE
index_set_not_void: index_set /= Void
RESIZABLE
increase_by_at_least_one: minimal_increase >= 1
BOUNDED
valid_count: count <= capacity
full_definition: full = (count = capacity)
FINITE
empty_definition: is_empty = (count = 0)
non_negative_count: count >= 0
indexing
library: "EiffelBase: Library of reusable components for Eiffel."
copyright: "Copyright (c) 1984-2006, Eiffel Software and others"
license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
source: "[
Eiffel Software
356 Storke Road, Goleta, CA 93117 USA
Telephone 805-685-1006, Fax 805-685-6869
Website http://www.eiffel.com
Customer support http://support.eiffel.com
]"
end DIRECTORY_NAME