[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,
asm refinement
export apersistence-io-asm
import persistence-io-asm
using persistence-io-asm
,
apersistence-io-asm
by mapping persistence_io_recover# → apersistence_io_recover#, persistence_io_commit# → apersistence_io_commit#,
persistence_io_requires_commit# → apersistence_io_requires_commit#,
persistence_io_add_log_leb# → apersistence_io_add_log_leb#, persistence_io_format# → apersistence_io_format#,
persistence_io_get_volume_size# → apersistence_io_get_volume_size#,
persistence_io_get_page_size# → apersistence_io_get_page_size#,
persistence_io_get_leb_size# → apersistence_io_get_leb_size#, persistence_io_write# → apersistence_io_write#,
persistence_io_read# → apersistence_io_read#, persistence_io_remap# → apersistence_io_remap#,
persistence_io_unmap# → apersistence_io_unmap#
abstraction PMAXINO = SB.maxino ∧ PROOTADR = SB.indexaddr ∧ # AVOL = SB.main + # PVOL
∧ PVOL = subarray(AVOL, SB.main, # AVOL - SB.main) ∧ is-encoded(PLOG, AVOL[SB.log].data)
∧ is-encoded(PLPT, lebs(AVOL, SB.lpt, lptlebs(# PVOL, LEB_SIZE))) ∧ is-encoded-pad(PORPHANS, SB.orphsize, AVOL[SB.orph].data)
;
end asm refinement