+
Point of view
All features
class CYGWIN_DIRECTORY_NOTATION
to_parent_directory (some_path:
STRING)
effective procedure
to_subdirectory_with (parent_path:
STRING, entry_name:
STRING)
effective procedure
require
- is_valid_path(parent_path)
- is_valid_path(entry_name)
ensure
- entry_name.is_equal(old entry_name.twin)
require
- is_valid_path(parent_path)
- is_valid_file_name(file_name)
ensure
- file_name.is_equal(old file_name.twin)
require
- is_valid_directory_path(parent_path)
- is_valid_path(subpath)
- not is_absolute_path(subpath)
ensure
- parent_path.is_empty or else is_valid_path(parent_path)
- parent_path.is_empty or else is_valid_directory_path(parent_path) = old is_valid_directory_path(subpath)
- parent_path.is_empty or else is_absolute_path(parent_path) = old is_absolute_path(parent_path)
to_directory_path (path:
STRING)
effective procedure
require
- path /= Void
- is_valid_path(path)
ensure
- is_valid_directory_path(path)
require
- is_valid_path(path)
- buffer /= Void
require
- can_map_drive(source_notation, drive)
ensure
- is_valid_path(drive)
- is_absolute_path(drive)
to_default_root (directory:
STRING)
effective procedure
ensure
- is_valid_path(directory)
- is_absolute_path(directory)
to_current_directory (directory:
STRING)
effective procedure
require
ensure
- is_valid_path(directory)
- not is_absolute_path(directory)
is True
constant attribute
ensure
- path.is_equal(old path.twin)
- Result implies not path.is_empty
ensure
- path.is_equal(old path.twin)
- Result implies is_valid_path(path)
ensure
- name.is_equal(old name.twin)
- Result implies not name.is_empty
require
ensure
- path.is_equal(old path.twin)
require
- is_valid_path(path)
- destination_notation /= Void
ensure
- path.is_equal(old path.twin)
- Result.is_empty or else destination_notation.is_valid_path(Result)
frozen
effective procedure
frozen
effective procedure
to_valid_file_name (name:
STRING)
effective procedure