[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,
enrich
IOrefine-def,
streamseq-mon-lim
,
project-right
with
functions
repls
: ('s × 'a × 's → Bool) × ('cs × 'ca × 'cs → Bool) × ('ca → 'pa) × ('a → 'pa) × ('aa → 'pa) × ('ca → Option('e)) × ('aa → Option('e)) ×
Stream(('s, 'cs)) × Stream('pa) × Stream('as) × Stream('aa)
→ Stream(('s, 'as))
;
repla
: ('s × 'a × 's → Bool) × ('cs × 'ca × 'cs → Bool) × ('ca → 'pa) × ('a → 'pa) × ('aa → 'pa) × ('ca → Option('e)) × ('aa → Option('e)) ×
Stream(('s, 'cs)) × Stream('pa) × Stream('as) × Stream('aa)
→ Stream('pa)
;
repls
: ('s × 'a × 's → Bool) × ('cs × 'ca × 'cs → Bool) × ('ca → 'pa) × ('a → 'pa) × ('aa → 'pa) × ('ca → Option('e)) × ('aa → Option('e)) ×
List(('s, 'cs)) × List('pa) × Stream('as) × Stream('aa)
→ List(('s, 'as))
;
repla
: ('s × 'a × 's → Bool) × ('cs × 'ca × 'cs → Bool) × ('ca → 'pa) × ('a → 'pa) × ('aa → 'pa) × ('ca → Option('e)) × ('aa → Option('e)) ×
List(('s, 'cs)) × List('pa) × Stream('as) × Stream('aa)
→ List('pa)
;
lift : List('as) × 's → List(('s, 'as));
predicates
nounsharedextR : ('ca → 'pa) × ('ca → Option('e)) × ('a → 'pa);
comment: true, if C has no unshared external action;
sameshared : ('ca → 'pa) × ('aa → 'pa) × ('a → 'pa);
variables
cstart : 'cs → Bool;
astart : 'as → Bool;
start : 's → Bool;
pcstart : ('s, 'cs) → Bool;
pastart : ('s, 'as) → Bool;
cstep : 'cs × 'ca × 'cs → Bool;
astep : 'as × 'aa × 'as → Bool;
step : 's × 'a × 's → Bool;
pcstep : ('s, 'cs) × 'pa × ('s, 'cs) → Bool;
pastep : ('s, 'as) × 'pa × ('s, 'as) → Bool;
cext : 'ca → Option('e);
aext : 'aa → Option('e);
ext : 'a → Option('e);
pext : 'pa → Option('e);
cren : 'ca → 'pa;
aren : 'aa → 'pa;
ren : 'a → 'pa;
cs : 'cs;
as : 'as;
s : 's;
pcs : ('s, 'cs);
pas : ('s, 'as);
ca : 'ca;
aa : 'aa;
a : 'a;
pa : 'pa;
e : 'e;
pcσ : Stream(('s, 'cs));
pcsl : List(('s, 'cs));
paσ : Stream(('s, 'as));
pasl : List(('s, 'as));
pasf : Nat → ('s, 'as);
pcsf : Nat → ('s, 'cs);
aσ : Stream('as);
asl : List('as);
cσ : Stream('cs);
csl : List('cs);
β : Stream('e);
aα : Stream('aa);
cα : Stream('ca);
cal : List('ca);
aal : List('aa);
pα : Stream('pa);
pal : List('pa);
paf : Nat → 'pa;
aaf : Nat → 'aa;
caf : Nat → 'ca;
csf : Nat → 'cs;
asf : Nat → 'as;
n : Nat;
redext : 'e → Option('f);
el : List('e);
axioms
sameshared-def: sameshared(cren, aren, ren) ↔ (∀ a. cod(cren)(ren(a)) ↔ cod(aren)(ren(a)));
comment: program shares the same events with C and A;
nounsharedextR-def: nounsharedextR(cren, cext, ren) ↔ (∀ ca. cext(ca) ≠ None → (∃ a. ren(a) = cren(ca)));
lift-base: lift([], s) = [];
used for: s, ls;
lift-rec: lift(as ' + asl, s) = (s, as) ' + lift(asl, s);
used for: s, ls;
repls-base: repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ', [], ⌜as '⌝ + aσ, aα) = (s, as) ';
used for: s, ls;
repla-base: repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ', [], ⌜as '⌝ + aσ, aα) = [];
used for: s, ls;
repls-rec-addS:
step(s, a, s0) ∧ ¬ cod(cren)(ren(a))
→ repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs) ' + pcsl, ren(a) ' + pal, ⌜as '⌝ + aσ, aα)
= (s, as) ' + repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs) ' + pcsl, pal, ⌜as '⌝ + aσ, aα);
used for: s, ls;
repla-rec-addS:
step(s, a, s0) ∧ ¬ cod(cren)(ren(a))
→ repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs) ' + pcsl, ren(a) ' + pal, ⌜as '⌝ + aσ, aα)
= ren(a) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs) ' + pcsl, pal, ⌜as '⌝ + aσ, aα);
used for: s, ls;
repls-rec-skip:
cstep(cs, ca, cs0) ∧ ¬ cod(ren)(cren(ca))
→ repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s, cs0) ' + pcsl, cren(ca) ' + pal, ⌜as '⌝ + aσ, aα)
= repls(step, cstep, cren, ren, aren, cext, aext, (s, cs0) ' + pcsl, pal, ⌜as '⌝ + aσ, aα);
used for: s, ls;
repla-rec-skip:
cstep(cs, ca, cs0) ∧ ¬ cod(ren)(cren(ca))
→ repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s, cs0) ' + pcsl, cren(ca) ' + pal, ⌜as '⌝ + aσ, aα)
= repla(step, cstep, cren, ren, aren, cext, aext, (s, cs0) ' + pcsl, pal, ⌜as '⌝ + aσ, aα);
used for: s, ls;
repls-rec-addboth:
step(s, a, s0) ∧ cstep(cs, ca, cs0) ∧ aext !(⌜aal⌝ ) = [] ∧ cext(ca) = aext(aa) ∧ cren(ca) = ren(a) ∧ n = # aal
→ repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a) ' + pal, aσ, ⌜aal⌝ + ⌜aa '⌝ + aα)
= lift(aσ.take(n), s) + (s, aσ[n]) ' + repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal, aσ.drop(n + 1), aα);
used for: s, ls;
repla-rec-addboth:
step(s, a, s0) ∧ cstep(cs, ca, cs0) ∧ cren(ca) = ren(a) ∧ aext !(⌜aal⌝ ) = [] ∧ cext(ca) = aext(aa) ∧ n = # aal
→ repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a) ' + pal, aσ, ⌜aal⌝ + ⌜aa '⌝ + aα)
= aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal, aσ.drop(n + 1), aα);
used for: s, ls;
replstate-fin-def:
# pcsl = # pal + 1
→ repls(step, cstep, cren, ren, aren, cext, aext, ⌜pcsl⌝ , ⌜pal⌝ , aσ, aα)
= ⌜repls(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, aσ, aα)⌝ ;
replaction-fin-def:
# pcsl = # pal + 1
→ repla(step, cstep, cren, ren, aren, cext, aext, ⌜pcsl⌝ , ⌜pal⌝ , aσ, aα)
= ⌜repla(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, aσ, aα)⌝ ;
replstate-inf-def:
cext !(πra(step, cstep, ren, cren, ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα)
→ repls(step, cstep, cren, ren, aren, cext, aext, ⌜pcsf⌝ , ⌜paf⌝ , aσ, aα)
= lim(⌜λ n. ⌜repls(step, cstep, cren, ren, aren, cext, aext, pcsf.take(n + 1), paf.take(n), aσ, aα)⌝ ⌝ );
replaction-inf-def:
cext !(πra(step, cstep, ren, cren, ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα)
→ repla(step, cstep, cren, ren, aren, cext, aext, ⌜pcsf⌝ , ⌜paf⌝ , aσ, aα)
= lim(⌜λ n. ⌜repla(step, cstep, cren, ren, aren, cext, aext, pcsf.take(n + 1), paf.take(n), aσ, aα)⌝ ⌝ );
theorems
repl-exec:
IOAut?(IOAut(start, step, ext)), IOAut?(IOAut(cstart, cstep, cext)), IOAut?(IOAut(astart, astep, aext)), nounsharedextR(cren, cext, ren),
nounsharedextR(aren, aext, ren), sameshared(cren, aren, ren), Πok(ext, cext, ren, cren), Πok(ext, aext, ren, aren),
exec(Π(IOAut(start, step, ext), IOAut(cstart, cstep, cext), ren, cren))(pcσ, pα), exec(IOAut(astart, astep, aext))(aσ, aα),
cext !(πra(step, cstep, ren, cren, pcσ, pα)) = aext !(aα)
⊦ exec(Π(IOAut(start, step, ext), IOAut(astart, astep, aext), ren, aren))
(repls(step, cstep, cren, ren, aren, cext, aext, pcσ, pα, aσ, aα), repla(step, cstep, cren, ren, aren, cext, aext, pcσ, pα, aσ, aα));
comment: first formula ensures that there are no external C actions which are unshared;
refines-product:
IOAut?(IOAut(start, step, ext)), IOAut?(IOAut(cstart, cstep, cext)), IOAut?(IOAut(astart, astep, aext)), nounsharedextR(cren, cext, ren),
nounsharedextR(aren, aext, ren), sameshared(cren, aren, ren), Πok(ext, cext, ren, cren), Πok(ext, aext, ren, aren),
C_≤T_A(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext))
⊦ C_≤T_A(Π(IOAut(start, step, ext), IOAut(cstart, cstep, cext), ren, cren), Π(IOAut(start, step, ext), IOAut(astart, astep, aext), ren, aren));
refines-hidingproduct:
IOAut?(IOAut(start, step, ext)), IOAut?(IOAut(cstart, cstep, cext)), IOAut?(IOAut(astart, astep, aext)), nounsharedextR(cren, cext, ren),
nounsharedextR(aren, aext, ren), sameshared(cren, aren, ren), Πhok(ext, cext, ren, cren, redext), Πhok(ext, aext, ren, aren, redext),
C_≤T_A(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext))
⊦ C_≤T_A
(Πh(IOAut(start, step, ext), IOAut(cstart, cstep, cext), ren, cren, redext),
Πh(IOAut(start, step, ext), IOAut(astart, astep, aext), ren, aren, redext));
end enrich