[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 Instance
instantiate AccessControl

< MeydenIntrans

with Properties
by mapping : systemstate → (name × Agent → Data); : secdomain → domain; : value → Data; : command → action; : name → name, Agent; 
           initialstate → [λ nam, ag. null]; null → [null]; cdom → [dom]; contents → [λ s, nam, ag. s(nam, ag)]; step → [STEP#]; obs → [obs]; 
           observe → [λ nam, ag, domvar. observe(domvar, nam, ag)]; alter → [λ nam, ag, domvar. alter(domvar, nam, ag)]; ⇒ → [⇒]; eqd → [eqd]; co → a; 
           sys → s; sys0 → s0; sys1 → s1; d → domvar; d0 → domvar0; d1 → domvar1; nam → nam, ag; v → v; v0 → v0; v1 → v1;
   rename + → +; .first → .first; ' → '; + → +; + → +; ++ → ++; .last → .last; mklist → mklist; fillfirst → fillfirst; ++ → ++; { } → { }; -- → --; 
          run → run; run → run; ipurge → ipurge; sources → sources; ∈ → ∈; ∈ → ∈; eqds → eqds; secure → secure; co0 → (a3); co1 → (a4); co2 → (a5);
end instantiate