[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 znode-ops
enrich
   znode, 
   indexnode

with
   

   
   
   functions  scan : key × zbranch-array × nat × nat → nat;
              shl : zbranch-array × nat × nat → zbranch-array;
              shr : zbranch-array × nat × nat → zbranch-array;
              load : ref × index-node → znode;
              save : znode → index-node;
              load : branch-array × nat × nat → zbranch-array;
              save : zbranch-array × nat × nat → branch-array;
              load : branch → zbranch;
              save : zbranch → branch;
   
   
   variables  len : nat;
              nused : nat;
              bv : bool;
   
   

   

   axioms scan-base :  ⊦ scan(key, zbrar, m, 0) = m;
          used for: s, ls;
          scan-rec :  ⊦ scan(key, zbrar, m, n + 1) = (key ≤ zbrar[m].key ⊃ m;scan(key, zbrar, m + 1, n));
          used for: s, ls;
          shr :  ⊦ shr(zbrar, n, m) = copy(zbrar, n, zbrar, n + 1, m - n);
          used for: ls;
          shl :  ⊦ shl(zbrar, n, m) = copy(zbrar, n + 1, zbrar, n, m - n - 1);
          used for: ls;
          load-node :  ⊦ load(r, ind) = mkznode(r, load(ind.branches, 0, ind.usedsize), ind.leaf, false, ind.usedsize);
          used for: ls;
          save-node :  ⊦ save(znd) = indexnode(save(znd.zbranches, 0, znd.usedsize), znd.leaf, znd.usedsize);
          used for: ls;
          load-branches-base :  ⊦ load(brar, m, 0) = mkzbrarray(BRANCH_SIZE);
          used for: s, ls;
          load-branches-rec :  ⊦ load(brar, m, nused + 1) = load(brar, m + 1, nused)[m, load(brar[m])];
          save-branches-base :  ⊦ save(zbrar, m, 0) = mkbrarray(BRANCH_SIZE);
          used for: s, ls;
          save-branches-rec :  ⊦ save(zbrar, m, nused + 1) = save(zbrar, m + 1, nused)[m, save(zbrar[m])];
          load-branch :  ⊦ load(mkbranch(key, adr)) = mkzbranch(key, adr, null);
          used for: s, ls;
          load-entry :  ⊦ load(mkentry(key, adr)) = mkzentry(key, adr);
          used for: s, ls;
          save-branch :  ⊦ save(mkzbranch(key, adr, r)) = mkbranch(key, adr);
          used for: s, ls;
          save-entry :  ⊦ save(mkzentry(key, adr)) = mkentry(key, adr);
          used for: s, ls;

   

   
end enrich