state-var-allowed{i:l}(R;dd;x;T) ==
let S,ds,da = dd in
i:{i:Id| (i 
S)}
((kfpf-domain(da i).(
read-allowed(R;k;i;[x]))
(write-allowed(R;k;i;x)))
(
R-affects(R;x;i))
R-decls-compat(R;es-decl-set-single(i;x : T;
)))
Definitions :
spreadn: spread3,
all: x:A. B[x],
set: {x:A| B[x]} ,
l_member: (x l),
Id: Id,
l_all: (xL.P[x]),
fpf-domain: fpf-domain(f),
apply: f a,
Knd: Knd,
cons: [car / cdr],
nil: [],
and: P Q,
not: A,
assert: b,
R-decls-compat: R-decls-compat(R;dd),
es-decl-set-single: es-decl-set-single(i;ds;da),
fpf-single: x : v,
fpf-empty:
FDL editor aliases :
state-var-allowed
state-var-allowed\{i:l\}(R;dd;x;T) ==
let S,ds,da = dd in
\mforall{}i:\{i:Id| (i \mmember{} S)\}
((\mforall{}k\mmember{}fpf-domain(da i).(\muparrow{}read-allowed(R;k;i;[x])) \mwedge{} (\muparrow{}write-allowed(R;k;i;x)))
\mwedge{} (\mneg{}\muparrow{}R-affects(R;x;i))
\mwedge{} R-decls-compat(R;es-decl-set-single(i;x : T;\motimes{})))
Date html generated:
2010_08_27-AM-09_32_27
Last ObjectModification:
2009_12_16-AM-01_10_26
Home
Index