[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 key
data specification
   comment: a datastructure for ubifs keys, @see key.h, ubifs_media.h;

   using nat, 
         string


   data types key
               := inodekey(. .ino : nat) with .inode?
               | datakey(. .ino : nat;. .part : nat) with .data?
               | dentrykey(. .ino : nat;. .name : string) with .dentry?
               ;

   variables  key : key;

   

   
end data specification