This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| eqkeys | ⊦ eqkeys(st, st0) ↔ (∀ rk. rk ∈ st ↔ rk ∈ st0) | An Axiom |
| reftypep | ⊦ reftypep(val, st) ↔ is_referencevalue(val) ∧ (val .refval = jvmref ∨ val .refval ∈ st) | An Axiom |
| classOf | ⊦ classof(r, class1, st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ st[r -- _type] = typeval(mkclasstype(class1)) | An Axiom |
| typeOf | ⊦ typeof(r, ty, st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ st[r -- _type] = typeval(ty) | An Axiom |
| exception | ⊦ exception(class1, st) ↔ is_throw_mode(st[_mode]) ∧ st[_mode] .type = mkclasstype(class1) | An Axiom |
| equalXmode | ⊦ st =mode st0 ↔ st = st0 ∨ (∃ r, class1. st = (st0[r -- _type, typeval(mkclasstype(class1))][_mode, throw(r, mkclasstype(class1))]) ∧ newref(r, st0)) | An Axiom |
| eqexmode | ⊦ eqexmode(st, st0, r) ↔ st -- r =mode st0 -- r | An Axiom |
| eqex | ⊦ eqex(st, st0, r) ↔ st -- r = st0 -- r | An Axiom |
| lookup-xtra | ⊦ ∅[rk] = noval | An Axiom |
| init-def | ⊦ init(class1, st) = st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', initval(done)] | An Axiom |
| eqobj | ⊦ eqobj(r, st, st0) ↔ (∀ sk. (r -- sk ∈ st ↔ r -- sk ∈ st0) ∧ st[r -- sk] = st0[r -- sk]) | An Axiom |
| eqobjid | ⊦ eqobjid(r, st, st0) ↔ (∀ sk. r -- sk ∈ st ↔ r -- sk ∈ st0) ∧ (r -- _type ∈ st → st[r -- _type] = st0[r -- _type]) ∧ (r -- _length ∈ st → st[r -- _length] = st0[r -- _length]) | An Axiom |
| onlyModified | ⊦ onlyModified(r, st1, st2) ↔ (∀ rk. rk ∈ st1 ↔ rk ∈ st2) ∧ (∀ r0, sk. r0 ≠ r → st1[r0 -- sk] = st2[r0 -- sk]) ∧ (r -- _type ∈ st1 → st1[r -- _type] = st2[r -- _type]) ∧ (r -- _length ∈ st1 → st1[r -- _length] = st2[r -- _length]) | An Axiom |
| noiniterror | ⊦ noiniterror(claset, st) ↔ (∀ class. class ∈ claset → ¬ initerror(class, st)) | An Axiom |
| uninit | ⊦ uninit(claset, st) ↔ (∀ class. class ∈ claset → initundone(class, st)) | An Axiom |
| init | ⊦ init(claset, st) ↔ (∀ class. class ∈ claset → initdone(class, st)) | An Axiom |
| union-rec | ⊦ st ∪ st0[rk, val] = (st ∪ st0)[rk, val] | An Axiom |
| union-empty | ⊦ st ∪ ∅ = st | An Axiom |
| refs-def | ⊦ r ∈ st .refs ↔ r ∈ st | An Axiom |
| has_type | ⊦ has_type(r, st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) | An Axiom |
| initerror | ⊦ initerror(claset, st) ↔ (∀ class. class ∈ claset → initerror(class, st)) | An Axiom |
| nouninit | ⊦ nouninit(claset, st) ↔ (∀ class. class ∈ claset → ¬ initundone(class, st)) | An Axiom |
| onlyModifiedSet-def | ⊦ onlyModified(refs, st1, st2) ↔ (∀ r. r ∈ refs → onlyModified(r, st1, st2)) | An Axiom |
| initdone-def | ⊦ initdone(classes, st) ↔ (∀ class. class ∈ classes → initdone(class, st)) | An Axiom |
| classof | ⊦ classof(r, class1, st[r -- _type, val]) ↔ val = typeval(mkclasstype(class1)) ∧ r ≠ jvmref | A User Theorem |
| classof-01 | sk ≠ _type ⊦ classof(r, class1, st[r0 -- sk, val]) ↔ classof(r, class1, st) | A User Theorem |
| classof-02 | ⊦ classof(r, class1, st) → r ∈ st | A User Theorem |
| classof-03 | ⊦ classof(r, class1, st) → (st[r -- _type] .type ≠ mkclasstype(class1) ↔ false) | A User Theorem |
| classof-04 | ⊦ classof(r, class1, st[_out, val]) ↔ classof(r, class1, st) | A User Theorem |
| classof-05 | ⊦ classof(r, class1, st[_mode, val]) ↔ classof(r, class1, st) | A User Theorem |
| classof-06 | ⊦ classof(r, class1, st) → r ≠ jvmref | A User Theorem |
| classof-07 | ⊦ r ≠ r0 → (classof(r, class1, st[r0 -- sk, val]) ↔ classof(r, class1, st)) | A User Theorem |
| eq-mod | ⊦ st0 =mode st ∧ exception(class1, st0) ∧ initdone(class0, st) → initdone(class0, st0) | A User Theorem |
| eqex-at | ⊦ eqex(st, st0, r) ∧ rk .ref ≠ r → (st[rk] ≠ st0[rk] ↔ false) | A User Theorem |
| eqex-mode | r ≠ jvmref ⊦ st[_mode] ≠ noval ∧ eqex(st, st0, r) → st0[_mode] ≠ noval | A User Theorem |
| eqex-ref | ⊦ eqex(st, st, r) | A User Theorem |
| eqex-sym | ⊦ eqex(st, st0, r) → eqex(st0, st, r) | A User Theorem |
| eqex-tput | ⊦ eqex(st, st0, r) ∧ eqex(st0[rk, val], st1, r) → eqex(st[rk, val], st1, r) | A User Theorem |
| eqex-trans | ⊦ eqex(st, st0, r) ∧ eqex(st0, st1, r) → eqex(st, st1, r) | A User Theorem |
| eqmode | ⊦ st =mode st | A User Theorem |
| eqmode-01 | ⊦ newref(r, st) → (st[r -- _type, typeval(mkclasstype(class1))][_mode, throw(r, mkclasstype(class1))]) =mode st | A User Theorem |
| eqmode-length | ⊦ st =mode st0 ∧ r ∈ st0 → ¬ st0[r -- _length] .intval < st[r -- _length] .intval | A User Theorem |
| exception-01 | ⊦ exception(class1, st[_mode, throw(r, mkclasstype(class1))]) | A User Theorem |
| exception-02 | ⊦ exception(class, st) → st[_mode] ≠ noval | A User Theorem |
| exception-03 | ⊦ exception(class, st[_mode, throw(r, ty)]) ↔ ty = mkclasstype(class) | A User Theorem |
| init-one | ⊦ init(∅ ++ class, st) ↔ initdone(class, st) | A User Theorem |
| init-set | ⊦ init(claset, st) → init(claset, st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(done)]) | A User Theorem |
| initdone-empty | ⊦ initdone([], st) | A User Theorem |
| initdone-one | ⊦ initdone(class ', st) ↔ initdone(class, st) | A User Theorem |
| initdone-rec | ⊦ initdone(class ' + classes, st) ↔ initdone(class, st) ∧ initdone(classes, st) | A User Theorem |
| initerror-one | ⊦ initerror(∅ ++ class, st) ↔ initerror(class, st) | A User Theorem |
| instore-inrefs | ⊦ r ∈ st ↔ r ∈ st .refs | A User Theorem |
| instore-inrefs-01 | ⊦ ¬ r ∈ st .refs → ¬ r ∈ st | A User Theorem |
| instore-inrefs-02 | ⊦ ¬ r ∈ st → ¬ r ∈ st .refs | A User Theorem |
| mode-notin | ⊦ ¬ jvmref ∈ st .refs → ¬ _mode ∈ st | A User Theorem |
| mode-notin-01 | ⊦ ¬ jvmref ∈ st .refs → (st ∪ st0)[_mode] = st0[_mode] | A User Theorem |
| mode-notin-02 | ⊦ ¬ jvmref ∈ st → (st ∪ st0)[_mode] = st0[_mode] | A User Theorem |
| newref-same | ⊦ st .refs = st0 .refs → newref(st) = newref(st0) | A User Theorem |
| nouninit-empty | ⊦ nouninit(∅, st) | A User Theorem |
| nouninit-mode | ⊦ nouninit(claset, st[_mode, noval]) ↔ nouninit(claset, st) | A User Theorem |
| nouninit-mode-01 | ⊦ nouninit(claset, st[_mode, val]) ↔ nouninit(claset, st) | A User Theorem |
| nouninit-put | ⊦ nouninit(claset, st) → nouninit(claset, st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(done)]) | A User Theorem |
| nouninit-put-01 | ⊦ nouninit(claset, st) → nouninit(claset, st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)]) | A User Theorem |
| nouninit-put-02 | ⊦ r ≠ jvmref → (nouninit(claset, st[r -- sk, val]) ↔ nouninit(claset, st)) | A User Theorem |
| nouninit-put-03 | ⊦ ty ≠ void_type → (nouninit(claset, st[r -- mkfs(class, ty, fieldvar) ', val]) ↔ nouninit(claset, st)) | A User Theorem |
| nouninit-put-statfield | ⊦ ty ≠ void_type → (nouninit(claset, st[jvmref -- mkfs(class, ty, fieldvar) ', val]) ↔ nouninit(claset, st)) | A User Theorem |
| nouninit-undone | ⊦ nouninit(claset, st) ∧ initundone(class, st) → ¬ class ∈ claset | A User Theorem |
| onlymod-del | ⊦ onlyModified(r, st, st0) ∧ rk ∈ st → onlyModified(r, st -- rk, st0 -- rk) | A User Theorem |
| onlymod-in | ⊦ ¬ rk ∈ st ∧ onlyModified(r, st, st0) → ¬ rk ∈ st0 | A User Theorem |
| onlymod-in-01 | ⊦ rk ∈ st ∧ onlyModified(r, st, st0) → rk ∈ st0 | A User Theorem |
| onlymod-init | ⊦ ¬ initdone(class, st0) ∧ onlyModified(r, st, st0) ∧ r ≠ jvmref → ¬ initdone(class, st) | A User Theorem |
| onlymod-init-01 | ⊦ ¬ initundone(class, st0) ∧ onlyModified(r, st, st0) ∧ r ≠ jvmref → ¬ initundone(class, st) | A User Theorem |
| onlymod-init-02 | ⊦ ¬ initerror(class, st0) ∧ onlyModified(r, st, st0) ∧ r ≠ jvmref → ¬ initerror(class, st) | A User Theorem |
| onlymod-length | ⊦ onlyModified(r, st, st0) → st[r0 -- _length] = st0[r0 -- _length] | A User Theorem |
| onlymod-length-01 | ⊦ st[r0 -- _length] .intval ≠ i ∧ onlyModified(r, st, st0) → st0[r0 -- _length] .intval ≠ i | A User Theorem |
| onlymod-mode | ⊦ r ≠ jvmref ∧ onlyModified(r, st, st0) ∧ st[_mode] = noval → (st0[_mode] ≠ noval ↔ false) | A User Theorem |
| onlymod-mode-01 | ⊦ r ≠ jvmref ∧ onlyModified(r, st, st0) ∧ st[_mode] = noval → st0[_mode] = noval | A User Theorem |
| onlymod-other | ⊦ r ≠ r0 ∧ onlyModified(r, st, st0) → st[r0 -- sk] = st0[r0 -- sk] | A User Theorem |
| onlymod-put | ⊦ sk ≠ _type ∧ sk ≠ _length ∧ onlyModified(r, st, st0) ∧ r -- sk ∈ st → onlyModified(r, st, st0[r -- sk, val]) | A User Theorem |
| onlymod-put-01 | ⊦ sk ≠ _type ∧ sk ≠ _length ∧ r -- sk ∈ st0 → (onlyModified(r, st, st0[r -- sk, val]) ↔ onlyModified(r, st, st0)) | A User Theorem |
| onlymod-same | ⊦ onlyModified(r, st, st) | A User Theorem |
| onlymod-shift | ⊦ rk ∈ st → ( onlyModified(r, st[rk, val], st1) ↔ onlyModified(r, st, st1[rk, st[rk]]) ∧ rk ∈ st1 ∧ (r ≠ rk .ref ∨ rk = r -- _length ∨ rk = r -- _type → st1[rk] = val)) | A User Theorem |
| onlymod-sym | ⊦ onlyModified(r, st, st0) ↔ onlyModified(r, st0, st) | A User Theorem |
| onlymod-sym-01 | ⊦ ¬ onlyModified(r, st, st0) → ¬ onlyModified(r, st0, st) | A User Theorem |
| onlymod-type | ⊦ st[r0 -- _type] ≠ val ∧ onlyModified(r, st, st0) → st0[r0 -- _type] ≠ val | A User Theorem |
| refs-del | ⊦ (st -- r) .refs = st .refs -- r | A User Theorem |
| refs-empty | ⊦ ∅ .refs = ∅ | A User Theorem |
| refs-empty-01 | ⊦ st .refs = ∅ ↔ st = ∅ | A User Theorem |
| refs-equal | ⊦ # st .refs = # st0 .refs ∧ st ⊆ st0 ∧ r ∈ st0 → r ∈ st | A User Theorem |
| refs-equal-in | ⊦ r ∈ st ∧ st .refs = st0 .refs → r ∈ st0 | A User Theorem |
| refs-notin | ⊦ ¬ r ∈ st .refs → ¬ r -- sk ∈ st | A User Theorem |
| refs-put | ⊦ st[rk, val] .refs = st .refs ++ rk .ref | A User Theorem |
| reftype-01 | ⊦ reftypep(val, st) → refval(val .refval) = val | A User Theorem |
| reftype-02 | ⊦ r ∈ st → reftypep(refval(r), st) | A User Theorem |
| reftype-03 | ⊦ r ≠ r0 → (reftypep(refval(r), st[r0 -- sk, val0]) ↔ reftypep(refval(r), st)) | A User Theorem |
| reftype-04 | ⊦ val .refval ≠ r → (reftypep(val, st[r -- sk, val]) ↔ reftypep(val, st)) | A User Theorem |
| reftype-int | ⊦ r ∈ st → (reftypep(val, st[r -- i ', val0]) ↔ reftypep(val, st)) | A User Theorem |
| reftype-int-01 | r ≠ r0 ⊦ reftypep(refval(r0), st[r -- i ', val0]) ↔ reftypep(refval(r0), st) | A User Theorem |
| reftype-int-02 | ⊦ r0 ∈ st → (reftypep(refval(r0), st[r -- i ', val0]) ↔ reftypep(refval(r0), st)) | A User Theorem |
| reftype-jvmref | ⊦ reftypep(refval(jvmref), st) | A User Theorem |
| reftype-mode | ⊦ reftypep(val, st[_mode, val0]) ↔ reftypep(val, st) | A User Theorem |
| reftype-out | ⊦ reftypep(val, st[_out, val0]) ↔ reftypep(val, st) | A User Theorem |
| reftype-put | ⊦ r ∈ st → (reftypep(val, st[r -- sk, val0]) ↔ reftypep(val, st)) | A User Theorem |
| subset-is-union | ⊦ st ⊆ st1 ↔ (∃ st0. st1 = st0 ∪ st ∧ st .keys ∩ st0 .keys = ∅) | A User Theorem |
| subset-size | ⊦ # st0 .refs < # st .refs → ¬ st ⊆ st0 | A User Theorem |
| uninit-empty | ⊦ uninit(∅, st) | A User Theorem |
| uninit-one | ⊦ uninit(∅ ++ class, st) ↔ initundone(class, st) | A User Theorem |
| uninit-rec | ⊦ uninit(claset ++ class, st) ↔ uninit(claset, st) ∧ initundone(class, st) | A User Theorem |
| uninit-uninit | ⊦ uninit(st) → uninit(claset, st) | A User Theorem |
| union-at-left | ⊦ ¬ rk ∈ st0 → (st ∪ st0)[rk] = st[rk] | A User Theorem |
| union-at-right | ⊦ rk ∈ st0 .keys → (st ∪ st0)[rk] = st0[rk] | A User Theorem |
| union-at-right-01 | ⊦ rk ∈ st0 → (st ∪ st0)[rk] = st0[rk] | A User Theorem |
| union-at-right-02 | ⊦ ¬ rk ∈ st → (st ∪ st0)[rk] = st0[rk] | A User Theorem |
| union-at-right-03 | ⊦ ¬ r ∈ st .refs → (st ∪ st0)[r -- sk] = st0[r -- sk] | A User Theorem |
| union-def | ⊦ rk × val ∈ st ∪ st0 ↔ rk × val ∈ st0 ∨ ¬ rk ∈ st0 ∧ rk × val ∈ st | A User Theorem |
| union-empty-01 | ⊦ ∅ ∪ st = st | A User Theorem |
| union-in | ⊦ rk ∈ st ∪ st0 ↔ rk ∈ st ∨ rk ∈ st0 | A User Theorem |
| union-in-01 | ⊦ r ∈ st ∪ st0 ↔ r ∈ st ∨ r ∈ st0 | A User Theorem |
| union-in-02 | ⊦ ¬ r ∈ st .refs → (r -- sk ∈ st ∪ st0 ↔ r -- sk ∈ st0) | A User Theorem |
| union-init | ⊦ ¬ jvmref ∈ st → (initdone(class, st ∪ st0) ↔ initdone(class, st0)) | A User Theorem |
| union-init-01 | ⊦ ¬ jvmref ∈ st → (initundone(class, st ∪ st0) ↔ initundone(class, st0)) | A User Theorem |
| union-init-02 | ⊦ init(st) ∧ ¬ jvmref ∈ st1 → (¬ init(st1 ∪ st) ↔ false) | A User Theorem |
| union-init-03 | ⊦ ¬ jvmref ∈ st → (init(str, st ∪ st0) ↔ init(str, st0)) | A User Theorem |
| union-keys | ⊦ (st ∪ st0) .keys = st .keys ∪ st0 .keys | A User Theorem |
| union-newref | ⊦ ¬ r ∈ st .refs → (newref(r, st ∪ st0) ↔ newref(r, st0)) | A User Theorem |
| union-newref-01 | ⊦ ¬ r ∈ st → (newref(r, st ∪ st0) ↔ newref(r, st0)) | A User Theorem |
| union-newref-02 | ⊦ newref(r, st ∪ st0) ↔ newref(r, st) ∧ newref(r, st0) | A User Theorem |
| union-rec-rew | ⊦ (st ∪ st0)[rk, val] = st ∪ st0[rk, val] | A User Theorem |
| union-refs | ⊦ (st ∪ st0) .refs = st .refs ∪ st0 .refs | A User Theorem |
| union-subset | ⊦ st0 ⊆ st ∪ st0 | A User Theorem |
| union-subset-left | ⊦ st .refs ∩ st0 .refs = ∅ → st ⊆ st ∪ st0 | A User Theorem |