[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 path-permission
enrich
   permission-param
, 
   permission
with
   

   
   
   
   predicates  px : user × path × state;
               py : user × path × state;
               pr : user × path × state;
               pw : user × path × state;
   
   

   

   axioms px :  ⊦ px(user, p, st) ↔ (∀ q. q ⊑ p → px(user, meta(q, st)));
          pr :  ⊦ pr(user, p, st) ↔ pr(user, meta(p, st)) ∧ (p ≠ ε → px(user, parent(p), st));
          pw :  ⊦ pw(user, p, st) ↔ pw(user, meta(p, st)) ∧ (p ≠ ε → px(user, parent(p), st));
          py :  ⊦ py(user, p, st) ↔ pw(user, meta(p, st)) ∧ px(user, p, st);

   

   
end enrich