[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 awbuf-asm
Status:
Proved!
Axioms: 17, User Theorems: 49 (Proved: 49, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 595, Interactions: 40
add-log-leb(0,0)
crash-neutral-get-page-size(4,0)
crash-neutral-unmap(18,6)
get-page-size(0,0)
inv-get-leb-size(3,0)
inv-requires-commit(3,0)
requires-commit(0,0)
synced-get-volume-size(2,0)
unmap(0,0)
commit(0,0)
crash-neutral-get-volume-size(4,0)
crash-neutral-write-buf(22,1)
get-volume-size(0,0)
inv-get-page-size(3,0)
inv-unmap(5,0)
synced-add-log-leb(25,1)
synced-is-readonly(2,0)
write-buf(0,0)
crash-neutral-add-log-leb(13,1)
crash-neutral-is-readonly(4,0)
destroy-buf(0,0)
inv-add-log-leb(13,1)
inv-get-volume-size(4,0)
inv-write-buf(28,0)
synced-commit(35,1)
synced-move-buf(2,0)
crash-neutral-commit(18,1)
crash-neutral-move-buf(15,1)
enter-readonly(0,0)
inv-commit(18,0)
inv-is-readonly(3,0)
is-readonly(0,0)
synced-destroy-buf(2,0)
synced-read-buf(2,0)
crash-neutral-destroy-buf(8,0)
crash-neutral-read-buf(18,2)
format(0,0)
inv-destroy-buf(9,1)
inv-move-buf(21,3)
move-buf(0,0)
synced-enter-readonly(2,0)
synced-remap(38,2)
crash-neutral-enter-readonly(4,0)
crash-neutral-recover(12,1)
fwd-buffered-mapped(3,1)
inv-enter-readonly(3,0)
inv-read-buf(19,0)
read-buf(0,0)
synced-get-buf(2,0)
synced-requires-commit(2,0)
crash-neutral-get-buf(4,0)
crash-neutral-remap(13,1)
get-buf(0,0)
inv-format(21,1)
inv-recover(11,0)
recover(0,0)
synced-get-leb-size(2,0)
synced-unmap(6,0)
crash-neutral-get-leb-size(4,0)
crash-neutral-requires-commit(4,0)
get-leb-size(0,0)
inv-get-buf(3,0)
inv-remap(14,0)
remap(0,0)
synced-get-page-size(2,0)
synced-write-buf(122,15)