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

View long theorem info. View the proof. 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,

Theorem traverse

btree_traverse#(MOD, RP, ADR0, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, DIRTY, EXISTS, ADR, ZH, ISTORE; ERR) {btree_io_load#(RP, ADR0, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, ZH; ERR); if ERR = ESUCCESS then {if ZH[R].leaf then let N = 0 in {btree_io_scan#(MOD.key, 0, R, ZH; N); let FOUND = N < ZH[R].usedsize ∧ ZH[R].zbranches[N].key = MOD.key in {EXISTS := FOUND ∧ ZH[R].zbranches[N].entry?; if EXISTS then ADR := ZH[R].zbranches[N].adr; if MOD.contains? then {ERR := ESUCCESS; DIRTY := false} else if MOD.lookup? then {ERR := ESUCCESS; DIRTY := false} else if MOD.store? then {if ¬ FOUND then {btree_io_shift_right#(N, R; ZH); ZH[R].usedsize := ZH[R].usedsize + 1}; ZH[R].zbranches[N] := mkzentry(MOD.key, MOD.adr); DIRTY := true; ERR := ESUCCESS} else if MOD.remove? then if FOUND then {btree_io_shift_left#(N, R; ZH); ZH[R].usedsize := ZH[R].usedsize - 1; DIRTY := true; ERR := ESUCCESS} else {DIRTY := false; ERR := ESUCCESS}}} else let N = 0 in {btree_io_scan#(MOD.key, 1, R, ZH; N); let RC = ZH[R].zbranches[N].child, ADRC = ZH[R].zbranches[N].adr in {btree_traverse# (MOD, R, ADRC, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RC, DIRTY, EXISTS, ADR, ZH, ISTORE; ERR); if ERR = ESUCCESS then if ZH[RC].usedsize = BRANCH_SIZE then let RL = null, RR = null, POSITION = MIN_SIZE in {btree_io_split#(POSITION, RC; RL, RR, ERR, ZH); btree_io_shift_right#(N, R; ZH); ZH[R].zbranches[N].child := RL; ZH[R].zbranches[N].key := ZH[RL].zbranches[POSITION - 1].key; ZH[R].zbranches[N + 1].child := RR; ZH[R].usedsize := ZH[R].usedsize + 1; DIRTY := true} else if ZH[RC].usedsize = 0 ∧ ZH[R].usedsize ≠ 0 then {btree_io_shift_left#(N, R; ZH); ZH[R].usedsize := ZH[R].usedsize - 1; DIRTY := true; ZH := ZH -- RC} else ZH[R].zbranches[N].child := RC}}; btree_io_dirty#(R, ADR0, DIRTY, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ERR, ZH, ISTORE)} }