[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 aubifs-replay
enrich
   aubifs-inv

with
   

   
   
   functions  replay : address-list × node-store × node-index × key-set → node-index;
              replay-log : address-list × node-store × node-index → node-index;
              replay-one : address × node × node-index → node-index;
   predicates  orphans-cons : node-store × node-index × key-set;
               replay-cons-strong : node-store × node-index × key-set × node-index × key-set × address-list;
               replay-safe : address-list × node-store × node-index;
   
   variables  ro : key-set;
              ro0 : key-set;
              fo : key-set;
              ld : key-set;
              ld0 : key-set;
   
   

   

   axioms orphans-cons
          :  ⊦ orphans-cons(fs, ri, ro) ↔ (∀ ino. inodekey(ino) ∈ ri → (fs[ri[inodekey(ino)]].nlink = 0 ∧ ino ≠ ROOT_INO ↔ inodekey(ino) ∈ ro));
          replay-cons-strong :  ⊦ replay-cons-strong(fs, ri, ro, fi, fo, log) ↔ replay-safe(log, fs, fi ⊖ fo) ∧ replay(log, fs, fi, fo) = ri ⊖ ro;
          replay-safe-empty :  ⊦ replay-safe([], fs, fi);
          used for: s, ls;
          replay-safe-rec
          : ⊦   replay-safe(adr ' + log, fs, ri)
              ↔ adr ∈ fs ∧ ¬ adr ∈ ri ∧ node-cons(fs[adr].key, fs[adr]) ∧ replay-safe(log, fs, replay-one(adr, fs[adr], ri));
          used for: s, ls;
          replay :  ⊦ replay(log, fs, fi, fo) = replay-log(log, fs, fi ⊖ fo);
          replay-log-empty :  ⊦ replay-log([], fs, ri) = ri;
          used for: s, ls;
          replay-log-rec :  ⊦ replay-log(adr ' + log, fs, ri) = replay-log(log, fs, replay-one(adr, fs[adr], ri));
          used for: s, ls;
          replay-ino
          :  ⊦ replay-one(adr, inodenode(key, md, boolvar, n, n0, m), ri) = (n ≠ 0 ∨ key.ino = ROOT_INO ⊃ ri[key, adr];(boolvar ⊃ ri -- key;ri ⊖ key));
          used for: s, ls;
          replay-dentry :  ⊦ replay-one(adr, dentrynode(key, ino), ri) = (ino ≠ 0 ⊃ ri[key, adr];ri -- key);
          used for: s, ls;
          replay-data :  ⊦ replay-one(adr, datanode(key, buf), ri) = (inodekey(key.ino) ∈ ri ⊃ ri[key, adr];ri);
          used for: s, ls;
          replay-trunc :  ⊦ replay-one(adr, truncnode(key, n), ri) = ri \ datakeys(key, n, ri);
          used for: s, ls;

   

   
end enrich