+
Point of view
All features
class MICROSOFT_PATH_NAME
Summary
Operating system path name, Microsoft notation (DOS, Win9x, WinNT)
Direct parents
Inherit list: UNIXISH_PATH_NAME
Class invariant
Overview
Creation features
{ANY}
Features
Creation
{ANY}
Constants
{ANY}
Access
{ANY}
Operations
{ANY}
  • to_absolute
    Transform into equivalent absolute path
  • normalize
    Normalize removing double separators, and up-references
  • normalize_case
    Transform into normalized case version (equivalent), with standard path separators
  • remove_last
    Remove last component of path (keep the "dirname")
  • add_last (elem: STRING)
  • expand_user
    Replace an initial "~" or "~user" by user home directory
  • expand_shellouts
    Replace substrings of form $(command) with execution of shell commands
Copying, comparison
{ANY}
  • copy (other: MICROSOFT_PATH_NAME)
    Update current object using fields of object attached to other, so as to yield equal objects.
  • is_equal (other: MICROSOFT_PATH_NAME): BOOLEAN
    Is other attached to an object considered equal to current object?
Representation
{MICROSOFT_PATH_NAME}
{PATH_JOINER}
  • start_join (a_drive: STRING, absoluteness: INTEGER_32)
    Start joining an absolute path to Current
    drive is optional absoluteness is, e.g., the number of leading slashes:
      0 for relative paths
      1 for absolute paths
      more for super-absolute paths (for instance, network-wide)
    
  • join_element (element: STRING)
    Add an unspecified element (directory or file) to the end of the path
  • end_join
    Finish joining the path
Representation
{}
Internal
{}
Access
{ANY}
Operations
{ANY}
{PATH_JOINER}
{}
Creation/ Initialization
{ANY}
Access
{ANY}
Operations
{ANY}
  • join (other: PATH_NAME)
    Join with other using filesystem semantics
  • expand_variables
    Replace substrings of form $name or ${name} with environment variable values
{PATH_JOINER}
{PATH_JOINER}
make_empty
effective procedure
{ANY}
Make a 'null' path
ensure
make_root
effective procedure
{ANY}
Path to root directory (in current drive)
ensure
make_current
effective procedure
{ANY}
Path to current directory (relative).
See also to_absolute if you need the absolute current working directory
ensure
make_from_string (s: STRING)
effective procedure
{ANY}
require
  • s /= Void
  • s.is_empty or else is_valid_path(s)
ensure
  • to_string.is_equal(s)
  • old to_string /= s implies to_string /= s
up_directory: STRING
is ".."
constant attribute
{ANY}
this_directory: STRING
is "."
constant attribute
{ANY}
extension_separator: CHARACTER
is '.'
constant attribute
{ANY}
Character used to separate filenames from extensions
directory_separator: CHARACTER
is '\'
constant attribute
{ANY}
Character used to separate directories This character is forbidden in filenames
drive_separator: CHARACTER
is ':'
constant attribute
{ANY}
to_string: STRING
effective function
{ANY}
String representation
ensure
  • Result /= Void
  • Result.is_empty or else is_valid_path(Result)
drive_specification: STRING
effective function
{ANY}
Drive specified by the current path, Void if none
ensure
  • Result.count = 0 or Result.count = 2
  • drive = '%U' = Result.is_empty
  • not Result.is_empty implies Result.first = drive
  • not Result.is_empty implies Result.item(2) = ':'
  • Result /= Void implies to_string.has_prefix(Result)
count: INTEGER_32
effective function
{ANY}
Number of elements in_path
ensure
  • Result >= 0
last: STRING
effective function
{ANY}
Last component (also known as "basename")
require
  • not is_empty
ensure
  • to_string.has_suffix(Result)
  • not Result.has(directory_separator)
  • Result /= Void
  • is_valid_file_name(Result)
extension: STRING
effective function
{ANY}
Path extension (may be empty)
ensure
  • is_extension: not Result.is_empty implies Result.first = extension_separator
  • is_minimal: Result.occurrences(extension_separator) <= 1
  • not Result.has(directory_separator)
  • is_suffix: to_string.has_suffix(Result)
  • is_extension: not Result.is_empty implies Result.first = extension_separator
  • is_minimal: Result.occurrences(extension_separator) <= 1
  • not Result.has(directory_separator)
  • is_empty implies Result.is_empty
is_absolute: BOOLEAN
effective function
{ANY}
absolute path?
is_normalized: BOOLEAN
effective function
{ANY}
Has no redundant separators, or redundant up-references
ensure
is_separator (ch: CHARACTER): BOOLEAN
effective function
{ANY}
Is ch a possible path separator?
( '/' or '\' )
ensure
  • ch = directory_separator implies Result
is_valid_path (a_path: STRING): BOOLEAN
effective function
{ANY}
Does path represent a syntactically valid file or directory path?
The result does not imply that there actually a file or directory with that name. This operation does not perform any disk access.
require
  • a_path /= Void
ensure
  • a_path.is_equal(old a_path.twin)
is_valid_file_name (elem: STRING): BOOLEAN
effective function
{ANY}
Does path only contain valid characters for a file?
The result does not imply that there is actually a file or directory with that name. Not the same as is_valid_path: path separators (/ for unix, \ for windows, ...) are allowed in paths, but not in file names. This operation does not perform any disk access.
require
  • elem /= Void
ensure
  • Result implies not elem.has(directory_separator)
  • elem.is_equal(old elem.twin)
exists: BOOLEAN
effective function
{ANY}
     local
        i: FILE_INFORMATION
same_file (other: MICROSOFT_PATH_NAME): BOOLEAN
effective function
{ANY}
     local
        i, j: FILE_INFORMATION
to_absolute
effective procedure
{ANY}
Transform into equivalent absolute path
ensure
  • is_absolute
  • is_normalized
normalize
effective procedure
{ANY}
Normalize removing double separators, and up-references
ensure
  • is_normalized
  • old is_normalized implies to_string.is_equal(old to_string.twin)
normalize_case
effective procedure
{ANY}
Transform into normalized case version (equivalent), with standard path separators
remove_last
effective procedure
{ANY}
Remove last component of path (keep the "dirname")
require
  • not is_empty
ensure
add_last (elem: STRING)
effective procedure
{ANY}
require
  • elem /= Void
  • not elem.has(directory_separator)
ensure
  • last.is_equal(elem)
  • not_reduced: old count <= count
  • may_grow_one: count <= old count + 1
expand_user
effective procedure
{ANY}
Replace an initial "~" or "~user" by user home directory
ensure
  • not old to_string.twin.has_prefix("~") implies to_string.is_equal(old to_string.twin)
expand_shellouts
effective procedure
{ANY}
Replace substrings of form $(command) with execution of shell commands
ensure
  • not to_string.has_substring("$(") implies to_string.is_equal(old to_string.twin)
copy (other: MICROSOFT_PATH_NAME)
effective procedure
{ANY}
Update current object using fields of object attached to other, so as to yield equal objects.
Note: you can't copy object from a different dynamic type.
require
  • not immutable
  • same_dynamic_type(other)
ensure
  • is_equal(other)
is_equal (other: MICROSOFT_PATH_NAME): BOOLEAN
effective function
{ANY}
Is other attached to an object considered equal to current object?
require
  • other /= Void
ensure
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
drive: CHARACTER
writable attribute
Drive letter, or if none
start_join (a_drive: STRING, absoluteness: INTEGER_32)
effective procedure
Start joining an absolute path to Current
drive is optional absoluteness is, e.g., the number of leading slashes:
  0 for relative paths
  1 for absolute paths
  more for super-absolute paths (for instance, network-wide)
require
  • absoluteness >= 0
ensure
join_element (element: STRING)
effective procedure
Add an unspecified element (directory or file) to the end of the path
require
  • element /= Void
ensure
end_join
effective procedure
Finish joining the path
ensure
  • drive = old drive
  • old join_error implies join_error
no_drive: CHARACTER
is '%U'
constant attribute
{}
to_string_cache: STRING
writable attribute
{}
valid_cache: BOOLEAN
writable attribute
{}
tmp: MICROSOFT_PATH_NAME
once function
{}
ensure
  • Result /= Void
start_join_to (other: PATH_JOINER): INTEGER_32
effective function
{}
require
  • other /= Void
ensure
  • Result.in_range(path.lower, path.upper + 1)
is_valid_directory: BOOLEAN
is True
constant attribute
{ANY}
Does Current represent a syntactically valid directory path?
For many Systems, there may be no syntactical difference between file paths and directory paths, in that case is_valid_directory is always True.
ensure
  • Result or is_valid_file
is_valid_file: BOOLEAN
effective function
{ANY}
Does Current represent a syntactically valid directory path?
For many Systems, there may be no syntactical difference between file paths and directory paths, in that case is_valid_file is always True.
ensure
  • Result or is_valid_directory
go_up
effective procedure
{ANY}
Go up by one directory
join_to (other: PATH_JOINER)
effective procedure
{ANY}
require
  • other /= Void
short_name: STRING
effective function
{ANY}
ensure
  • Result /= Void
join_extension (an_extension: STRING)
effective procedure
Add an extension to the last element of the path
require
  • an_extension /= Void
ensure
  • old join_error implies join_error
join_error: BOOLEAN
is False
constant attribute
Did an error occur during joining
path: STRING
writable attribute
{}
scan_element (p: INTEGER_32, element: STRING): INTEGER_32
effective function
{}
require
  • path.valid_index(p)
  • element /= Void
ensure
  • Result.in_range(p + 1, path.upper + 1)
  • path.substring(p, Result - 1).has_suffix(element)
join_directory_to (other: PATH_JOINER, element: STRING)
effective procedure
{}
require
  • other /= Void
  • not element.is_empty
join_element_to (other: PATH_JOINER, element: STRING)
effective procedure
{}
require
  • other /= Void
  • not element.is_empty
make_from_path_name (pn: PATH_NAME)
effective procedure
{ANY}
require
  • pn /= Void
is_empty: BOOLEAN
effective function
{ANY}
Path is null.
Note that you can have a null absolute path (i.e., root) or a null relative path (current directory)
ensure
as_absolute: MICROSOFT_PATH_NAME
effective function
{ANY}
Equivalent absolute path
ensure
is_file: BOOLEAN
effective function
{ANY}
Path points to an existing regular file?
is_directory: BOOLEAN
effective function
{ANY}
Path points to an existing directory?
infix "+" (other: MICROSOFT_PATH_NAME): MICROSOFT_PATH_NAME
effective function
{ANY}
Join with other using filesystem semantics
require
  • other /= Void
infix "/" (elem: STRING): MICROSOFT_PATH_NAME
effective function
{ANY}
Path with elem inside current
require ensure
join (other: PATH_NAME)
effective procedure
{ANY}
Join with other using filesystem semantics
require
  • other /= Void
ensure
  • old is_normalized implies is_normalized
    definition: to_string.is_equal (old (Current+other).to_string) assertion above is commented out because of SE bug

expand_variables
effective procedure
{ANY}
Replace substrings of form $name or ${name} with environment variable values
ensure
join_up
effective procedure
Go up one directory
ensure
  • old join_error implies join_error
join_directory (element: STRING)
effective procedure
Add a directory to the end of the path
require
  • element /= Void
ensure
join_file (element: STRING)
effective procedure
Add a file to the end of the path
require
  • element /= Void
ensure