[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
,
Theorem base summary for Specification apersistence-asm
Status:
Proved!
Axioms: 22, User Theorems: 43 (Proved: 43, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 580, Interactions: 38
add-gnds(0,0)
crash-neutral-allocate-ind(14,0)
crash-neutral-is-log-empty(4,0)
crash-neutral-set-iblock-refsize(48,12)
get-leb-size(0,0)
inv-get-block-free-size(8,0)
inv-read-gnd(15,0)
is-readonly(0,0)
sync(0,0)
add-ind(0,0)
crash-neutral-commit(24,0)
crash-neutral-is-readonly(4,0)
crash-neutral-sync(19,2)
inv-add-gnds(39,6)
inv-get-gblock-refsize(5,0)
inv-read-ind(12,0)
read-gblock(0,0)
allocate-gnd(0,0)
crash-neutral-deallocate-gnd(14,0)
crash-neutral-read-gblock(11,0)
deallocate-gnd(0,0)
inv-add-ind(29,3)
inv-get-gc-block(9,0)
inv-recovery(11,0)
read-gnd(0,0)
allocate-ind(0,0)
crash-neutral-get-block-free-size(10,1)
crash-neutral-read-gnd(14,0)
format(0,0)
inv-allocate-gnd(19,2)
inv-get-iblock-refsize(5,0)
inv-requires-commit(4,0)
read-ind(0,0)
commit(0,0)
crash-neutral-get-gblock-refsize(5,0)
crash-neutral-read-ind(11,0)
get-block-free-size(0,0)
inv-allocate-ind(16,2)
inv-get-leb-size(4,0)
inv-set-gblock-refsize(5,0)
recovery(0,0)
crash-neutral-add-gnds(36,3)
crash-neutral-get-gc-block(6,0)
crash-neutral-recovery(13,0)
get-gblock-refsize(0,0)
inv-commit(25,1)
inv-is-log-empty(4,0)
inv-set-iblock-refsize(16,4)
requires-commit(0,0)
crash-neutral-add-ind(22,1)
crash-neutral-get-iblock-refsize(5,0)
crash-neutral-requires-commit(4,0)
get-gc-block(0,0)
inv-deallocate-gnd(12,0)
inv-is-readonly(4,0)
inv-sync(17,0)
set-gblock-refsize(0,0)
crash-neutral-allocate-gnd(19,0)
crash-neutral-get-leb-size(4,0)
crash-neutral-set-gblock-refsize(11,1)
get-iblock-refsize(0,0)
inv-format(11,0)
inv-read-gblock(12,0)
is-log-empty(0,0)
set-iblock-refsize(0,0)