[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 heap
Status:
Proved!
Axioms: 14, User Theorems: 34 (Proved: 34, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 112, Interactions: 34
alloc(0,0)
at-write-mod-three-other(2,0)
at-write-other(2,0)
exin(7,2)
in-write-strong(2,0)
sanity(0,0)
sw-del-add(9,4)
alloc-write(3,1)
at-write-mod-three-other-2(2,0)
at-write-same(2,0)
ext(0,0)
nonnull(2,0)
size-alloc(0,0)
sw-del-add-01(3,1)
at-alloc(0,0)
at-write-mod-three-other-3(2,0)
at-write-same-alloc(2,0)
gen(0,0)
overwrite(2,1)
size-emp(0,0)
sw-delwr(3,1)
at-del(0,0)
at-write-mod-three-other-4(2,0)
del-new(5,2)
in-alloc(0,0)
overwrite-split(2,1)
size-write(0,0)
sw-put(5,2)
at-write(0,0)
at-write-mod-two-other(2,0)
del-notin(5,2)
in-del(0,0)
overwrite-split2(2,1)
size-zero(5,2)
write-again(5,2)
at-write-mod-other(2,0)
at-write-mod-two-other-2(2,0)
del-sw(2,1)
in-emp(0,0)
put-eq(5,1)
structind(12,6)
write-del(2,1)
at-write-mod-other-2(2,0)
at-write-mod-two-other-3(2,0)
del-twice(2,1)
in-write(0,0)
rm-size(2,1)
sw-alloc-put(3,1)