[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 wbuf-refine
Status:
Proved!
Axioms: 0, User Theorems: 24 (Proved: 24, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 1208, Interactions: 205
abs-buffered(4,1)
nat0(2,0)
refine-destroy-buf(34,6)
refine-get-volume-size(9,0)
refine-requires-commit(9,0)
abs-unbuffered(7,2)
nat1(2,0)
refine-enter-readonly(18,4)
refine-is-readonly(8,0)
refine-unmap(26,3)
at-append-cut(2,1)
recovery(80,20)
refine-get-buf(8,0)
refine-move-buf(79,9)
refine-write-buf(244,36)
initialization(56,2)
refine-add-log-leb(115,12)
refine-get-leb-size(9,0)
refine-read-buf(321,94)
synced(2,0)
mod-to-aligndown-minus(2,0)
refine-commit(80,6)
refine-get-page-size(8,0)
refine-remap(83,9)