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

   

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

   

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