[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-asm
import persistence-asm
using persistence-asm
,
apersistence-asm
by mapping persistence_recover# → apersistence_recover#, persistence_read_gnd# → apersistence_read_gnd#,
persistence_read_ind# → apersistence_read_ind#, persistence_read_gblock_nodes# → apersistence_read_gblock_nodes#,
persistence_get_gc_block# → apersistence_get_gc_block#, persistence_add_gnds# → apersistence_add_gnds#,
persistence_add_ind# → apersistence_add_ind#, persistence_is_readonly# → apersistence_is_readonly#,
persistence_get_leb_size# → apersistence_get_leb_size#, persistence_sync# → apersistence_sync#,
persistence_set_gblock_refsize# → apersistence_set_gblock_refsize#,
persistence_set_iblock_refsize# → apersistence_set_iblock_refsize#,
persistence_get_gblock_refsize# → apersistence_get_gblock_refsize#,
persistence_get_iblock_refsize# → apersistence_get_iblock_refsize#,
persistence_get_block_free_size# → apersistence_get_block_free_size#,
persistence_is_log_empty# → apersistence_is_log_empty#, persistence_allocate_gnd# → apersistence_allocate_gnd#,
persistence_deallocate_gnd# → apersistence_deallocate_gnd#, persistence_allocate_ind# → apersistence_allocate_ind#,
persistence_commit# → apersistence_commit#, persistence_requires_commit# → apersistence_requires_commit#,
persistence_format# → apersistence_format#
abstraction abs-istore(WVOL, LPT, ISTORE) ∧ abs-gstore(WVOL, LPT, GSTORE, GINVAL) ∧ ROOTADR = WROOTADR ∧ MAXINO = WMAXINO ∧ NL = LOG
∧ GINVAL < # LPT ∧ OS = WORPHANS ∧ flash-lpt-cons(WLPT, ISTORE0, GSTORE0) ∧ (PSYNCED → synced(WVOL))
∧ (PSTATE = unbuffered → WBUFLEB = nobuffer) ∧ (PSTATE = readonly ↔ AROFS)
∧ (PSTATE ≠ unbuffered ∧ PSTATE ≠ readonly → WBUFLEB = buffered(PSTATE.lnum))
;
end asm refinement