[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 cache-asm
Status:
Proved!
Axioms: 22, User Theorems: 31 (Proved: 31, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 5857, Interactions: 115
check-commit(0,0)
fsync-pages(0,0)
inv-format(53,1)
inv-readdir(20,1)
inv-rename-file-dentry(526,5)
inv-truncate-buff-none-uncached(385,6)
mkdir(0,0)
truncate(0,0)
create(0,0)
fsync-pages-inv(312,9)
inv-fsync(100,7)
inv-readpage(95,1)
inv-rename-file-negdentry(299,3)
inv-truncate-buff-some(364,8)
readdir(0,0)
unlink(0,0)
evict(0,0)
fsyncdir(0,0)
inv-fsyncdir(13,2)
inv-recover(63,7)
inv-rename-negdentry(25,3)
inv-unlink(211,2)
readpage(0,0)
write_inode(0,0)
format(0,0)
iget(0,0)
inv-iget(58,1)
inv-renam(29,3)
inv-rmdir(224,2)
inv-write_inode(459,4)
recover(0,0)
writepage(0,0)
fsync(0,0)
inv-check-commit(12,2)
inv-link(233,2)
inv-rename-dentry(29,3)
inv-sync(10,2)
inv-writepage(167,3)
renam(0,0)
fsync-inode(0,0)
inv-create(185,2)
inv-lookup(53,1)
inv-rename-dir-dentry(575,4)
inv-truncate(19,7)
link(0,0)
rmdir(0,0)
fsync-inode-inv(187,2)
inv-evict(224,9)
inv-mkdir(197,2)
inv-rename-dir-negdentry(305,3)
inv-truncate-buff-none-cached(425,8)
lookup(0,0)
sync(0,0)