Specification ebm-vol-asm

[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,
data asm specification 
   ebm_vol

   using ebm-asm
, 
         default-volid


   

   
   
   
   
   procedures ebm_vol_get_volume_size# volid × abstract-volumes :  : nat  ;
              ebm_vol_write# nat × nat × nat × nat × buffer × volid : abstract-volumes : error  nondeterministic;
              ebm_vol_read# nat × nat × nat × nat × volid × abstract-volumes : buffer : error  nondeterministic;
              ebm_vol_change# nat × nat × buffer × volid : abstract-volumes : error  nondeterministic;
              ebm_vol_remap# nat × volid : abstract-volumes : error  nondeterministic;
              ebm_vol_unmap# nat × volid : abstract-volumes nonfunctional ;
              ebm_vol_sync_device# abstract-volumes :  : error  nondeterministic;
              ebm_vol_get_page_size# abstract-volumes :  : nat  ;
              ebm_vol_get_leb_size# abstract-volumes :  : nat  ;
              ebm_vol_format# nat : volid × abstract-volumes : error  nondeterministic;
              ebm_vol_recover#  : abstract-volumes : volid × error  nondeterministic;
   variables  VOLSIZE : nat flexible;
              VOLID : volid flexible;
   
   

   

   state variables  VOLID : volid flexible;

   initialization procedure ebm_vol_format#

   if ERR = ESUCCESS

   sequential

   invariants volid :  ⊦ VOLID ∈ AVOLS ∧ VOLID = default-volid;

   

   

   

   recovery procedure ebm_vol_recover#

   if ERR = ESUCCESS

   declarations get-volume-size:
                ebm_vol_get_volume_size#(VOLID, AVOLS; ; N)
                  precondition true;
                  postcondition true;
                {ebm_get_volume_size#(VOLID, AVOLS; ; N)
                }
                write:
                ebm_vol_write#(LNUM, OFFSET, N0, N, BUF, VOLID; AVOLS; ERR)
                  precondition   LNUM < # AVOLS[VOLID] ∧ OFFSET + N ≤ LEB_SIZE ∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE)
                               ∧ N + N0 ≤ # BUF ∧ (AVOLS[VOLID][LNUM].mapped? → OFFSET ≥ AVOLS[VOLID][LNUM].fill)
                ;
                  postcondition true;
                {if   LNUM < # AVOLS[VOLID] ∧ OFFSET + N ≤ LEB_SIZE ∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE)
                    ∧ N + N0 ≤ # BUF ∧ (AVOLS[VOLID][LNUM].mapped? → OFFSET ≥ AVOLS[VOLID][LNUM].fill)
                 then ebm_write#(VOLID, LNUM, OFFSET, N0, N, BUF; AVOLS; ERR)
                 else abort
                }
                read:
                ebm_vol_read#(LNUM, OFFSET, N0, N, VOLID, AVOLS; BUF; ERR)
                  precondition AVOLS[VOLID][LNUM].mapped? ∧ LNUM < # AVOLS[VOLID] ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF;
                  postcondition true;
                {if AVOLS[VOLID][LNUM].mapped? ∧ LNUM < # AVOLS[VOLID] ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF
                 then ebm_read#(VOLID, LNUM, OFFSET, N0, N, AVOLS; BUF; ERR)
                 else abort
                }
                change:
                ebm_vol_change#(LNUM, N, BUF, VOLID; AVOLS; ERR)
                  precondition LNUM < # AVOLS[VOLID] ∧ N ≤ LEB_SIZE ∧ N ≤ # BUF ∧ is-aligned(N, EB_PAGE_SIZE);
                  postcondition true;
                {if LNUM < # AVOLS[VOLID] ∧ N ≤ LEB_SIZE ∧ N ≤ # BUF ∧ is-aligned(N, EB_PAGE_SIZE)
                 then ebm_change#(VOLID, LNUM, N, BUF; AVOLS; ERR)
                 else abort
                }
                remap:
                ebm_vol_remap#(LNUM, VOLID; AVOLS; ERR)
                  precondition LNUM < # AVOLS[VOLID];
                  postcondition true;
                {if LNUM < # AVOLS[VOLID] then {ebm_vol_unmap#(LNUM, VOLID; AVOLS); ebm_map#(VOLID, LNUM; AVOLS; ERR)} else abort
                }
                unmap:
                ebm_vol_unmap#(LNUM, VOLID; AVOLS)
                  precondition LNUM < # AVOLS[VOLID];
                  postcondition true;
                {if LNUM < # AVOLS[VOLID] then ebm_unmap#(VOLID, LNUM; AVOLS) else abort
                }
                sync-device:ebm_vol_sync_device#(AVOLS; ; ERR)  precondition true;  postcondition true;{ebm_sync_device#(AVOLS; ; ERR)}
                get-page-size:ebm_vol_get_page_size#(AVOLS; ; N)  precondition true;  postcondition true;{ebm_get_page_size#(AVOLS; ; N)}
                get-leb-size:ebm_vol_get_leb_size#(AVOLS; ; N)  precondition true;  postcondition true;{ebm_get_leb_size#(AVOLS; ; N)}
                format:
                ebm_vol_format#(VOLSIZE; VOLID, AVOLS; ERR)
                  precondition true;
                  postcondition true;
                {{ebm_format#(; ; AVOLS, ERR); if ERR = ESUCCESS then {VOLID := default-volid; ebm_create_volume#(VOLID, VOLSIZE; AVOLS; ERR)}}
                }
                recover:
                ebm_vol_recover#(; AVOLS; VOLID, ERR)
                  precondition true;
                  postcondition true;
                {{ebm_recover#(; AVOLS; ERR); VOLID := default-volid}
                }
end data asm specification