[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification posix-event
data specification
   

   using nat, metadata, 
         buffer, stringset, 
         seekflag, path, 
         mode, error-class, 
         inode

   posix-event
    = mkdir(. .path : path;. .meta : metadata;. .err : error)
    | rmdir(. .path : path;. .err : error)
    | create(. .path : path;. .meta : metadata;. .err : error)
    | unlink(. .path : path;. .err : error)
    | renam(. .path : path;. .path' : path;. .err : error)
    | link(. .path : path;. .path' : path;. .err : error)
    | open(. .path : path;. .fd : nat;. .mode : mode;. .err : error)
    | close(. .fd : nat;. .err : error)
    | read(. .fd : nat;. .buf : buffer;. .n : nat;. .err : error)
    | write(. .fd : nat;. .buf : buffer;. .n : nat;. .err : error)
    | seek(. .fd : nat;. .n : nat;. .whence : seekflag;. .err : error)
    | readmeta(. .path : path;. .meta : metadata;. .err : error)
    | writemeta(. .path : path;. .meta : metadata;. .err : error)
    | readdir(. .path : path;. .names : stringset;. .err : error)
    | truncate(. .path : path;. .n : nat;. .err : error)
    | crash
    ;

   variables  posix-event : posix-event;

   

   
end data specification