Specification ablock-store-inv

[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,
enrich
   ablock-store, 
   eraseblock
, 
   address-list-set
, 
   address-data

with
   

   
   
   functions  . .flashsize : elem → nat;
              . .flashsize : list → nat;
              remove-refsize0 : store → store;
              . .to-adr ( . ) : laddress-list × nat → address-list;
              . [ . ] : store × address → elem;
   predicates  . ⊑ . : store × store;
               . =○refsize . : store × store;
               inv-flashsize : list × laddress-list;
               inv : ablock;
               inv : store;
               . ∈ . : address × store;
   
   
   
   

   

   axioms inv-block
          :  ⊦ inv(ablock) ↔ # ablock.list = # ablock.ladrlist ∧ inv-flashsize(ablock.list, ablock.ladrlist) ∧ ¬ dups(ablock.ladrlist);
          used for: ls;
          inv-flashsize :  ⊦ inv-flashsize(x, lax) ↔ # x = # lax ∧ (∀ n. n < # x → lax[n].size = x[n].flashsize);
          inv-store :  ⊦ inv(st) ↔ (∀ n. n ∈ st → inv(st[n]));
          used for: ls;
          blockstore-prefix
          : ⊦   st0 ⊑ st
              ↔   dom st0 ⊆ dom st
                ∧ (∀ n. 
                       n ∈ st0 ∧ n ∈ st
                     →   st0[n].list ⊑ st[n].list ∧ st0[n].ladrlist ⊑ st[n].ladrlist ∧ # st0[n].list = # st0[n].ladrlist
                       ∧ # st[n].list = # st[n].ladrlist);
          used for: lws;
          flashsize-neq-0 :  ⊦ a.flashsize ≠ 0;
          used for: s, ls;
          size-base :  ⊦ [].flashsize = 0;
          used for: s, ls;
          size-rec :  ⊦ (a ' + x).flashsize = a.flashsize + x.flashsize;
          used for: s, ls;
          adrs-empty :  ⊦ ([]).to-adr(n) = [];
          used for: s, ls;
          adrs-rec :  ⊦ (ladr ' + lax).to-adr(n) = @(n, ladr.off, ladr.size) + lax.to-adr(n);
          used for: s, ls;
          in-remove-refsize0 :  ⊦ n ∈ remove-refsize0(st) ↔ n ∈ st ∧ st[n].ref-size ≠ 0;
          used for: ws, lws;
          at-remove-refsize0 :  ⊦ n ∈ st ∧ st[n].ref-size ≠ 0 → remove-refsize0(st)[n] = st[n];
          used for: s, ls;
          in :  ⊦ adr ∈ st ↔ adr.lnum ∈ st ∧ @(adr.pos, adr.size) ∈ st[adr.lnum].ladrlist;
          used for: lws;
          at :  ⊦ adr ∈ st → st[adr] = st[adr.lnum].list[pos(@(adr.pos, adr.size), st[adr.lnum].ladrlist)];
          used for: ls;
          except-refsize-eq :  ⊦ st0 =○refsize st1 ↔ (∀ n. (n ∈ st0 ↔ n ∈ st1) ∧ st0[n].list = st1[n].list ∧ st0[n].ladrlist = st1[n].ladrlist);
          used for: ls;

   

   
end enrich