[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
heap-aux-inst
with
functions mk : refset × (ref → obj) × (ref → aux) → heap-aux;
. [ . ] : heap-aux × ref × obj × aux → heap-aux;
. [ . ]o : heap-aux × ref → obj;
. [ . ]a : heap-aux × ref → aux;
. ==> ( . ) : ref × obj × aux → heap-aux → bool;
_∃ . : (obj × aux → heap-aux → bool) → heap-aux → bool;
predicates . [ . ] : (heap-aux → bool) × refset × (ref → obj) × (ref → aux);
variables f : ref → obj;
g : ref → aux;
rR : ref → heap-aux → bool;
oaR : obj × aux → heap-aux → bool;
rrR : ref × ref → heap-aux → bool;
hR : heap-aux → bool;
hP : heap-aux → bool;
h : heap-aux;
ha : heap-aux;
oa : objaux;
r : ref;
o : obj;
a : aux;
rs : refset;
bv : bool;
axioms
ex3 : ⊦ _∃ oaR = __∃(λ oa. oaR(oa.obj, oa.aux));
used for: ls;
selo-def : ⊦ h[r]o = h[r]__.obj;
used for: ls;
sela-def : ⊦ h[r]a = h[r]__.aux;
used for: ls;
mod-def : ⊦ h[r, o, a] = h[r, o ×× a]__;
used for: ls;
modifysep-def : ⊦ hP[rs, f, g] ↔ hP[rs, λ r. f(r) ×× g(r)]__;
used for: ls;
maplet-def : ⊦ r ==>(o, a) = r __=>(o ×× a);
used for: ls;
mk-def : ⊦ mk(rs, f, g) = __mk(rs, λ r. f(r) ×× g(r));
used for: ls;
theorems at-mk-M01 : ⊦ r ∈ rs → mk(rs, f, g)[r]o = f(r);
used for: s;
at-mk-M02 : ⊦ r ∈ rs → mk(rs, f, g)[r]a = g(r);
used for: s;
in-mk : ⊦ r ∈ mk(rs, f, g) ↔ r ∈ rs;
used for: s;
apply : ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g));
at-rw : ⊦ (r ==>(o, a) * hR)[rs, f, g] → (f(r) = o ∧ g(r) = a ↔ true);
at-rw0 : ⊦ r ==>(o, a)[rs, f, g] → (f(r) = o ∧ g(r) = a ↔ true);
at-unil-M01 : ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs0 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]o = f(r);
used for: s;
at-unil-M02 : ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs0 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]a = g(r);
used for: s;
at-unir-M01 : ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs1 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]o = f0(r);
used for: s;
at-unir-M02 : ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs1 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]a = g0(r);
used for: s;
del : ⊦ mk(rs -- r, f, g) = mk(rs, f, g) -- r;
disj : ⊦ mk(rs0, f, g) ⊥ mk(rs1, f0, g0) ↔ rs0 ∩ rs1 = ∅;
used for: s;
emp : ⊦ mk(∅, f, g) = ∅;
used for: s;
ex1-shift : ⊦ (_∃ rR * hR)[rs, f, g] ↔ (∃ r. (rR(r) * hR)[rs, f, g]);
ex2-shift : ⊦ (_∃ rrR * hR)[rs, f, g] ↔ (∃ r0, r1. (rrR(r0, r1) * hR)[rs, f, g]);
ex3-shift-01 : ⊦ (_∃ oaR * hR)[rs, f, g] ↔ (∃ o, a. (oaR(o, a) * hR)[rs, f, g]);
in-uni : ⊦ rs0 ∩ rs1 = ∅ → (r ∈ mk(rs0, f, g) ∪ mk(rs1, f0, g0) ↔ r ∈ rs0 ∨ r ∈ rs1);
map-del : ⊦ (r ==>(o, a) * hR)[rs, f, g] ↔ hR[rs -- r, f, g] ∧ r ∈ rs ∧ f(r) = o ∧ g(r) = a;
map-in : ⊦ (r ==>(o, a) * hR)[rs, f, g] → r ∈ rs;
map-in0 : ⊦ r ==>(o, a)[rs, f, g] → r ∈ rs;
map-put : ⊦ (r ==>_ * hR)[rs, f, g] ↔ (r ==>(o1, a1) * hR)[rs, f(r; o1), g(r; a1)] ∧ r ∈ rs;
map-putrev : r ∈ rs ⊦ (r ==>(o0, a0) * hR)[rs, f(r; o1), g(r; a1)] ↔ (o0 = o1 ∧ a0 = a1) ∧ (r ==>_ * hR)[rs, f, g];
mapex-del : ⊦ (r ==>_ * hR)[rs, f, g] → hR[rs -- r, f, g];
mapex-elim : ⊦ (r ==>(o, a) * hR)[rs, f, g] → (r ==>_ * hR)[rs, f, g];
mapex-in : ⊦ (r ==>_ * hR)[rs, f, g] → r ∈ rs;
mapex-in0 : ⊦ r ==>_[rs, f, g] → r ∈ rs;
mapex-new : ¬ r ∈ rs, r ≠ null ⊦ hR[rs, f, g] ↔ (r ==>_ * hR)[rs ++ r, f, g];
mapex-put : r ∈ rs ⊦ (r ==>_ * hR)[rs, f(r; o), g(r; a)] ↔ (r ==>(o, a) * hR)[rs, f(r; o), g(r; a)];
mk-exists : ⊦ ∃ rs, f, g. ha = mk(rs, f, g);
mk-ext : ⊦ hR0 = hR1 ↔ (∀ rs, f, g. hR0[rs, f, g] ↔ hR1[rs, f, g]);
prop : ⊦ ⌜bv⌝ [rs, f, g] ↔ bv;
prop-emp : ⊦ ((⌜bv⌝ ∧ emp) * hR)[rs, f, g] ↔ bv ∧ hR[rs, f, g];
prop-false : ⊦ ¬ false[rs, f, g];
prop-sep : ⊦ ((⌜bv⌝ ∧ hR0) * hR1)[rs, f, g] ↔ bv ∧ (hR0 * hR1)[rs, f, g];
prop-true : ⊦ true[rs, f, g];
sep : ⊦ (hR0 * hR1)[rs, f, g] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ hR0[rs0, f, g] ∧ hR1[rs1, f, g]);
split-uni : ⊦ hR0[rs0, f, g] ∧ hR1[rs1, f, g] ∧ rs0 ∩ rs1 = ∅ → (hR0 * hR1)[rs0 ∪ rs1, f, g];
true-elim : ⊦ (hR0 * hR)[rs, f, g] → (true * hR)[rs, f, g];
true-emp : ⊦ hR[rs, f, g] → (true * hR)[rs, f, g];
uni : ⊦ rs0 ∩ rs1 = ∅ → mk(rs0 ∪ rs1, f, g) = mk(rs0, f, g) ∪ mk(rs1, f, g);
write : ⊦ r ∈ rs → mk(rs, f(r; o), g(r; a)) = mk(rs, f, g)[r, o, a];
ex1 : ⊦ (_∃ rR)(ha) ↔ (∃ r. rR(r)(ha));
ex2 : ⊦ (_∃ rrR)(ha) ↔ (∃ r0, r1. rrR(r0, r1)(ha));
maplet : ⊦ r ==>(o, a)(ha) ↔ ha = (∅ ++ r)[r, o, a] ∧ r ≠ null;
mapex : ⊦ r ==>_ = _∃(λ o, a. r ==>(o, a));
ex3-03 : ⊦ (_∃ oaR)(ha) ↔ (∃ o, a. oaR(o, a)(ha));
mapornull : ⊦ r ==>? = (r = null ⊃ emp;r ==>_);
at-eq : ⊦ ((r ==>(o0, a0) * hR))(ha) → (ha[r]o = o1 ∧ ha[r]a = a1 ↔ o0 = o1 ∧ a0 = a1);
at-rw-M01 : ⊦ ((r ==>(o0, a0) * hR))(ha) → ha[r]o = o0;
used for: s;
at-rw-M02 : ⊦ ((r ==>(o0, a0) * hR))(ha) → ha[r]a = a0;
used for: s;
eq-objs-M01 : ⊦ ((r ==>(o0, a0) * hR0))(ha) ∧ ((r ==>(o1, a1) * hR1))(ha) → o0 = o1;
eq-objs-M02 : ⊦ ((r ==>(o0, a0) * hR0))(ha) ∧ ((r ==>(o1, a1) * hR1))(ha) → a0 = a1;
ex1-shift-01 : ⊦ ((_∃ rR * hR))(ha) ↔ (∃ r. ((rR(r) * hR))(ha));
ex1-shiftw : ⊦ ((_∃ rR -* hR))(ha) ↔ (∀ r. ((rR(r) -* hR))(ha));
ex1-shiftw-inst : ⊦ (((_∃ rR -* hR) * hR0))(ha) ↔ (((_∃ rR -* hR) * hR0))(ha) ∧ (((rR(r) -* hR) * hR0))(ha);
ex2-shift-01 : ⊦ ((_∃ rrR * hR))(ha) ↔ (∃ r0, r1. ((rrR(r0, r1) * hR))(ha));
ex2-shiftw : ⊦ ((_∃ rrR -* hR))(ha) ↔ (∀ r0, r1. ((rrR(r0, r1) -* hR))(ha));
ex2-shiftw-inst : ⊦ (((_∃ rrR -* hR) * hR0))(ha) ↔ (((_∃ rrR -* hR) * hR0))(ha) ∧ (((rrR(r0, r1) -* hR) * hR0))(ha);
ex3-shift : ⊦ ((_∃ oaR * hR))(ha) ↔ (∃ o, a. ((oaR(o, a) * hR))(ha));
used for: s;
ex3-shiftw : ⊦ ((_∃ oaR -* hR))(ha) ↔ (∀ o, a. ((oaR(o, a) -* hR))(ha));
ex3-shiftw-inst : ⊦ (((_∃ oaR -* hR) * hR0))(ha) ↔ (((_∃ oaR -* hR) * hR0))(ha) ∧ (((oaR(o, a) -* hR) * hR0))(ha);
map-del-01 : ⊦ ((r ==>(o, a) * hR))(ha) ↔ hR(ha -- r) ∧ r ∈ ha ∧ ha[r]o = o ∧ ha[r]a = a;
map-in-01 : ⊦ ((r ==>(o, a) * hR))(ha) → r ∈ ha;
map-in0-02 : ⊦ r ==>(o, a)(ha) → r ∈ ha;
map-null : ⊦ null ==>(o, a) = ⌜false⌝ ;
map-put-01 : ⊦ ((r ==>_ * hR))(ha) ↔ ((r ==>(o1, a1) * hR))(ha[r, o1, a1]) ∧ r ∈ ha;
map-put-rw : r ∈ ha ⊦ ((r ==>(o, a) * hR))(ha) → (((r ==>(o0, a0) * hR))(ha[r, o1, a1]) ↔ o0 = o1 ∧ a0 = a1);
map-putex : r ∈ ha ⊦ ((r ==>(o0, a0) * hR))(ha[r, o1, a1]) ↔ (o0 = o1 ∧ a0 = a1) ∧ ((r ==>_ * hR))(ha);
map-same : ⊦ r ==>(o0, a0) * r ==>(o1, a1) = false;
map-write-M01 : r ∈ ha ⊦ ((r ==>(o0, a0) * hR))(ha[r, o1, a1]) → o0 = o1;
map-write-M02 : r ∈ ha ⊦ ((r ==>(o0, a0) * hR))(ha[r, o1, a1]) → a0 = a1;
mapex-and : ⊦ (r ==>_ ∧ r ==>(o, a)) = r ==>(o, a);
mapex-del-01 : ⊦ ((r ==>_ * hR))(ha) → hR(ha -- r);
mapex-elim-01 : ⊦ ((r ==>(o, a) * hR))(ha) → ((r ==>_ * hR))(ha);
mapex-in-01 : ⊦ ((r ==>_ * hR))(ha) → r ∈ ha;
mapex-new-01 : ¬ r ∈ ha, r ≠ null ⊦ hR(ha) ↔ ((r ==>_ * hR))(ha ++ r);
mapex-new-rw : ¬ r ∈ ha, r ≠ null ⊦ ((r ==>_ * hR))(ha ++ r) ↔ hR(ha);
mapex-null : ⊦ null ==>_ = ⌜false⌝ ;
mapex-put-01 : r ∈ ha ⊦ ((r ==>_ * hR))(ha[r, o, a]) ↔ ((r ==>(o, a) * hR))(ha[r, o, a]);
mapex-put-rw : r ∈ ha ⊦ ((r ==>_ * hR))(ha) → (((r ==>(o0, a0) * hR))(ha[r, o1, a1]) ↔ o0 = o1 ∧ a0 = a1);
maplet-singleton-heap : ⊦ r ==>(o, a)(ha) ↔ r ≠ null ∧ ha = (∅ ++ r)[r, o, a];
mapornull-emp : ⊦ null ==>? = emp;
mapornull-ex : ⊦ r ≠ null → r ==>? = r ==>_;
precise-map : ⊦ precise(r ==>(o, a));
precise-mapex : ⊦ precise(r ==>_);
precise-mapornull : ⊦ precise(r ==>?);
end enrich