[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,

Specification error-class
enrich
   error
with
   

   
   
   
   predicates  ⌊ . ⌋ : error;
   procedures fail#  :  : error  nondeterministic;
              fail_or_success#  :  : error  nondeterministic;
   variables  ERR : error flexible;
              ERR0 : error flexible;
   
   

   

   axioms class
          :  ⊦ ⌊err⌋  ↔ err ≠ ESUCCESS ∧ err ≠ EEXISTS ∧ err ≠ ENOENT ∧ err ≠ EISDIR ∧ err ≠ ENOTEMPTY ∧ err ≠ ENOTDIR ∧ err ≠ EBADFD ∧ err ≠ EACCESS;
          used for: ls;

   

   declarations fail : fail#(; ; ERR){choose ERR0 with ⌊ERR0⌋  in ERR := ERR0};
                fail-or-success : fail_or_success#(; ; ERR){choose ERR0 with ⌊ERR0⌋  ∨ ERR0 = ESUCCESS in ERR := ERR0};
end enrich