Specification dcache-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 
   dcache

   using cache-base, 
         error-class


   

   
   
   
   
   procedures dcache_format#  :  : dcache × error  ;
              dcache_recovery#  :  : dcache × error  ;
              dcache_get# nat × string × dcache : bool × dentry × error nonfunctional ;
              dcache_set# nat × string × dentry : error × dcache nonfunctional ;
              dcache_delete# nat × string : error × dcache nonfunctional ;
   variables  DCACHE : dcache flexible;
              P_INO : nat flexible;
              NAME : string flexible;
              HIT : bool flexible;
              DENT : dentry flexible;
              KEY : key flexible;
   
   

   

   state variables  DCACHE : dcache flexible;

   initialization procedure dcache_format#

   if ERR = ESUCCESS

   sequential

   

   crash predicate true

   with crash-neutrality

   

   recovery procedure dcache_recovery#

   if ERR = ESUCCESS

   declarations format:dcache_format#(; ; DCACHE, ERR)  precondition true;  postcondition true;{{DCACHE := ∅; ERR := ESUCCESS}}
                recovery:dcache_recovery#(; ; DCACHE, ERR)  precondition true;  postcondition true;{{DCACHE := ∅; ERR := ESUCCESS}}
                get:
                dcache_get#(P_INO, NAME, DCACHE; HIT, DENT, ERR)
                  precondition true;
                  postcondition true;
                {{let KEY = dentrykey(P_INO, NAME) in if KEY ∈ DCACHE then {DENT := DCACHE[KEY]; HIT := true} else HIT := false; ERR := ESUCCESS}
                }
                set:
                dcache_set#(P_INO, NAME, DENT; ERR, DCACHE)
                  precondition true;
                  postcondition true;
                {let KEY = dentrykey(P_INO, NAME) in DCACHE[KEY] := DENT
                }
                delete:
                dcache_delete#(P_INO, NAME; ERR, DCACHE)
                  precondition true;
                  postcondition true;
                {let KEY = dentrykey(P_INO, NAME) in DCACHE := DCACHE -- KEY
                }
end data asm specification