data asm specification 
   ebm_avol

   using avolume, ebm-vol-inv

   

   
   
   
   
   procedures ebm_avol_get_volume_size# avolume :  : nat  ;
              ebm_avol_write# nat × nat × nat × nat × buffer : avolume : error  nondeterministic;
              ebm_avol_read# nat × nat × nat × nat × avolume : buffer : error  nondeterministic;
              ebm_avol_change# nat × nat × buffer : avolume : error  nondeterministic;
              ebm_avol_remap# nat : avolume : error  nondeterministic;
              ebm_avol_unmap# nat : avolume nonfunctional ;
              ebm_avol_sync_device# avolume :  : error  nondeterministic;
              ebm_avol_get_page_size# avolume :  : nat  ;
              ebm_avol_get_leb_size# avolume :  : nat  ;
              ebm_avol_format# nat :  : avolume × error  nondeterministic;
              ebm_avol_recover#  : avolume : error  nondeterministic;
   variables  AVOL : avolume flexible;
              BUF : buffer flexible;
              BUF0 : buffer flexible;
              N : nat flexible;
              N0 : nat flexible;
              N1 : nat flexible;
              LNUM : nat flexible;
              OFFSET : nat flexible;
              ERR : error flexible;
              ERR0 : error flexible;
              VOLSIZE : nat flexible;
   
   

   

   state variables  AVOL : avolume flexible;

   initialization procedure ebm_avol_format#

   if ERR = ESUCCESS

   sequential

   invariants inv :  ⊦ ebm-vol-inv(AVOL);

   crash predicate AVOL` ⊆ AVOL

   with crash-neutrality

   

   recovery procedure ebm_avol_recover#

   if ERR = ESUCCESS

   declarations get-volume-size:ebm_avol_get_volume_size#(AVOL; ; N)  precondition true;  postcondition true;{N := # AVOL}
                write:
                ebm_avol_write#(LNUM, OFFSET, N0, N, BUF; AVOL; ERR)
                  precondition   LNUM < # AVOL ∧ AVOL[LNUM].mapped? ∧ # AVOL[LNUM].data ≤ OFFSET ∧ is-aligned(OFFSET, EB_PAGE_SIZE)
                               ∧ is-aligned(N, EB_PAGE_SIZE) ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF
                ;
                  postcondition true;
                {if   LNUM < # AVOL ∧ AVOL[LNUM].mapped? ∧ # AVOL[LNUM].data ≤ OFFSET ∧ is-aligned(OFFSET, EB_PAGE_SIZE)
                    ∧ is-aligned(N, EB_PAGE_SIZE) ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF
                 then {fail_or_success#(; ; ERR); 
                       if ERR = ESUCCESS
                       then if N ≠ 0 then AVOL[LNUM] := mapped(AVOL[LNUM].data + mkempbuf(OFFSET - # AVOL[LNUM].data) + subarray(BUF, N0, N))
                       else choose N1
                            with N1 < N ∧ is-aligned(N1, EB_PAGE_SIZE)
                            in if N1 ≠ 0 then AVOL[LNUM] := mapped(AVOL[LNUM].data + mkempbuf(OFFSET - # AVOL[LNUM].data) + subarray(BUF, N0, N1))
                            ifnone skip}
                 else abort
                }
                read:
                ebm_avol_read#(LNUM, OFFSET, N0, N, AVOL; BUF; ERR)
                  precondition LNUM < # AVOL ∧ AVOL[LNUM].mapped? ∧ N0 + N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE;
                  postcondition true;
                {if LNUM < # AVOL ∧ AVOL[LNUM].mapped? ∧ N0 + N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE
                 then {fail_or_success#(; ; ERR); 
                       if ERR = ESUCCESS
                       then BUF := copy(AVOL[LNUM].data + mkempbuf(LEB_SIZE - # AVOL[LNUM].data), OFFSET, BUF, N0, N)
                       else choose BUF0
                            with # BUF0 = # BUF ∧ range=(BUF, 0, BUF0, 0, N0) ∧ range=(BUF, N0 + N, BUF0, N0 + N, # BUF - N0 + N)
                            in BUF := BUF0}
                 else abort
                }
                change:
                ebm_avol_change#(LNUM, N, BUF; AVOL; ERR)
                  precondition LNUM < # AVOL ∧ N ≤ # BUF ∧ N ≤ LEB_SIZE ∧ is-aligned(N, EB_PAGE_SIZE);
                  postcondition true;
                {if LNUM < # AVOL ∧ N ≤ # BUF ∧ N ≤ LEB_SIZE ∧ is-aligned(N, EB_PAGE_SIZE)
                 then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then AVOL[LNUM] := mapped(subarray(BUF, 0, N))}
                 else abort
                }
                remap:
                ebm_avol_remap#(LNUM; AVOL; ERR)
                  precondition LNUM < # AVOL;
                  postcondition true;
                {if LNUM < # AVOL
                 then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then AVOL[LNUM] := mapped(mkbuf(0)) else {skip or AVOL[LNUM] := unmapped}}
                 else abort
                }
                unmap:
                ebm_avol_unmap#(LNUM; AVOL)
                  precondition LNUM < # AVOL;
                  postcondition true;
                {if LNUM < # AVOL then AVOL[LNUM] := unmapped else abort
                }
                sync-device:ebm_avol_sync_device#(AVOL; ; ERR)  precondition true;  postcondition true;{fail_or_success#(; ; ERR)}
                get-page-size:ebm_avol_get_page_size#(AVOL; ; N)  precondition true;  postcondition true;{N := EB_PAGE_SIZE}
                get-leb-size:ebm_avol_get_leb_size#(AVOL; ; N)  precondition true;  postcondition true;{N := LEB_SIZE}
                format:
                ebm_avol_format#(VOLSIZE; ; AVOL, ERR)
                  precondition true;
                  postcondition true;
                {{fail_or_success#(; ; ERR); if ERR = ESUCCESS then AVOL := fill(mkavolume(VOLSIZE), unmapped) else AVOL := ?}
                }
                recover:
                ebm_avol_recover#(; AVOL; ERR)
                  precondition true;
                  postcondition true;
                {{fail_or_success#(; ; ERR); if ERR ≠ ESUCCESS then AVOL := ?}
                }
end data asm specification