[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 vfs-contracts
Status:
Proved!
Axioms: 4, User Theorems: 21 (Proved: 21, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 1242, Interactions: 317
read-inv(0,0)
read-loop-inv(35,8)
write-inv-in0(3,1)
write-inv-post(52,22)
write-loop-inv(9,3)
read-inv-post(18,8)
truncate-inv(227,33)
write-inv-in1(3,1)
write-inv-rec(77,39)
write-prepost(249,60)
read-inv-rec(48,21)
write-block-inv(59,6)
write-inv-ls(3,1)
write-inv-stream(5,2)
write-prepost-partial(238,60)
read-inv-strong(0,0)
write-inode-inv(42,5)
write-inv-meta(3,1)
write-inv-strong(0,0)
writepage-afs-cons(55,13)
read-loop-err(30,3)
write-inv(0,0)
write-inv-others(3,1)
write-inv-strong-rec(27,6)
writepage-prepost(56,23)