[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 aubifs-internal-asm
import gjournal-asm
using gjournal-asm,
aubifs-internal-asm
by mapping gjournal_recover# → aubifs_core_recover#, gjournal_format# → aubifs_core_format#,
gjournal_index_newino# → aubifs_core_index_newino#, gjournal_index_contains# → aubifs_core_index_contains#,
gjournal_index_lookup# → aubifs_core_index_lookup#, gjournal_index_store# → aubifs_core_index_store#,
gjournal_index_remove# → aubifs_core_index_remove#, gjournal_index_truncate# → aubifs_core_index_truncate#,
gjournal_index_entries# → aubifs_core_index_entries#, gjournal_journal_get# → aubifs_core_journal_get#,
gjournal_journal_add1# → aubifs_core_journal_add1#, gjournal_journal_add2# → aubifs_core_journal_add2#,
gjournal_journal_add3# → aubifs_core_journal_add3#, gjournal_journal_add4# → aubifs_core_journal_add4#,
gjournal_journal_add5# → aubifs_core_journal_add5#, gjournal_journal_sync# → aubifs_core_journal_sync#,
gjournal_journal_gc# → aubifs_core_journal_gc#, gjournal_check_commit# → aubifs_core_check_commit#,
gjournal_commit# → aubifs_core_commit#, gjournal_orphans_contains# → aubifs_core_orphans_contains#,
gjournal_orphans_insert# → aubifs_core_orphans_insert#, gjournal_orphans_remove# → aubifs_core_orphans_remove#
abstraction JRO.keys = RO ∧ P_OS.keys = FO ∧ PRI = RI ∧ PFI = FI ∧ LOG = abs-log(PNL, PSTORE ↓) ∧ FS = nodes(PSTORE ↓, PINVAL)
∧ (CSYNCED → ISYNCED)
;
end asm refinement