Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: timing_integration.prf Sprache: VDM

Original von: VDM^©

class FileSystemLayerAlg

types

public
Path = <Root> | seq1 of FileName;

public
FileName = seq1 of char;

public
FileContents = seq of char;

public
FileStore = map Path to File
inv fileStore ==
  <Root> in set dom fileStore and
  forall path in set dom fileStore &
    let parent = dirName(path) in
        parent in set dom fileStore and
        isDirectory(fileStore(parent));

public
File :: attributes : Attributes
        contents   : [FileContents]
inv file ==
  (file.attributes.fileType = <Directory> and file.contents = nil) or
  (file.attributes.fileType = <RegularFile> and file.contents <> nil);

public
Attributes :: fileType : FileType;

public
FileType = <RegularFile> | <Directory>;

public
OpenFileDescriptorTable =
  map FileHandler to OpenFileDescriptor;

public
FileHandler = nat;

public
OpenFileDescriptor ::
  path : Path;

public
System :: table       : OpenFileDescriptorTable
          fileStore   : FileStore
inv sys ==
  forall openfiledescriptor in set rng sys.table &
    openfiledescriptor.path in set dom sys.fileStore;

functions

public
FS_DeleteFileDir_Main : System * Path -> System * FFS_Status
FS_DeleteFileDir_Main(sys, full_path) ==
  if not isRoot(full_path) and
     isElemFileStore(full_path, sys.fileStore) and
     pre_FS_DeleteFileDir_System(sys, full_path)
  then mk_(FS_DeleteFileDir_System(sys, full_path), <FFS_StatusSuccess>)
  else mk_(sys, FS_DeleteFileDir_Exception(sys, full_path));

private
FS_DeleteFileDir_System : System * Path -> System
FS_DeleteFileDir_System(sys, full_path) ==
  mu(sys, fileStore |-> FS_DeleteFileDir_FileStore(sys.fileStore, full_path))
pre pre_FS_DeleteFileDir_FileStore(sys.fileStore, full_path) and
  forall buffer in set rng sys.table & buffer.path <> full_path;

private
FS_DeleteFileDir_FileStore : FileStore * Path -> FileStore
FS_DeleteFileDir_FileStore(fileStore, full_path) ==
  {full_path} <-: fileStore
pre forall path in set dom fileStore & dirName(path) <> full_path;

private
FS_DeleteFileDir_Exception : System * Path -> FFS_Status
FS_DeleteFileDir_Exception(sys, full_path) ==
  if isRoot(full_path)
  then   <FS_ErrorInvalidPath>
  elseif not isElemFileStore(full_path, sys.fileStore)
  then   <FS_ErrorPathNotFound>
  elseif exists buffer in set rng sys.table & buffer.path = full_path
  then   <FS_ErrorFileStillOpen>
  elseif isDirectory(sys.fileStore(full_path)) or
         exists path in set dom sys.fileStore & full_path = dirName(path)
  then   <FS_ErrorDirectoryNotEmpty>
  else   <FFS_StatusUnknown>;

public
FS_Init_Main : () -> System * FFS_Status
FS_Init_Main() == mk_(FS_Init_System(), <FFS_StatusSuccess>);

private
FS_Init_System : () -> System
FS_Init_System() == mk_System(FS_Init_Table(), FS_Init_FileStore());

private
FS_Init_Table : () -> OpenFileDescriptorTable

FS_Init_Table() == {|->};

private
FS_Init_FileStore : () -> FileStore
FS_Init_FileStore() == {<Root> |-> mk_File(mk_Attributes(<Directory>), nil)};

static public
dirName : Path -> Path
dirName(full_path) ==
  if full_path = <Root> or len full_path = 1
  then <Root>
  else [ full_path(i) | i in set inds full_path & i < len full_path ];

static public
isDirectory : File -> bool
isDirectory(file) == file.attributes.fileType = <Directory>;

public
isRoot : Path -> bool
isRoot(path) == path = <Root>;

public
isElemFileStore : Path * FileStore -> bool
isElemFileStore(path, fileStore) == path in set dom fileStore;

types
public FFS_Status =
                    <FFS_StatusSuccess>
                  | <FFS_StatusNotFound>
                  | <FFS_StatusUnknown>
                  | <FS_ErrorDirectoryNotEmpty>
                  | <FS_ErrorFileStillOpen>
                  | <FS_ErrorPathNotFound>
                  | <FS_ErrorInvalidPath>
                  | <FS_ErrorTooManyOpenFiles>;

end FileSystemLayerAlg

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.