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: |
|---|---|---|
| addclass-no2 | ⊦ addclass(class1, (i ' × val) ' + fis, st) = addclass(class1, fis, st) | An Axiom |
| addclass-no1 | ⊦ class1 ≠ class2 → addclass(class1, (mkfs(class2, ty, fieldvar) ' × val) ' + fis, st) = addclass(class1, fis, st) | An Axiom |
| addclass-yes | ⊦ addclass(class1, (mkfs(class1, ty, fieldvar) ' × val) ' + fis, st) = (addclass(class1, fis, st)[jvmref -- mkfs(class1, ty, fieldvar) ', val]) | An Axiom |
| addclass-base | ⊦ addclass(class1, [], st) = st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', initval(done)] | An Axiom |
| addobj-rec | ⊦ addobj(r, class1, (sk × val) ' + fis, st) = (addobj(r, class1, fis, st)[r -- sk, val]) | An Axiom |
| addobj-base | ⊦ addobj(r, class1, [], st) = st[r -- _type, typeval(mkclasstype(class1))] | An Axiom |
| is_obj | ⊦ is_obj(r, class1, sks, st) ↔ r ≠ jvmref ∧ (r -- _type) × typeval(mkclasstype(class1)) ∈ st ∧ goodfieldsandtypes(r, sks, st) | An Axiom |
| is_obj_exact | ⊦ is_obj_exact(r, class1, sks, st) ↔ r ≠ jvmref ∧ (r -- _type) × typeval(mkclasstype(class1)) ∈ st ∧ exactfieldsandtypes(r, sks, st) | An Axiom |
| instfields-predef | ⊦ is_predefined_class(class) → instfields(class) = [] | An Axiom |
| statfields-predef | ⊦ is_predefined_class(class) → statfields(class) = [] | An Axiom |
| is_obj-def | ⊦ is_obj(r, class, st) ↔ r ≠ jvmref ∧ (r -- _type) × typeval(mkclasstype(class)) ∈ st ∧ goodfieldsandtypes(r, instfields(class), st) | An Axiom |
| addobj-keysrec | ⊦ addobj(r, class, sk ' + sks, st) = (addobj(r, class, sks, st)[r -- sk, initial_value(sk .fs .type)]) | An Axiom |
| addobj-keysempty | ⊦ addobj(r, class, [], st) = st[r -- _type, typeval(mkclasstype(class))] | An Axiom |
| addobj-simple | ⊦ addobj(r, class, st) = addobj(r, class, instfields(class), st) | An Axiom |
| is-valid-ref | ⊦ is_valid_ref(r, st) ↔ is_obj(r, st) ∨ is_array(r, st) | An Axiom |
| is-any-object | ⊦ is_obj(r, st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ is_classtype(st[r -- _type] .type) ∧ is_obj(r, st[r -- _type] .type .class, st) | An Axiom |
| instfields-special | ⊦ ¬ mkfs(class0, void_type, fieldvar) ' ∈ instfields(class) | An Axiom |
| statfields-special | ⊦ ¬ mkfs(class0, void_type, fieldvar) ' ∈ statfields(class) | An Axiom |
| instfields-subclass | ⊦ fs ' ∈ instfields(class) ∧ class0 ≤ class → fs ' ∈ instfields(class0) | An Axiom |
| has_reffield-array | ⊦ is_array(r, st) → (has_reffield(r, st) ↔ st[r -- _length] .intval > 0 ∧ (is_reftype(st[r -- _type] .type .type) ∨ st[r -- _type] .type .type = void_type)) | An Axiom |
| has_reffield-class | ⊦ is_obj(r, st) → (has_reffield(r, st) ↔ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_reftype(fs .type))) | An Axiom |
| has_reffield-no | ⊦ ¬ is_valid_ref(r, st) → ¬ has_reffield(r, st) | An Axiom |
| instfields-abstract | ⊦ ¬ mkfs(class0, abstract_type, fieldvar) ' ∈ instfields(class) | An Axiom |
| statfields-abstract | ⊦ ¬ mkfs(class0, abstract_type, fieldvar) ' ∈ statfields(class) | An Axiom |
| validfieldinits-all | ⊦ validfieldinits(fis, st) ↔ (∀ sk, val. sk × val ∈ fis → is_fskey(sk) ∧ oktype(val, sk .fs .type, st) ∧ ( is_referencevalue(val) → val .refval = jvmref ∨ val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ st[val .refval -- _type] .type ≤ sk .fs .type)) | An Axiom |
| okfieldinits-rec | ⊦ okfieldinits(class, (sk × val) ' + fis) ↔ is_fskey(sk) ∧ val = initial_value(sk .fs .type) ∧ sk .fs .class = class ∧ sk .fs .type ≠ abstract_type ∧ okfieldinits(class, fis) | An Axiom |
| okfieldinits-empty | ⊦ okfieldinits(class, []) | An Axiom |
| okstatfields-def | ⊦ okstatfields(class, st) ↔ goodfieldsandtypes(jvmref, statfields(class), st) | An Axiom |
| instfields-index | ⊦ ¬ i ' ∈ instfields(class) | An Axiom |
| statfields-index | ⊦ ¬ i ' ∈ statfields(class) | An Axiom |
| statfields-same-class | ⊦ mkfs(class0, ty, fieldvar) ' ∈ statfields(class) → class = class0 | An Axiom |
| is-valid-ref-stronger-def | ⊦ is_valid_ref(str, r, st) ↔ is_obj(str, r, st) ∨ is_array(str, r, st) | An Axiom |
| is-real-object-def | ⊦ is_obj(str, r, st) ↔ class+∃(str, st[r -- _type] .type .class) ∧ ¬ is_abstract(st[r -- _type] .type .class) ∧ is_obj(r, st) | An Axiom |
| instfields-typeex | ⊦ mkfs(class0, ty, fieldvar) ' ∈ instfields(class) ∧ tdname+∃(str, class) → type∃(str, ty) | An Axiom |
| statfields-typeex | ⊦ mkfs(class0, ty, fieldvar) ' ∈ statfields(class0) ∧ tdname+∃(str, class0) → type∃(str, ty) | An Axiom |
| instfields-nodups | ⊦ ¬ dups(instfields(class)) | An Axiom |
| statfields-nodups | ⊦ ¬ dups(statfields(class)) | An Axiom |
| ac-bad | class1 ≠ class2 ⊦ addclass(class1, fis + (mkfs(class2, ty, fieldvar) ' × val) ' + fis0, st) = addclass(class1, fis + fis0, st) | A User Theorem |
| ac-bad-01 | class1 ≠ class2 ⊦ addclass(class1, fis + (mkfs(class2, ty, fieldvar) ' × val) ', st) = addclass(class1, fis, st) | A User Theorem |
| ac-bad-02 | ⊦ addclass(class1, fis + (i ' × val) ' + fis0, st) = addclass(class1, fis + fis0, st) | A User Theorem |
| ac-bad-03 | ⊦ addclass(class1, fis + (i ' × val) ', st) = addclass(class1, fis, st) | A User Theorem |
| ac-class | ⊦ classof(r0, class0, addclass(class1, fis, st)) ↔ classof(r0, class0, st) | A User Theorem |
| ac-del | ⊦ (addclass(class1, fis + (sk × val0) ' + fis0, st)[jvmref -- sk, val]) = (addclass(class1, fis + fis0, st)[jvmref -- sk, val]) | A User Theorem |
| ac-del-01 | ⊦ (addclass(class1, fis + (sk × val0) ', st)[jvmref -- sk, val]) = (addclass(class1, fis, st)[jvmref -- sk, val]) | A User Theorem |
| ac-del-02 | ⊦ (addclass(class1, (sk × val0) ' + fis0, st)[jvmref -- sk, val]) = (addclass(class1, fis0, st)[jvmref -- sk, val]) | A User Theorem |
| ac-del-03 | ⊦ (addclass(class1, (sk × val0) ', st)[jvmref -- sk, val]) = (st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', initval(done)][jvmref -- sk, val]) | A User Theorem |
| ac-dups | ⊦ addclass(class1, fis + ((sk × val) + (sk × val0) + fis0), st) = addclass(class1, fis + ((sk × val) + fis0), st) | A User Theorem |
| ac-dups-01 | ⊦ addclass(class1, fis + ((sk × val) + (fis1 + ((sk × val0) + fis0))), st) = addclass(class1, fis + ((sk × val) + (fis1 + fis0)), st) | A User Theorem |
| ac-dups-02 | ⊦ addclass(class1, fis + (sk × val) ' + (sk × val0) ' + fis0, st) = addclass(class1, fis + (sk × val) ' + fis0, st) | A User Theorem |
| ac-dups-03 | ⊦ addclass(class1, fis + (sk × val) ' + fis1 + (sk × val0) ' + fis0, st) = addclass(class1, fis + (sk × val) ' + fis1 + fis0, st) | A User Theorem |
| ac-dups-04 | ⊦ addclass(class1, (sk × val) ' + (sk × val0) ', st) = addclass(class1, (sk × val) ', st) | A User Theorem |
| ac-dups-05 | ⊦ addclass(class1, (sk × val) ' + fis1 + (sk × val0) ', st) = addclass(class1, (sk × val) ' + fis1, st) | A User Theorem |
| ac-getbar | ⊦ r ≠ jvmref → getbytearray(r, addclass(class, fis, st)) = getbytearray(r, st) | A User Theorem |
| ac-in | ⊦ jvmref -- mkfs(class1, ty, fieldvar) ' ∈ addclass(class1, fis, st) ↔ ¬ ¬ ( mkfs(class1, ty, fieldvar) ' ∈ fis ∨ jvmref -- mkfs(class1, ty, fieldvar) ' ∈ st ∨ mkfs(class1, ty, fieldvar) = mkfs(class1, void_type, `initstate' .field)) | A User Theorem |
| ac-in-01 | class1 ≠ class2 ⊦ jvmref -- mkfs(class2, ty, fieldvar) ' ∈ addclass(class1, fis, st) ↔ jvmref -- mkfs(class2, ty, fieldvar) ' ∈ st | A User Theorem |
| ac-in-02 | ⊦ r -- i ' ∈ addclass(class1, fis, st) ↔ r -- i ' ∈ st | A User Theorem |
| ac-in-03 | ¬ _type ∈ fis ⊦ jvmref -- _type ∈ addclass(class1, fis, st) ↔ jvmref -- _type ∈ st | A User Theorem |
| ac-in-03-02 | r ≠ jvmref ⊦ r -- sk ∈ addclass(class1, fis, st) ↔ r -- sk ∈ st | A User Theorem |
| ac-in-04 | mkfs(class1, ty, fieldvar) ' ∈ fis ⊦ jvmref -- mkfs(class1, ty, fieldvar) ' ∈ addclass(class1, fis, st) | A User Theorem |
| ac-in-05 | mkfs(class1, ty, fieldvar) ' ∈ fis ⊦ (jvmref -- mkfs(class1, ty, fieldvar) ') × val ∈ addclass(class1, fis, st) ↔ fis[mkfs(class1, ty, fieldvar) '] = val | A User Theorem |
| ac-in-06 | class1 ≠ class2 ⊦ jvmref -- mkfs(class1, ty, fieldvar) ' ∈ addclass(class2, fis, st) ↔ jvmref -- mkfs(class1, ty, fieldvar) ' ∈ st | A User Theorem |
| ac-in-07 | class1 ≠ class2 ⊦ (jvmref -- mkfs(class1, ty, fieldvar) ') × val ∈ addclass(class2, fis, st) ↔ (jvmref -- mkfs(class1, ty, fieldvar) ') × val ∈ st | A User Theorem |
| ac-in-08 | ⊦ r ∈ st → r ∈ addclass(class1, fis, st) | A User Theorem |
| ac-in-09 | ⊦ r ≠ jvmref → (r ∈ addclass(class1, fis, st) ↔ r ∈ st) | A User Theorem |
| ac-in-10 | ⊦ ¬ sk ∈ fis ∧ sk ≠ mkfs(class, void_type, `initstate' .field) ' → (r -- sk ∈ addclass(class, fis, st) ↔ r -- sk ∈ st) | A User Theorem |
| ac-in-11 | ⊦ ¬ is_fskey(sk) → (r -- sk ∈ addclass(class, fis, st) ↔ r -- sk ∈ st) | A User Theorem |
| ac-init | ¬ mkfs(class1, void_type, `initstate' .field) ' ∈ fis ⊦ initdone(class1, addclass(class1, fis, st)) | A User Theorem |
| ac-init-01 | ¬ mkfs(class1, void_type, `initstate' .field) ' ∈ fis ⊦ ¬ initundone(class1, addclass(class1, fis, st)) | A User Theorem |
| ac-init-02 | ¬ mkfs(class1, void_type, `initstate' .field) ' ∈ fis ⊦ ¬ initerror(class1, addclass(class1, fis, st)) | A User Theorem |
| ac-init-03 | class1 ≠ class2, class2 ≠ `java.lang.Object' .class ⊦ initdone(class1, addclass(class2, fis, st)) ↔ initdone(class1, st) | A User Theorem |
| ac-init-04 | class1 ≠ class2, class2 ≠ `java.lang.Object' .class ⊦ initundone(class1, addclass(class2, fis, st)) ↔ initundone(class1, st) | A User Theorem |
| ac-init-05 | class1 ≠ class2 ⊦ initerror(class1, addclass(class2, fis, st)) ↔ initerror(class1, st) | A User Theorem |
| ac-init-06 | ¬ mkfs(class1, void_type, `initstate' .field) ' ∈ fis ⊦ initerror(class1, addclass(class1, fis + (mkfs(class1, void_type, `initstate' .field) ' × val) ' + fis0, st)) ↔ val = initval(error) | A User Theorem |
| ac-init-07 | ¬ mkfs(class1, void_type, `initstate' .field) ' ∈ fis ⊦ initundone(class1, addclass(class1, fis + (mkfs(class1, void_type, `initstate' .field) ' × val) ' + fis0, st)) ↔ val = initval(undone) | A User Theorem |
| ac-init-08 | ¬ mkfs(class1, void_type, `initstate' .field) ' ∈ fis ⊦ initdone(class1, addclass(class1, fis + (mkfs(class1, void_type, `initstate' .field) ' × val) ' + fis0, st)) ↔ val ≠ initval(error) ∧ val ≠ initval(undone) | A User Theorem |
| ac-init-09 | ¬ mkfs(class1, void_type, `initstate' .field) ' ∈ fis ⊦ initerror(class1, addclass(class1, fis + (mkfs(class1, void_type, `initstate' .field) ' × val) ', st)) ↔ val = initval(error) | A User Theorem |
| ac-init-10 | ¬ mkfs(class1, void_type, `initstate' .field) ' ∈ fis ⊦ initundone(class1, addclass(class1, fis + (mkfs(class1, void_type, `initstate' .field) ' × val) ', st)) ↔ val = initval(undone) | A User Theorem |
| ac-init-11 | ¬ mkfs(class1, void_type, `initstate' .field) ' ∈ fis ⊦ initdone(class1, addclass(class1, fis + (mkfs(class1, void_type, `initstate' .field) ' × val) ', st)) ↔ val ≠ initval(error) ∧ val ≠ initval(undone) | A User Theorem |
| ac-init-first | ⊦ class ∈ claset ∧ class ≠ `java.lang.Object' .class ∧ ¬ mkfs(class, void_type, `initstate' .field) ' ∈ fis → (init(claset, addclass(class, fis, st)) ↔ init(claset -- class, st)) | A User Theorem |
| ac-init-other | ⊦ ¬ class ∈ claset ∧ class ≠ `java.lang.Object' .class → (init(claset, addclass(class, fis, st)) ↔ init(claset, st)) | A User Theorem |
| ac-isarray | ⊦ is_arrayref(r, i, addclass(class1, fis, st)) ↔ is_arrayref(r, i, st) | A User Theorem |
| ac-lookup | mkfs(class1, ty, fieldvar) ' ∈ fis ⊦ (addclass(class1, fis, st)[jvmref -- mkfs(class1, ty, fieldvar) ']) = fis[mkfs(class1, ty, fieldvar) '] | A User Theorem |
| ac-lookup-01 | class1 ≠ class2 ⊦ (addclass(class2, [], st)[jvmref -- mkfs(class1, ty, fieldvar) ']) = st[jvmref -- mkfs(class1, ty, fieldvar) '] | A User Theorem |
| ac-lookup-02 | class1 ≠ class2 ⊦ (addclass(class2, fis, st)[jvmref -- mkfs(class1, ty, fieldvar) ']) = st[jvmref -- mkfs(class1, ty, fieldvar) '] | A User Theorem |
| ac-lookup-03 | ¬ mkfs(class1, void_type, `initstate' .field) ' ∈ fis ⊦ (addclass(class1, fis, st)[jvmref -- mkfs(class1, void_type, `initstate' .field) ']) = initval(done) | A User Theorem |
| ac-lookup-04 | r ≠ jvmref ⊦ (addclass(class1, fis, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| ac-lookup-05 | ⊦ ¬ is_fskey(sk) → (addclass(class, fis, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| ac-lookup-06 | ⊦ ¬ sk ∈ fis ∧ sk ≠ mkfs(class, void_type, `initstate' .field) ' → (addclass(class, fis, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| ac-mode | class1 ≠ `java.lang.Object' .class ⊦ (addclass(class1, fis, st)[_mode]) = st[_mode] | A User Theorem |
| ac-mode-01 | ⊦ ¬ _mode .key ∈ fis → (addclass(class, fis, st)[_mode]) = st[_mode] | A User Theorem |
| ac-new | ⊦ newref(r, addclass(class1, fis, st)) ↔ newref(r, st) | A User Theorem |
| ac-newrefs | ⊦ is_newref_list(refs, addclass(class1, fis, st)) ↔ is_newref_list(refs, st) | A User Theorem |
| ac-no1 | ⊦ is_fskey(fv .1) ∧ fv .1 .fs .class ≠ class → addclass(class, fv ' + fis, st) = addclass(class, fis, st) | A User Theorem |
| ac-no2 | ⊦ is_indexkey(fv .1) → addclass(class, fv ' + fis, st) = addclass(class, fis, st) | A User Theorem |
| ac-okarray | ⊦ r ≠ jvmref → (okarray(refval(r), ty, i, addclass(class1, fis, st)) ↔ okarray(refval(r), ty, i, st)) | A User Theorem |
| ac-okarray-01 | ⊦ val ≠ refval(jvmref) → (okarray(val, ty, i, addclass(class, fis, st)) ↔ okarray(val, ty, i, st)) | A User Theorem |
| ac-okarrays | ⊦ r ≠ jvmref → (okarrays(r, fis, addclass(class, fis0, st)) ↔ okarrays(r, fis, st)) | A User Theorem |
| ac-okclass | ⊦ okclass(refval(r0), class1, addclass(class0, fis, st)) ↔ okclass(refval(r0), class1, st) | A User Theorem |
| ac-okreftype | ⊦ val ≠ refval(jvmref) → (okreftype(val, ty, addclass(class1, fis, st)) ↔ okreftype(val, ty, st)) | A User Theorem |
| ac-oktype | ⊦ oktype(val, ty, addclass(class1, fis, st)) ↔ oktype(val, ty, st) | A User Theorem |
| ac-one1 | ⊦ addclass(class1, (mkfs(class1, ty, fieldvar) ' × val) ', st) = (st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', initval(done)][jvmref -- mkfs(class1, ty, fieldvar) ', val]) | A User Theorem |
| ac-one2 | class1 ≠ class2 ⊦ addclass(class1, (mkfs(class2, ty, fieldvar) ' × val) ', st) = st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', initval(done)] | A User Theorem |
| ac-one3 | ⊦ addclass(class1, (i ' × val) ', st) = st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', initval(done)] | A User Theorem |
| ac-out | class1 ≠ `java.lang.Object' .class ⊦ addclass(class1, fis, st[_out, val]) = (addclass(class1, fis, st)[_out, val]) | A User Theorem |
| ac-out-01 | class1 ≠ `java.lang.Object' .class ⊦ (addclass(class1, fis, st)[_out]) = st[_out] | A User Theorem |
| ac-refin | ⊦ rk ∈ st → rk ∈ addclass(class, fis, st) | A User Theorem |
| ac-refs | ⊦ addclass(class, fis, st) .refs = st .refs ++ jvmref | A User Theorem |
| ac-reftype | ⊦ reftypep(val, addclass(class1, fis, st)) ↔ reftypep(val, st) | A User Theorem |
| ac-shift | class2 ≠ class1 ⊦ (addclass(class1, fis, st)[jvmref -- mkfs(class2, ty, fieldvar) ', val]) = addclass(class1, fis, st[jvmref -- mkfs(class2, ty, fieldvar) ', val]) | A User Theorem |
| ac-shift-01 | ⊦ (addclass(class1, fis, st)[jvmref -- mkfs(class1, ty, fieldvar) ', val]) = addclass(class1, (mkfs(class1, ty, fieldvar) ' × val) + fis, st) | A User Theorem |
| ac-shift-02 | ⊦ (addclass(class1, fis, st)[jvmref -- mkfs(class1, ty, fieldvar) ', val]) = addclass(class1, fis[mkfs(class1, ty, fieldvar) ', val], st) | A User Theorem |
| ac-shift-03 | ⊦ (addclass(class, fis, st)[jvmref -- mkfs(class, ty, fieldvar) ', val]) = addclass(class, fis[mkfs(class, ty, fieldvar) ', val], st) | A User Theorem |
| ac-type | ⊦ ¬ _type ∈ fis → (addclass(class, fis, st)[r -- _type]) = st[r -- _type] | A User Theorem |
| ac-uninit | ⊦ class ≠ `java.lang.Object' .class → (_uninit ∈ addclass(class, fis, st) ↔ _uninit ∈ st) | A User Theorem |
| ac-uninitset | ⊦ ¬ class1 ∈ claset ∧ class1 ≠ `java.lang.Object' .class → (uninit(claset, addclass(class1, fis, st)) ↔ uninit(claset, st)) | A User Theorem |
| add-at | ⊦ r0 ∈ st ∧ newref(r, st) → (addobj(r, class1, fis, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| add-at-01 | ⊦ (addobj(r, class, [], st)[r0 -- i ']) = st[r0 -- i '] | A User Theorem |
| add-class | ⊦ r ≠ r0 → (classof(r0, class0, addobj(r, class1, fis, st)) ↔ classof(r0, class0, st)) | A User Theorem |
| add-classof | ¬ _type ∈ fis ⊦ r ≠ jvmref → classof(r, class1, addobj(r, class1, fis, st)) | A User Theorem |
| add-dupput | sk ∈ fis ⊦ addobj(r, class1, fis + (sk × val) ' + fis0, st) = addobj(r, class1, fis + fis0, st) | A User Theorem |
| add-field | ⊦ (addobj(r, class1, (sk × val) ' + fis, st)[r -- sk]) = val | A User Theorem |
| add-field-01 | ⊦ (addobj(r, class1, (sk × val) ', st)[r -- sk]) = val | A User Theorem |
| add-field-02 | ⊦ sk ≠ sk0 → (addobj(r, class1, (sk × val) ' + fis, st)[r -- sk0]) = (addobj(r, class1, fis, st)[r -- sk0]) | A User Theorem |
| add-field-03 | sk ≠ sk0, sk ≠ _type ⊦ (addobj(r, class1, (sk0 × val) ', st)[r -- sk]) = st[r -- sk] | A User Theorem |
| add-field-if | ⊦ (addobj(r, class1, (sk × val) ' + fis, st)[r -- sk0]) = ((sk = sk0 ⊃ val; addobj(r, class1, fis, st)[r -- sk0])) | A User Theorem |
| add-field-same | str ≠ str0 ⊦ (addobj(r, class, (mkfs(class0, ty0, ((* str)) .field) ' × val) ' + fis, st)[r -- mkfs(class1, ty1, ((* str0)) .field) ']) = (addobj(r, class, fis, st)[r -- mkfs(class1, ty1, str0 .field) ']) | A User Theorem |
| add-field-same-01 | ⊦ (addobj(r, class, (mkfs(class0, int_type, fieldvar0) ' × val) ' + fis, st)[r -- mkfs(class1, boolean_type, fieldvar1) ']) = (addobj(r, class, fis, st)[r -- mkfs(class1, boolean_type, fieldvar1) ']) | A User Theorem |
| add-field-same-02 | str ≠ str0 ⊦ (addobj(r, class, (mkfs(((* str)) .class, ty, fieldvar) ' × val) ' + fis, st)[r -- mkfs(((* str0)) .class, ty0, fieldvar0) ']) = (addobj(r, class, fis, st)[r -- mkfs(str0 .class, ty0, fieldvar0) ']) | A User Theorem |
| add-gins | ⊦ (addobj(r, class1, fis, st)[r -- sk, val]) = addobj(r, class1, fis[sk, val], st) | A User Theorem |
| add-gins-01 | sk0 ≠ sk ⊦ addobj(r, class1, ((sk0 × val0) ' + fis)[sk, val], st) = addobj(r, class1, (sk0 × val0) ' + fis[sk, val], st) | A User Theorem |
| add-goodfield | ⊦ r ≠ r0 → (goodfieldandtype(r, sk, addobj(r0, class, fis, st)) ↔ goodfieldandtype(r, sk, st)) | A User Theorem |
| add-gput | ⊦ (addobj(r, class1, fis, st)[r -- sk, val]) = addobj(r, class1, (sk × val) ' + fis, st) | A User Theorem |
| add-in | ⊦ r ∈ addobj(r, class1, fis, st) | A User Theorem |
| add-in-01 | ⊦ r ≠ r0 → (r ∈ addobj(r0, class1, fis, st) ↔ r ∈ st) | A User Theorem |
| add-in-02 | ⊦ r ∈ addobj(r0, class1, fis, st) ↔ r = r0 ∨ r ∈ st | A User Theorem |
| add-in-03 | ⊦ rk ∈ st → rk ∈ addobj(r, class1, fis, st) | A User Theorem |
| add-in-04 | ⊦ r ≠ r0 → (r -- sk ∈ addobj(r0, class1, fis, st) ↔ r -- sk ∈ st) | A User Theorem |
| add-in-05 | ⊦ sk ∈ fis → r -- sk ∈ addobj(r, class1, fis, st) | A User Theorem |
| add-in-06 | sk ∈ fis ⊦ r -- sk ∈ addobj(r, class1, fis, st) | A User Theorem |
| add-in-07 | ⊦ r ≠ r0 → ((r -- sk) × val ∈ addobj(r0, class1, fis, st) ↔ (r -- sk) × val ∈ st) | A User Theorem |
| add-in-08 | ⊦ r -- sk ∈ addobj(r, class, fis, st) ↔ ¬ ¬ (sk ∈ fis ∨ sk = _type ∨ r -- sk ∈ st) | A User Theorem |
| add-in-09 | ⊦ sk ∈ fis → (addobj(r, class, fis, st)[r -- sk]) = fis[sk] | A User Theorem |
| add-init | ⊦ initdone(class, addobj(r, class0, [], st)) ↔ initdone(class, st) | A User Theorem |
| add-init-newref | ⊦ initdone(class, addobj(newref(st), class0, fis, st)) ↔ initdone(class, st) | A User Theorem |
| add-init-newref-01 | ⊦ initundone(class, addobj(newref(st), class0, fis, st)) ↔ initundone(class, st) | A User Theorem |
| add-init-newref-02 | ⊦ initerror(class, addobj(newref(st), class0, fis, st)) ↔ initerror(class, st) | A User Theorem |
| add-initdone | ⊦ ¬ initdone(class, addobj(r, class0, [], st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)])) | A User Theorem |
| add-initdone-01 | ⊦ ¬ mkfs(class, void_type, `initstate' .field) ' ∈ fis → ¬ initdone(class, addobj(r, class0, fis, st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)])) | A User Theorem |
| add-initerror | ⊦ ¬ mkfs(class, void_type, `initstate' .field) ' ∈ fis → initerror(class, addobj(r, class0, fis, st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)])) | A User Theorem |
| add-initerror-01 | ⊦ initerror(class, addobj(r, class0, [], st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)])) | A User Theorem |
| add-initundone | ⊦ ¬ mkfs(class, void_type, `initstate' .field) ' ∈ fis → ¬ initundone(class, addobj(r, class0, fis, st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)])) | A User Theorem |
| add-initundone-01 | ⊦ ¬ initundone(class, addobj(r, class0, [], st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)])) | A User Theorem |
| add-isarray | ⊦ r ≠ r0 → (is_arrayref(r, i, addobj(r0, class1, fis, st)) ↔ is_arrayref(r, i, st)) | A User Theorem |
| add-length | ¬ _length ∈ fis ⊦ (addobj(r0, class, fis, st)[r -- _length]) = st[r -- _length] | A User Theorem |
| add-mode | ⊦ newref(r, st) → (addobj(r, class1, fis, st)[_mode]) = st[_mode] | A User Theorem |
| add-mode-01 | ⊦ r ≠ jvmref → (addobj(r, class1, fis, st)[_mode]) = st[_mode] | A User Theorem |
| add-mode-02 | ⊦ (addobj(newref(st), class, fis, st)[_mode]) = st[_mode] | A User Theorem |
| add-new | ⊦ newref(r0, addobj(r, class1, fis, st)) → r ≠ r0 | A User Theorem |
| add-new-01 | ⊦ r ≠ r0 → (newref(r0, addobj(r, class1, fis, st)) ↔ newref(r0, st)) | A User Theorem |
| add-notin | ⊦ ¬ sk ∈ fis ∧ sk ≠ _type → (addobj(r, class, fis, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| add-nput | ⊦ ¬ sk ∈ fis ∧ sk ≠ _type → (addobj(r, class1, fis, st)[r -- sk, val]) = addobj(r, class1, fis, st[r -- sk, val]) | A User Theorem |
| add-nput-01 | ⊦ ¬ sk ∈ fis → addobj(r, class1, fis + (sk × val) ' + fis0, st) = (addobj(r, class1, fis + fis0, st)[r -- sk, val]) | A User Theorem |
| add-nput-02 | ⊦ ¬ sk ∈ fis → addobj(r, class1, fis + (sk × val) ', st) = (addobj(r, class1, fis, st)[r -- sk, val]) | A User Theorem |
| add-okarray | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) ∧ r ≠ r0 → (okarray(refval(r), ty, i, addobj(r0, class1, fis, st)) ↔ okarray(refval(r), ty, i, st)) | A User Theorem |
| add-okarray-01 | ⊦ r ≠ r0 → (okarray(refval(r), byte_type, i, addobj(r0, class1, fis, st)) ↔ okarray(refval(r), byte_type, i, st)) | A User Theorem |
| add-okarray-02 | ⊦ r ≠ r0 → (okarray(refval(r), short_type, i, addobj(r0, class1, fis, st)) ↔ okarray(refval(r), short_type, i, st)) | A User Theorem |
| add-okarray-03 | ⊦ r ≠ r0 → (okarray(refval(r), int_type, i, addobj(r0, class1, fis, st)) ↔ okarray(refval(r), int_type, i, st)) | A User Theorem |
| add-okarray-04 | ⊦ r ≠ r0 → (okarray(refval(r), boolean_type, i, addobj(r0, class1, fis, st)) ↔ okarray(refval(r), boolean_type, i, st)) | A User Theorem |
| add-okarray-05 | ⊦ r ≠ r0 → (okarray(refval(r), ty, i, addobj(r0, class1, fis, st)) ↔ okarray(refval(r), ty, i, st)) | A User Theorem |
| add-okbar | ⊦ r ≠ r0 → (okbytearray(r, addobj(r0, class, fis, st)) ↔ okbytearray(r, st)) | A User Theorem |
| add-okclass | ¬ _type ∈ fis ⊦ okclass(refval(r), class1, addobj(r, class1, fis, st)) | A User Theorem |
| add-okclass-01 | ⊦ r ≠ r0 → (okclass(refval(r0), class1, addobj(r, class0, fis, st)) ↔ okclass(refval(r0), class1, st)) | A User Theorem |
| add-okreftype | ⊦ r ≠ r0 → (okreftype(refval(r), ty, addobj(r0, class1, fis, st)) ↔ okreftype(refval(r), ty, st)) | A User Theorem |
| add-okstore | ¬ _type ∈ fis ⊦ ¬ okstore(addobj(r, class1, fis, st)) → ¬ okstore(st) | A User Theorem |
| add-oktype | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) → (oktype(val, ty, addobj(r0, class1, fis, st)) ↔ oktype(val, ty, st)) | A User Theorem |
| add-oktype-01 | ⊦ r ≠ r0 → (oktype(refval(r), ty, addobj(r0, class1, fis, st)) ↔ oktype(refval(r), ty, st)) | A User Theorem |
| add-oktype-02 | ⊦ is_referencevalue(val) ∧ val .refval ≠ r0 → (oktype(val, ty, addobj(r0, class1, fis, st)) ↔ oktype(val, ty, st)) | A User Theorem |
| add-one | ⊦ addobj(r, class1, (sk × val) ', st) = (addobj(r, class1, [], st)[r -- sk, val]) | A User Theorem |
| add-out | ⊦ newref(r, st) → (addobj(r, class1, fis, st)[_out]) = st[_out] | A User Theorem |
| add-out-01 | ⊦ r ≠ jvmref → (addobj(r, class1, fis, st)[_out]) = st[_out] | A User Theorem |
| add-out-02 | ⊦ r ≠ jvmref → addobj(r, class1, fis, st[_out, val]) = (addobj(r, class1, fis, st)[_out, val]) | A User Theorem |
| add-put | ⊦ (addobj(r, class1, (sk × val) ', st)[r -- sk, val0]) = addobj(r, class1, (sk × val0) ', st) | A User Theorem |
| add-put-01 | ⊦ (addobj(r, class1, (sk × val) ' + fis, st)[r -- sk, val0]) = addobj(r, class1, (sk × val0) ' + fis, st) | A User Theorem |
| add-put-02 | sk ≠ sk0 ⊦ (addobj(r, class1, (sk0 × val1) ' + (sk × val) ' + fis, st)[r -- sk, val0]) = addobj(r, class1, (sk0 × val1) ' + (sk × val0) ' + fis, st) | A User Theorem |
| add-put-03 | ⊦ sks ≠ [] → (addobj(r, class1, (sk × val) ', st)[r -- (sk ' + sks), val0]) = (addobj(r, class1, (sk × val) ', st)[val .refval -- sks, val0]) | A User Theorem |
| add-put-04 | ⊦ sk ∈ fis ∧ sks ≠ [] → (addobj(r, class1, fis, st)[r -- (sk ' + sks), val0]) = (addobj(r, class1, fis, st)[fis[sk] .refval -- sks, val0]) | A User Theorem |
| add-put-05 | ⊦ (addobj(r, class1, (sk × val) ', st)[r -- (sk ' + sk0 ' + sks), val0]) = (addobj(r, class1, (sk × val) ', st)[val .refval -- (sk0 ' + sks), val0]) | A User Theorem |
| add-put-06 | ⊦ (addobj(r, class1, (sk × val) ', st)[r -- (sk ' + sk0 '), val0]) = (addobj(r, class1, (sk × val) ', st)[val .refval -- sk0, val0]) | A User Theorem |
| add-putbar-rew | ⊦ r ≠ r0 → putByteArray(bytes, r, i, addobj(r0, class, fis, st)) = addobj(r0, class, fis, putByteArray(bytes, r, i, st)) | A User Theorem |
| add-ref | ⊦ r ≠ r0 → (addobj(r, class1, fis, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| add-refin | ⊦ rk ∈ st → rk ∈ addobj(r, class, fis, st) | A User Theorem |
| add-refs | ⊦ addobj(r, class, fis, st) .refs = st .refs ++ r | A User Theorem |
| add-reftype | ⊦ reftypep(refval(r), addobj(r, class1, fis, st)) | A User Theorem |
| add-reftype-01 | ⊦ reftypep(refval(r0), st) → reftypep(refval(r0), addobj(r, class1, fis, st)) | A User Theorem |
| add-reftype-02 | ⊦ r ≠ r0 ∧ reftypep(st[r0 -- sk], st) → reftypep(st[r0 -- sk], addobj(r, class1, fis, st)) | A User Theorem |
| add-tput | ⊦ ¬ _type ∈ fis → (addobj(r, class1, fis, st)[r -- _type, val]) = addobj(r, class1, (_type × val) ' + fis, st) | A User Theorem |
| add-type | ¬ _type ∈ fis ⊦ (addobj(r, class1, fis, st)[r -- _type]) = typeval(mkclasstype(class1)) | A User Theorem |
| add-type-01 | ⊦ (addobj(r, class1, [], st)[r -- _type]) = typeval(mkclasstype(class1)) | A User Theorem |
| add-type-02 | ⊦ r -- _type ∈ addobj(r, class1, fis, st) | A User Theorem |
| add-type-03 | ⊦ is_typevalue(st[r0 -- _type]) ∧ ¬ _type ∈ fis → is_typevalue(addobj(r, class1, fis, st)[r0 -- _type]) | A User Theorem |
| add-type-04 | ¬ _type ∈ fis ⊦ (r -- _type) × typeval(mkclasstype(class1)) ∈ addobj(r, class1, fis, st) | A User Theorem |
| add-uninit | ⊦ r ≠ jvmref → (_uninit ∈ addobj(r, class, fis, st) ↔ _uninit ∈ st) | A User Theorem |
| add-update-same | ⊦ update(r, fis, addobj(r, class, fis0, st)) = addobj(r, class, fis + fis0, st) | A User Theorem |
| addclass-exactarray | ⊦ r ≠ jvmref → (exactarray(refval(r), ty, i, addclass(class0, fis, st)) ↔ exactarray(refval(r), ty, i, st)) | A User Theorem |
| addclass-mode-in | ⊦ class ≠ `java.lang.Object' .class → (_mode ∈ addclass(class, fis, st) ↔ _mode ∈ st) | A User Theorem |
| addclass-no | class1 ≠ class2 ⊦ addclass(class1, (mkfs(class2, ty, fieldvar) ' × val) ' + fis, st) = addclass(class1, fis, st) | A User Theorem |
| addclass-okarray | ⊦ okarray(r, ty, addclass(class, fis, st)) ↔ okarray(r, ty, st) | A User Theorem |
| addclass-okbytearray | ⊦ okbytearray(r, addclass(class, fis, st)) ↔ okbytearray(r, st) | A User Theorem |
| addclass-switch | ⊦ addclass(class, fis, st[r -- i ', val]) = (addclass(class, fis, st)[r -- i ', val]) | A User Theorem |
| addclass-switch-01 | ⊦ r ≠ jvmref → addclass(class, fis, st[r -- sk, val]) = (addclass(class, fis, st)[r -- sk, val]) | A User Theorem |
| addclass-union-sw | ⊦ ¬ jvmref ∈ st → st ∪ addclass(class0, fis0, st) = addclass(class0, fis0, st) | A User Theorem |
| addclass-update-sw | ⊦ r ≠ jvmref → update(r, fis, addclass(class0, fis0, st)) = addclass(class0, fis0, update(r, fis, st)) | A User Theorem |
| addclass-validFields | ⊦ r ≠ jvmref → (validFields(r, fis, addclass(class, fis0, st)) ↔ validFields(r, fis, st)) | A User Theorem |
| addobj-addclass-sw | ⊦ r ≠ jvmref → addobj(r, class, fis, addclass(class0, fis0, st)) = addclass(class0, fis0, addobj(r, class, fis, st)) | A User Theorem |
| addobj-addobj-switch | ⊦ r ≠ r0 → addobj(r, class, fis, addobj(r0, class0, fis0, st)) = addobj(r0, class0, fis0, addobj(r, class, fis, st)) | A User Theorem |
| addobj-at | ⊦ rk .ref ≠ r → (addobj(r, class, fis, st)[rk]) = st[rk] | A User Theorem |
| addobj-at-01 | ⊦ r ≠ r0 ∨ ¬ sk ∈ sks ∧ sk ≠ _type → (addobj(r0, class, sks, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| addobj-at-02 | ⊦ ¬ sk ∈ sks ∧ sk ≠ _type → (addobj(r0, class, sks, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| addobj-at-03 | ⊦ r ≠ r0 → (addobj(r0, class, sks, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| addobj-at-null | ⊦ r ≠ jvmref → (addobj(r, class, fis, st)[sk]) = st[sk] | A User Theorem |
| addobj-at-other | ⊦ r ≠ r0 ∧ sks ≠ [] → (addobj(r, class, fis, st)[r0 -- (sk ' + sks)]) = (addobj(r, class, fis, st)[st[r0 -- sk] .refval -- sks]) | A User Theorem |
| addobj-at-other-01 | ⊦ r ≠ r0 → (addobj(r, class, fis, st)[r0 -- (sk ' + sk0 ')]) = (addobj(r, class, fis, st)[st[r0 -- sk] .refval -- sk0]) | A User Theorem |
| addobj-at-other-02 | ⊦ r ≠ r0 → (addobj(r, class, fis, st)[r0 -- (sk ' + sk0 ' + sks)]) = (addobj(r, class, fis, st)[st[r0 -- sk] .refval -- (sk0 ' + sks)]) | A User Theorem |
| addobj-at-other-03 | ⊦ ¬ sk ∈ fis ∧ sk ≠ _type → (addobj(r, class, fis, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| addobj-at-this | ⊦ (addobj(r, class, (sk × val) ', st)[r -- (sk ' + sk0 ')]) = (addobj(r, class, (sk × val) ', st)[val .refval -- sk0]) | A User Theorem |
| addobj-at-this-01 | ⊦ (addobj(r, class, (sk × val) ', st)[r -- (sk ' + sk0 ' + sks)]) = (addobj(r, class, (sk × val) ', st)[val .refval -- (sk0 ' + sks)]) | A User Theorem |
| addobj-delsw | ⊦ r ≠ r0 → addobj(r0, class, fis, st) -- r = addobj(r0, class, fis, st -- r) | A User Theorem |
| addobj-getarray | ⊦ r ≠ r0 → getarray(r, addobj(r0, class, fis, st)) = getarray(r, st) | A User Theorem |
| addobj-getarray-01 | ⊦ r ≠ r0 → getarray(r, i, j, addobj(r0, class, fis, st)) = getarray(r, i, j, st) | A User Theorem |
| addobj-getintarray | ⊦ r ≠ r0 → getintarray(r, addobj(r0, class, fis, st)) = getintarray(r, st) | A User Theorem |
| addobj-getintarray-01 | ⊦ r ≠ r0 → getintarray(r, i, j, addobj(r0, class, fis, st)) = getintarray(r, i, j, st) | A User Theorem |
| addobj-in | ⊦ r ≠ r0 → (r -- sk ∈ addobj(r0, class, sks, st) ↔ r -- sk ∈ st) | A User Theorem |
| addobj-in-01 | ⊦ ¬ sk ∈ sks ∧ sk ≠ _type → (r -- sk ∈ addobj(r0, class, sks, st) ↔ r -- sk ∈ st) | A User Theorem |
| addobj-in-02 | ⊦ r ≠ r0 ∨ ¬ sk ∈ sks ∧ sk ≠ _type → (r -- sk ∈ addobj(r0, class, sks, st) ↔ r -- sk ∈ st) | A User Theorem |
| addobj-init | ⊦ r ≠ jvmref → (init(addobj(r, class, fis, st)) ↔ init(st)) | A User Theorem |
| addobj-init-01 | ⊦ r ≠ jvmref → (init(claset, addobj(r, class, fis, st)) ↔ init(claset, st)) | A User Theorem |
| addobj-init-02 | ⊦ r ≠ jvmref → (init(str, addobj(r, class, fis, st)) ↔ init(str, st)) | A User Theorem |
| addobj-initdone | ⊦ r ≠ jvmref → (initdone(class0, addobj(r, class, sks, st)) ↔ initdone(class0, st)) | A User Theorem |
| addobj-initerror | ⊦ r ≠ jvmref → (initerror(class0, addobj(r, class, sks, st)) ↔ initerror(class0, st)) | A User Theorem |
| addobj-initundone | ⊦ r ≠ jvmref → (initundone(class0, addobj(r, class, sks, st)) ↔ initundone(class0, st)) | A User Theorem |
| addobj-isarray | ⊦ r ≠ r0 → (is_array(r, addobj(r0, class, fis, st)) ↔ is_array(r, st)) | A User Theorem |
| addobj-isarray-01 | ⊦ ¬ _type ∈ fis → ¬ is_array(r, addobj(r, class, fis, st)) | A User Theorem |
| addobj-keys-one | ⊦ addobj(r, class, sk ', st) = (addobj(r, class, [], st)[r -- sk, initial_value(sk .fs .type)]) | A User Theorem |
| addobj-mode | ⊦ (addobj(r, class, [], st)[_mode]) = st[_mode] | A User Theorem |
| addobj-mode-01 | ⊦ (addobj(r, class, [], st)[_mode]) = st[_mode] | A User Theorem |
| addobj-okarray | ⊦ r ≠ r0 → (okarray(r, ty, addobj(r0, class, fis, st)) ↔ okarray(r, ty, st)) | A User Theorem |
| addobj-okbytearray | ⊦ okbytearray(r, st) ∧ newref(r0, st) → (¬ okbytearray(r, addobj(r0, class, fis, st)) ↔ false) | A User Theorem |
| addobj-oktype | ⊦ oktype(val, ty, addobj(r, class, fis, st)) ↔ oktype(val, ty, st) | A User Theorem |
| addobj-out-put | ⊦ r ≠ jvmref → (addobj(r, class, fis, st)[_out, val][r -- sk, val0]) = (addobj(r, class, fis, st)[r -- sk, val0][_out, val]) | A User Theorem |
| addobj-put | ⊦ r ≠ r0 ∧ r0 ≠ jvmref → (addobj(r, class1, fis, st)[r0 -- sk, val]) = addobj(r, class1, fis, st[r0 -- sk, val]) | A User Theorem |
| addobj-put-switch | ⊦ r ≠ r0 → addobj(r, class1, fis, st[r0 -- sk, val]) = (addobj(r, class1, fis, st)[r0 -- sk, val]) | A User Theorem |
| addobj-put-switch-01 | ⊦ rk .ref ≠ r → addobj(r, class, fis, st[rk, val]) = (addobj(r, class, fis, st)[rk, val]) | A User Theorem |
| addobj-rec-01 | ⊦ addobj(r, class1, fv ' + fis, st) = (addobj(r, class1, fis, st)[r -- fv .1, fv .2]) | A User Theorem |
| addobj-subset | ⊦ newref(r, st) → st ⊆ addobj(r, class, instfields(class), st) | A User Theorem |
| addobj-throw-subset | ⊦ st[_mode] = noval ∧ newref(r, st) → st ⊆ (addobj(r, class, fis, st)[_mode, noval]) | A User Theorem |
| addobj-type | ⊦ fis .keys = instfields(class) → (addobj(r, class, fis, st)[r -- _type]) = typeval(mkclasstype(class)) | A User Theorem |
| addobj-union | ⊦ newref(r, st) ∧ newref(r, st0) → addobj(r, class, fis, st) ∪ st0 = addobj(r, class, fis, st ∪ st0) | A User Theorem |
| addobj-union-rew | ⊦ newref(r, st ∪ st0) → addobj(r, class, fis, st ∪ st0) = st ∪ addobj(r, class, fis, st0) | A User Theorem |
| addobj-union-switch | ⊦ r ≠ r0 → addobj(r, class, fis, update(r0, fis0, st)) = update(r0, fis0, addobj(r, class, fis, st)) | A User Theorem |
| ao-init | ⊦ r ≠ jvmref → (initdone(class1, addobj(r, class2, fis, st)) ↔ initdone(class1, st)) | A User Theorem |
| ao-init-01 | ⊦ r ≠ jvmref → (initundone(class1, addobj(r, class2, fis, st)) ↔ initundone(class1, st)) | A User Theorem |
| ao-init-02 | ⊦ r ≠ jvmref → (initerror(class1, addobj(r, class2, fis, st)) ↔ initerror(class1, st)) | A User Theorem |
| ao-put | ⊦ r ≠ r0 → (addobj(r, class1, fis, st)[r0 -- sk, val]) = addobj(r, class1, fis, st[r0 -- sk, val]) | A User Theorem |
| del-addobj | ⊦ newref(r, st) → addobj(r, class, fis, st) -- r = st | A User Theorem |
| endfinallymode | ⊦ r ≠ jvmref → (_endfinallymode ∈ addobj(r, class1, fis, st) ↔ _endfinallymode ∈ st) | A User Theorem |
| endfinallymode-01 | ⊦ newref(r, st) → (addobj(r, class1, fis, st)[_endfinallymode]) = st[_endfinallymode] | A User Theorem |
| endfinallymode-02 | ⊦ r ≠ jvmref → (addobj(r, class1, fis, st)[_endfinallymode]) = st[_endfinallymode] | A User Theorem |
| endfinallymode-03 | ⊦ (addobj(newref(st), class, fis, st)[_endfinallymode]) = st[_endfinallymode] | A User Theorem |
| endfinallymode-04 | class1 ≠ `java.lang.Object' .class ⊦ (addclass(class1, fis, st)[_endfinallymode]) = st[_endfinallymode] | A User Theorem |
| endfinallymode-05 | ⊦ ¬ _endfinallymode .key ∈ fis → (addclass(class, fis, st)[_endfinallymode]) = st[_endfinallymode] | A User Theorem |
| eqmode-01 | ⊦ newref(r, st) → (addobj(r, class1, [], st)[_mode, throw(r, mkclasstype(class1))]) =mode st | A User Theorem |
| exactarray-addobj | ⊦ r ≠ r0 → (exactarray(refval(r), ty, i, addobj(r0, class, fis, st)) ↔ exactarray(refval(r), ty, i, st)) | A User Theorem |
| exactarray-addobj-01 | ⊦ is_referencevalue(val) ∧ val .refval ≠ r0 → (exactarray(val, ty, i, addobj(r0, class, fis, st)) ↔ exactarray(val, ty, i, st)) | A User Theorem |
| getByteArray-addobject | ⊦ r ≠ r1 → getbytearray(r1, addobj(r, class, fis, st)) = getbytearray(r1, st) | A User Theorem |
| getByteArray-addobject-01 | ⊦ r ≠ r1 → getbytearray(r1, i, j, addobj(r, class, fis, st)) = getbytearray(r1, i, j, st) | A User Theorem |
| haskeys-addobj | ⊦ r ≠ r0 → (hasKeys(r, sks, addobj(r0, class, fis, st)) ↔ hasKeys(r, sks, st)) | A User Theorem |
| instfields-Object | ⊦ instfields(`java.lang.Object' .class) = [] | A User Theorem |
| instfields-index-01 | ⊦ is_indexkey(sk) → ¬ sk ∈ instfields(class) | A User Theorem |
| instfields-index-02 | ⊦ sk ∈ instfields(class0) → (sk .fs = mkfs(class, ty, fieldvar) ↔ sk = mkfs(class, ty, fieldvar) ') | A User Theorem |
| instfields-subclass-01 | ⊦ sk ∈ instfields(class) ∧ class0 ≤ class → sk ∈ instfields(class0) | A User Theorem |
| instfields-subclass-in | ⊦ fs ' ∈ instfields(class) ∧ ty ≤ mkclasstype(class) ∧ is_classtype(ty) → fs ' ∈ instfields(ty .class) | A User Theorem |
| instfields-type | ⊦ fis .keys = instfields(class) → ¬ _type ∈ fis | A User Theorem |
| instfields-type-01 | ⊦ ¬ _type ∈ instfields(class) | A User Theorem |
| instore-addobj | unique_al(fis), ¬ _type ∈ fis ⊦ r ≠ jvmref → instore(r, class, fis, addobj(r, class, fis, st)) | A User Theorem |
| instore-addobj-rec | ⊦ r ≠ r1 → (instore(r, class, fis, addobj(r1, class1, fis1, st)) ↔ instore(r, class, fis, st)) | A User Theorem |
| is_array-addobj | ⊦ r ≠ r0 → (is_array(str, r, addobj(r0, class, fis, st)) ↔ is_array(str, r, st)) | A User Theorem |
| is_array-addobj-01 | ⊦ ¬ _type ∈ fis → ¬ is_array(str, r, addobj(r, class, fis, st)) | A User Theorem |
| is_array-validref | ⊦ ¬ is_valid_ref(r, st) → ¬ is_array(str, r, st) | A User Theorem |
| is_obj-01 | ⊦ ¬ is_obj(r, st) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-addobj | ⊦ r ≠ r0 → (is_obj(str, r, addobj(r0, class, fis, st)) ↔ is_obj(str, r, st)) | A User Theorem |
| is_obj-addobj-01 | ⊦ fis .keys = instfields(class) ∧ class+∃(str, class) ∧ validfieldinits(fis, st) ∧ ¬ is_abstract(class) ∧ r ≠ jvmref → is_obj(str, r, addobj(r, class, fis, st)) | A User Theorem |
| is_obj-array | ⊦ st[r -- _type] .type ≤ mkarraytype(ty) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-array-01 | ⊦ is_array(r, st) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-arraytype | ⊦ is_arraytype(st[r -- _type] .type) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-arraytype-01 | ⊦ is_arraytype(st[r -- (sk ' + _type ')] .type) → ¬ is_obj(str, st[r -- sk] .refval, st) | A User Theorem |
| is_obj-arraytype-02 | ⊦ st[r -- _type] = typeval(mkarraytype(ty)) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-bytearray | ⊦ is_obj(str, r, st) → ¬ okbytearray(r, st) | A User Theorem |
| is_obj-classtype | ⊦ ¬ is_classtype(st[r -- _type] .type) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-del | ⊦ r ≠ r0 → (is_obj(str, r0, st -- r) ↔ is_obj(str, r0, st)) | A User Theorem |
| is_obj-del-01 | ⊦ ¬ is_obj(str, r, st -- r) | A User Theorem |
| is_obj-field-in | ⊦ ¬ r -- sk ∈ st ∧ sk ∈ instfields(class) ∧ st[r -- _type] .type ≤ mkclasstype(class) ∧ r ≠ jvmref → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-field-noreftype | ⊦ is_referencevalue(st[r -- fs ']) ∧ ¬ is_reftype(fs .type) ∧ fs ' ∈ instfields(class) ∧ st[r -- _type] .type = mkclasstype(class) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-field-norefval | ⊦ ¬ is_referencevalue(st[r -- fs ']) ∧ is_reftype(fs .type) ∧ fs ' ∈ instfields(class) ∧ st[r -- _type] .type = mkclasstype(class) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-full-expand | ⊦ is_obj(str, r, st) ↔ class+∃(str, st[r -- _type] .type .class) ∧ ¬ is_abstract(st[r -- _type] .type .class) ∧ r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ is_classtype(st[r -- _type] .type) ∧ (r -- _type) × st[r -- _type] ∈ st ∧ goodfieldsandtypes(r, instfields(st[r -- _type] .type .class), st) | A User Theorem |
| is_obj-hasclasstype | ⊦ ¬ has_classtype(st[r -- _type] .type) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-isarray | ⊦ is_obj(str, r, st) → ¬ is_array(str, r, st) | A User Theorem |
| is_obj-isobj-01 | ⊦ ¬ is_obj(r, class, st) ∧ st[r -- _type] = typeval(mkclasstype(class)) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-newref | ⊦ newref(r, st) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-no-interface | ⊦ is_obj(str, r, st) ∧ st[r -- _type] .type = mkclasstype(class) → ¬ interface∃(str, class) | A User Theorem |
| is_obj-no-refval | mkfs(str2 .class, mkclasstype(str0 .class), str1 .field) ' ∈ instfields(st[r -- _type] .type .class) ⊦ ¬ is_referencevalue(st[r -- mkfs(((* str2)) .class, mkclasstype(((* str0)) .class), ((* str1)) .field) ']) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-no-refval-01 | mkfs(str2 .class, mkarraytype(ty), str1 .field) ' ∈ instfields(st[r -- _type] .type .class) ⊦ ¬ is_referencevalue(st[r -- mkfs(((* str2)) .class, mkarraytype(ty), ((* str1)) .field) ']) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-no-refval-02 | mkfs(str2 .class, mkclasstype(str0 .class), str1 .field) ' ∈ instfields(st[r -- _type] .type .class) ⊦ is_obj(str, r, st) → (¬ is_referencevalue(st[r -- mkfs(((* str2)) .class, mkclasstype(((* str0)) .class), ((* str1)) .field) ']) ↔ false) | A User Theorem |
| is_obj-no-refval-03 | mkfs(str2 .class, mkarraytype(ty), str1 .field) ' ∈ instfields(st[r -- _type] .type .class) ⊦ is_obj(str, r, st) → (¬ is_referencevalue(st[r -- mkfs(((* str2)) .class, mkarraytype(ty), ((* str1)) .field) ']) ↔ false) | A User Theorem |
| is_obj-not-classex | ⊦ ¬ class+∃(str, st[r -- _type] .type .class) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-not-classex-01 | ⊦ ¬ class+∃(str, class) ∧ st[r -- _type] .type = mkclasstype(class) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-not-classex-02 | ⊦ ¬ class∃(str, class) ∧ st[r -- _type] .type = mkclasstype(class) ∧ ¬ is_predefined_class(class) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-not-tdnameex | ⊦ ¬ tdname∃(str, class) ∧ st[r -- _type] .type = mkclasstype(class) ∧ ¬ is_predefined_class(class) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-notin | ⊦ ¬ r ∈ st → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-notin-01 | ⊦ ¬ r -- sk ∈ st ∧ sk ∈ instfields(st[r -- _type] .type .class) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-null | ⊦ ¬ is_obj(str, jvmref, st) | A User Theorem |
| is_obj-put | ⊦ is_obj(str, r, st) ∧ oktype(val, ty, st) ∧ ty ≠ void_type → is_obj(str, r, st[r1 -- mkfs(class, ty, fieldvar) ', val]) | A User Theorem |
| is_obj-put-01 | ⊦ r ≠ r0 → (is_obj(str, r0, st[r -- sk, val]) ↔ is_obj(str, r0, st)) | A User Theorem |
| is_obj-put-badfield | ⊦ is_obj(str, r, st) ∧ fs ' ≠ _type ∧ ¬ fs ' ∈ instfields(st[r -- _type] .type .class) → is_obj(str, r, st[r -- fs ', val]) | A User Theorem |
| is_obj-put-equiv | ⊦ okval(st[r1 -- sk], sk .fs .type) ∧ r1 -- sk ∈ st ∧ is_fskey(sk) ∧ okval(val, sk .fs .type) ∧ sk .fs .type ≠ void_type → (is_obj(str, r, st[r1 -- sk, val]) ↔ is_obj(str, r, st)) | A User Theorem |
| is_obj-put-index | ⊦ is_obj(str, r, st[r0 -- i ', val]) ↔ is_obj(str, r, st) | A User Theorem |
| is_obj-put-samefield | ⊦ r -- fs ' ∈ st ∧ oktype(st[r -- fs '], fs .type, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _type → (is_obj(str, r, st[r -- fs ', val]) ↔ is_obj(str, r, st)) | A User Theorem |
| is_obj-put-samefield-01 | ⊦ is_obj(str, r, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _type → is_obj(str, r, st[r -- fs ', val]) | A User Theorem |
| is_obj-put-statfield | ⊦ is_obj(str, r, st[jvmref -- sk, val]) ↔ is_obj(str, r, st) | A User Theorem |
| is_obj-putba | ⊦ r ≠ r1 → (is_obj(r, class, sk ', putByteArray(bytes, r1, i, st)) ↔ is_obj(r, class, sk ', st)) | A User Theorem |
| is_obj-putbar | ⊦ is_obj(str, r, putByteArray(bytes, r1, i, st)) → is_obj(str, r, st) | A User Theorem |
| is_obj-reftype | ⊦ ¬ is_reftype(st[r -- _type] .type) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-refval | mkfs(str2 .class, mkclasstype(str0 .class), str1 .field) ' ∈ instfields(st[r -- _type] .type .class) ⊦ is_obj(str, r, st) → refval(st[r -- mkfs(((* str2)) .class, mkclasstype(((* str0)) .class), ((* str1)) .field) '] .refval) = st[r -- mkfs(str2 .class, mkclasstype(str0 .class), str1 .field) '] | A User Theorem |
| is_obj-refval-01 | mkfs(str2 .class, mkarraytype(ty), str1 .field) ' ∈ instfields(st[r -- _type] .type .class) ⊦ is_obj(str, r, st) → refval(st[r -- mkfs(((* str2)) .class, mkarraytype(ty), ((* str1)) .field) '] .refval) = st[r -- mkfs(str2 .class, mkarraytype(ty), str1 .field) '] | A User Theorem |
| is_obj-subset | ⊦ st ⊆ st1 ∧ is_obj(str, r, st) → is_obj(str, r, st1) | A User Theorem |
| is_obj-type | ⊦ ¬ r -- _type ∈ st → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-type-01 | ⊦ ¬ is_typevalue(st[r -- _type]) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-type-02 | ⊦ st[r -- _type] .type = mkarraytype(ty) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-typeex | ⊦ ¬ type∃(str, st[r -- _type] .type) ∧ r ≠ jvmref → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-typeex-01 | ⊦ ¬ type∃(str, ty) ∧ st[r -- _type] = typeval(ty) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-typeex-02 | ⊦ ¬ type∃(str, st[r -- _type] .type) → ¬ is_obj(str, r, st) | A User Theorem |
| is_obj-typele | ⊦ is_obj(str, r, st) → st[r -- _type] .type ≤ mkclasstype(`java.lang.Object' .class) | A User Theorem |
| is_obj-union | ⊦ is_obj(str, r, st) → is_obj(str, r, st0 ∪ st) | A User Theorem |
| is_obj-union-disjoint | ⊦ st1 .refs ∩ st .refs = ∅ ∧ r ∈ st1 ∧ is_obj(str, r, st1) → is_obj(str, r, st1 ∪ st) | A User Theorem |
| is_obj-update | ⊦ r ≠ r0 → (is_obj(str, r, update(r0, fis, st)) ↔ is_obj(str, r, st)) | A User Theorem |
| is_obj-validref | ⊦ ¬ is_valid_ref(r, st) → ¬ is_obj(str, r, st) | A User Theorem |
| is_valid_ref | ⊦ ¬ is_obj(str, r, st) → (is_valid_ref(str, r, st) ↔ is_array(str, r, st)) | A User Theorem |
| is_valid_ref-01 | ⊦ ¬ is_array(str, r, st) → (is_valid_ref(str, r, st) ↔ is_obj(str, r, st)) | A User Theorem |
| is_valid_ref-02 | ⊦ is_obj(r, class, st) → (is_valid_ref(str, r, st) ↔ class+∃(str, class) ∧ ¬ is_abstract(class)) | A User Theorem |
| is_valid_ref-03 | ⊦ ¬ is_valid_ref(r, st) → ¬ is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-addobj | ⊦ r ≠ r0 → (is_valid_ref(str, r, addobj(r0, class, fis, st)) ↔ is_valid_ref(str, r, st)) | A User Theorem |
| is_valid_ref-addobj-01 | ⊦ ¬ _type ∈ fis → (is_valid_ref(str, r, addobj(r, class, fis, st)) ↔ is_obj(str, r, addobj(r, class, fis, st))) | A User Theorem |
| is_valid_ref-array | ⊦ st[r -- _type] .type = mkarraytype(ty) ∧ r ≠ jvmref → (is_valid_ref(str, r, st) ↔ is_array(str, r, st)) | A User Theorem |
| is_valid_ref-array-01 | ⊦ is_arraytype(st[r -- _type] .type) ∧ r ≠ jvmref → (is_valid_ref(str, r, st) ↔ is_array(str, r, st)) | A User Theorem |
| is_valid_ref-def | ⊦ is_valid_ref(str, r, st) ↔ ¬ ¬ (is_valid_ref(r, st) ∧ (is_obj(str, r, st) ∨ is_array(str, r, st))) | A User Theorem |
| is_valid_ref-del | ⊦ ¬ is_valid_ref(str, r, st -- r) | A User Theorem |
| is_valid_ref-del-01 | ⊦ r ≠ r0 → (is_valid_ref(str, r, st -- r0) ↔ is_valid_ref(str, r, st)) | A User Theorem |
| is_valid_ref-field-in | ⊦ ¬ r -- sk ∈ st ∧ sk ∈ instfields(class) ∧ st[r -- _type] .type ≤ mkclasstype(class) ∧ r ≠ jvmref → ¬ is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-int | ⊦ is_valid_ref(str, r, st) → st[r -- _type] .type ≠ int_type | A User Theorem |
| is_valid_ref-isarray | ⊦ is_array(str, r, st) → is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-isobj | ⊦ is_obj(str, r, st) → is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-new | ⊦ newref(r, st) → ¬ is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-no-arraytype | ⊦ ¬ is_arraytype(st[r -- _type] .type) → (is_valid_ref(str, r, st) ↔ is_obj(str, r, st)) | A User Theorem |
| is_valid_ref-notin | ⊦ ¬ r ∈ st → ¬ is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-notin-01 | ⊦ ¬ r -- _type ∈ st → ¬ is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-notin-02 | ⊦ ¬ r ∈ st .refs → ¬ is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-null | ⊦ ¬ is_valid_ref(str, jvmref, st) | A User Theorem |
| is_valid_ref-obj | ⊦ st[r -- _type] .type ≤ mkclasstype(class) ∧ class ≠ `java.lang.Object' .class ∧ r ≠ jvmref → (is_valid_ref(str, r, st) ↔ is_obj(str, r, st)) | A User Theorem |
| is_valid_ref-okbytearray | ⊦ okbytearray(r, st) → is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-primarray | ⊦ st[r -- _type] = typeval(mkarraytype(ty)) ∧ is_primtype(ty) → (is_valid_ref(str, r, st) ↔ is_array(r, st)) | A User Theorem |
| is_valid_ref-primtype | ⊦ is_valid_ref(str, r, st) → st[r -- _type] .type ≠ byte_type | A User Theorem |
| is_valid_ref-primtype-01 | ⊦ is_valid_ref(str, r, st) → st[r -- _type] .type ≠ short_type | A User Theorem |
| is_valid_ref-put | ⊦ oktype(val, ty, st) ∧ is_valid_ref(str, r, st) ∧ ty ≠ void_type ∧ mkfs(class, ty, fieldvar) ' ≠ _length → is_valid_ref(str, r, st[r1 -- mkfs(class, ty, fieldvar) ', val]) | A User Theorem |
| is_valid_ref-put-01 | ⊦ r ≠ r0 → (is_valid_ref(str, r0, st[r -- sk, val]) ↔ is_valid_ref(str, r0, st)) | A User Theorem |
| is_valid_ref-put-byte | ⊦ is_array(str, r0, st) ∧ okbytearray(r, st) → is_valid_ref(str, r0, st[r -- i ', byteval(by)]) | A User Theorem |
| is_valid_ref-put-equiv | ⊦ okval(st[r1 -- sk], sk .fs .type) ∧ r1 -- sk ∈ st ∧ is_fskey(sk) ∧ okval(val, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length → (is_valid_ref(str, r, st[r1 -- sk, val]) ↔ is_valid_ref(str, r, st)) | A User Theorem |
| is_valid_ref-put-index | ⊦ is_obj(str, r0, st) → is_valid_ref(str, r0, st[r -- i ', val]) | A User Theorem |
| is_valid_ref-put-samefield | ⊦ r -- fs ' ∈ st ∧ oktype(st[r -- fs '], fs .type, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _length ∧ fs ' ≠ _type → (is_valid_ref(str, r, st[r -- fs ', val]) ↔ is_valid_ref(str, r, st)) | A User Theorem |
| is_valid_ref-put-samefield-01 | ⊦ is_valid_ref(str, r, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _length ∧ fs ' ≠ _type → is_valid_ref(str, r, st[r -- fs ', val]) | A User Theorem |
| is_valid_ref-putbytearray | ⊦ st[r0 -- _type] .type ≤ ty ∧ ¬ is_arraytype(ty) ∧ ty ≠ mkclasstype(`java.lang.Object' .class) → (is_valid_ref(str, r0, putByteArray(bytes, r, i, st)) ↔ is_valid_ref(str, r0, st)) | A User Theorem |
| is_valid_ref-reftype | ⊦ ¬ is_reftype(st[r -- _type] .type) → ¬ is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-type | ⊦ is_valid_ref(str, r, st) ∧ r ≠ jvmref → st[r -- _type] .type ≤ mkclasstype(`java.lang.Object' .class) | A User Theorem |
| is_valid_ref-type-01 | ⊦ st[r -- _type] .type = mkclasstype(class) → (is_valid_ref(str, r, st) ↔ is_obj(str, r, st)) | A User Theorem |
| is_valid_ref-type-typeval | ⊦ st[r -- _type] .type = ty ∧ is_valid_ref(str, r, st) → st[r -- _type] = typeval(ty) | A User Theorem |
| is_valid_ref-typeex | ⊦ ¬ type∃(str, st[r -- _type] .type) ∧ r ≠ jvmref → ¬ is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-typeex-01 | ⊦ ¬ type∃(str, ty) ∧ st[r -- _type] = typeval(ty) → ¬ is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-typeex-02 | ⊦ ¬ type∃(str, st[r -- _type] .type) → ¬ is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-typeval | ⊦ ¬ is_typevalue(st[r -- _type]) → ¬ is_valid_ref(str, r, st) | A User Theorem |
| is_valid_ref-typeval-01 | ⊦ is_valid_ref(str, r, st) → typeval(st[r -- _type] .type) = st[r -- _type] | A User Theorem |
| is_valid_ref-update | ⊦ r ≠ r0 → (is_valid_ref(str, r, update(r0, fis, st)) ↔ is_valid_ref(str, r, st)) | A User Theorem |
| is_valid_ref-void | ⊦ st[r -- _type] = typeval(void_type) ∧ r ≠ jvmref → ¬ is_valid_ref(str, r, st) | A User Theorem |
| isarray-isobj | ⊦ is_array(r, st) → ¬ is_obj(r, st) | A User Theorem |
| isarray-isobj-01 | ⊦ is_array(str, r, st) → ¬ is_obj(str, r, st) | A User Theorem |
| isobj-addclass | ⊦ class ≠ class0 → (is_obj(r, class, sks, addclass(class0, fis, st)) ↔ is_obj(r, class, sks, st)) | A User Theorem |
| isobj-addobj | ⊦ r ≠ r0 → (is_obj(r, class, sks, addobj(r0, class0, fis, st)) ↔ is_obj(r, class, sks, st)) | A User Theorem |
| isobj-addobj-01 | ⊦ ¬ is_obj(r, class, addobj(r0, class0, fis, st)) ∧ newref(r0, st) → ¬ is_obj(r, class, st) | A User Theorem |
| isobj-addobj-02 | ⊦ r ≠ r0 → (is_obj(r, addobj(r0, class, fis, st)) ↔ is_obj(r, st)) | A User Theorem |
| isobj-addobj-03 | ⊦ r ≠ r0 → (is_obj(r, class0, addobj(r0, class, fis, st)) ↔ is_obj(r, class0, st)) | A User Theorem |
| isobj-addobj-04 | ⊦ fis .keys = instfields(class) ∧ validfieldinits(fis, st) ∧ r ≠ jvmref → is_obj(r, addobj(r, class, fis, st)) | A User Theorem |
| isobj-all | ⊦ is_obj(r, class, sks, st) ↔ r ≠ jvmref ∧ (r -- _type) × typeval(mkclasstype(class)) ∈ st ∧ (∀ sk. sk ∈ sks → goodfieldandtype(r, sk, st)) | A User Theorem |
| isobj-array | ⊦ okreftype(refval(r), mkarraytype(ty), st) → ¬ is_obj(r, st) | A User Theorem |
| isobj-array-01 | ⊦ is_obj(r, st) → ¬ is_array(str, r, st) | A User Theorem |
| isobj-arraytype | ⊦ is_arraytype(st[r -- _type] .type) → ¬ is_obj(r, st) | A User Theorem |
| isobj-arraytype-01 | ⊦ is_arraytype(st[r -- (sk ' + _type ')] .type) → ¬ is_obj(st[r -- sk] .refval, st) | A User Theorem |
| isobj-arraytype-02 | ⊦ st[r -- _type] = typeval(mkarraytype(ty)) → ¬ is_obj(r, st) | A User Theorem |
| isobj-bytearray | ⊦ is_obj(r, st) → ¬ okbytearray(r, st) | A User Theorem |
| isobj-classtype | ⊦ ¬ is_classtype(st[r -- _type] .type) → ¬ is_obj(r, st) | A User Theorem |
| isobj-del | ⊦ r ≠ r0 → (is_obj(r, class, sks, st -- r0) ↔ is_obj(r, class, sks, st)) | A User Theorem |
| isobj-del-01 | ⊦ r ≠ r0 → (is_obj(r, class, st -- r0) ↔ is_obj(r, class, st)) | A User Theorem |
| isobj-del-02 | ⊦ ¬ is_obj(r, class, st -- r) | A User Theorem |
| isobj-del-03 | ⊦ r ≠ r0 → (is_obj(r0, st -- r) ↔ is_obj(r0, st)) | A User Theorem |
| isobj-del-04 | ⊦ ¬ is_obj(r, st -- r) | A User Theorem |
| isobj-field-in | ⊦ ¬ r -- sk ∈ st ∧ sk ∈ instfields(class) ∧ st[r -- _type] .type ≤ mkclasstype(class) ∧ r ≠ jvmref → ¬ is_obj(r, st) | A User Theorem |
| isobj-fieldtype | ⊦ st[r -- mkfs(class0, int_type, fieldvar) '] = refval(r0) ∧ is_obj(r, class, st) → ¬ mkfs(class0, int_type, fieldvar) ' ∈ instfields(class) | A User Theorem |
| isobj-hasclasstype | ⊦ ¬ has_classtype(st[r -- _type] .type) → ¬ is_obj(r, st) | A User Theorem |
| isobj-instfields | ⊦ sk ∈ instfields(st[r -- _type] .type .class) ∧ is_obj(r, class, st) → st[r -- _type] = typeval(mkclasstype(class)) | A User Theorem |
| isobj-isarray | ⊦ is_obj(r, st) → ¬ is_array(r, st) | A User Theorem |
| isobj-isobj | ⊦ ¬ is_obj(r, st) → ¬ is_obj(r, class, st) | A User Theorem |
| isobj-isobj-01 | ⊦ ¬ is_obj(r, class, st) ∧ st[r -- _type] = typeval(mkclasstype(class)) → ¬ is_obj(r, st) | A User Theorem |
| isobj-jvmref | ⊦ is_obj(r, class1, sks, st) → r ≠ jvmref | A User Theorem |
| isobj-mode | ⊦ is_obj(r, class, sks, st[_mode, val]) ↔ is_obj(r, class, sks, st) | A User Theorem |
| isobj-newref | ⊦ newref(r, st) → ¬ is_obj(r, class, sks, st) | A User Theorem |
| isobj-newref-01 | ⊦ newref(r, st) → ¬ is_obj(r, class, st) | A User Theorem |
| isobj-newref-02 | ⊦ newref(r, st) → ¬ is_obj(r, st) | A User Theorem |
| isobj-notin | ⊦ ¬ r ∈ st → ¬ is_obj(r, class, sks, st) | A User Theorem |
| isobj-notin-01 | ⊦ ¬ r ∈ st .refs → ¬ is_obj(r, class, sks, st) | A User Theorem |
| isobj-notin-02 | ⊦ ¬ is_obj(r, class, sks, st -- r) | A User Theorem |
| isobj-notin-03 | ⊦ ¬ r ∈ st .refs → ¬ is_obj(r, class, st) | A User Theorem |
| isobj-notin-04 | ⊦ ¬ r ∈ st → ¬ is_obj(r, class, st) | A User Theorem |
| isobj-notin-05 | ⊦ ¬ r ∈ st → ¬ is_obj(r, st) | A User Theorem |
| isobj-null | ⊦ ¬ is_obj(jvmref, class, sks, st) | A User Theorem |
| isobj-null-01 | ⊦ ¬ is_obj(jvmref, class, st) | A User Theorem |
| isobj-null-02 | ⊦ ¬ is_obj(jvmref, st) | A User Theorem |
| isobj-put | ⊦ r ≠ r0 → (is_obj(r, class, sks, st[r0 -- sk, val]) ↔ is_obj(r, class, sks, st)) | A User Theorem |
| isobj-put-01 | ⊦ r ≠ r0 → (is_obj(r, class, st[r0 -- sk, val]) ↔ is_obj(r, class, st)) | A User Theorem |
| isobj-put-02 | ⊦ is_obj(r, st) ∧ oktype(val, ty, st) ∧ ty ≠ void_type → is_obj(r, st[r1 -- mkfs(class, ty, fieldvar) ', val]) | A User Theorem |
| isobj-put-03 | ⊦ is_obj(r, class0, st) ∧ oktype(val, ty, st) ∧ ty ≠ void_type → is_obj(r, class0, st[r1 -- mkfs(class, ty, fieldvar) ', val]) | A User Theorem |
| isobj-put-04 | ⊦ r ≠ r0 → (is_obj(r0, st[r -- sk, val]) ↔ is_obj(r0, st)) | A User Theorem |
| isobj-put-badfield | ⊦ is_obj(r, st) ∧ fs ' ≠ _type ∧ ¬ fs ' ∈ instfields(st[r -- _type] .type .class) → is_obj(r, st[r -- fs ', val]) | A User Theorem |
| isobj-put-index-01 | ⊦ is_obj(r, class, st[r0 -- i ', val]) ↔ is_obj(r, class, st) | A User Theorem |
| isobj-put-index-02 | ⊦ is_obj(r, st[r0 -- i ', val]) ↔ is_obj(r, st) | A User Theorem |
| isobj-put-samefield | ⊦ r -- fs ' ∈ st ∧ oktype(st[r -- fs '], fs .type, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _type → (is_obj(r, st[r -- fs ', val]) ↔ is_obj(r, st)) | A User Theorem |
| isobj-put-samefield-01 | ⊦ r -- fs ' ∈ st ∧ oktype(st[r -- fs '], fs .type, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _type → (is_obj(r, class, st[r -- fs ', val]) ↔ is_obj(r, class, st)) | A User Theorem |
| isobj-put-samefield-02 | ⊦ is_obj(r, class, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _type → is_obj(r, class, st[r -- fs ', val]) | A User Theorem |
| isobj-put-samefield-03 | ⊦ is_obj(r, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _type → is_obj(r, st[r -- fs ', val]) | A User Theorem |
| isobj-put-statfield | ⊦ is_obj(r, st[jvmref -- sk, val]) ↔ is_obj(r, st) | A User Theorem |
| isobj-putbar | ⊦ is_obj(r, putByteArray(bytes, r1, i, st)) → is_obj(r, st) | A User Theorem |
| isobj-putbar-01 | ⊦ is_obj(r, putByteArray(bytes, r1, i, st)) ↔ is_obj(r, st) | A User Theorem |
| isobj-putbar-02 | ⊦ is_obj(str, r, putByteArray(bytes, r1, i, st)) ↔ is_obj(str, r, st) | A User Theorem |
| isobj-putref | ⊦ r ≠ rk .ref → (is_obj(r, class, sks, st[rk, refval(r)]) ↔ is_obj(r, class, sks, st)) | A User Theorem |
| isobj-rec | ⊦ is_obj(r, class, sk ' + sks, st) ↔ goodfieldandtype(r, sk, st) ∧ is_obj(r, class, sks, st) | A User Theorem |
| isobj-reftype | ⊦ ¬ is_reftype(st[r -- _type] .type) → ¬ is_obj(r, st) | A User Theorem |
| isobj-subset | ⊦ st ⊆ st1 ∧ is_obj(r, st) → is_obj(r, st1) | A User Theorem |
| isobj-type | ⊦ is_obj(r, class1, sks, st) → st[r -- _type] .type = mkclasstype(class1) | A User Theorem |
| isobj-type-01 | ⊦ is_obj(r, class1, sks, st) → (st[r -- _type] .type = mkclasstype(class1) ↔ true) | A User Theorem |
| isobj-type-02 | ⊦ is_obj(r, class, st) → st[r -- _type] = typeval(mkclasstype(class)) | A User Theorem |
| isobj-type-03 | ⊦ is_obj(r, class, st) → (st[r -- _type] ≠ typeval(mkclasstype(class)) ↔ false) | A User Theorem |
| isobj-type-04 | ⊦ is_obj(r, class, st) → (st[r -- _type] .type ≠ mkclasstype(class) ↔ false) | A User Theorem |
| isobj-type-05 | ⊦ ¬ r -- _type ∈ st → ¬ is_obj(r, st) | A User Theorem |
| isobj-type-06 | ⊦ ¬ is_typevalue(st[r -- _type]) → ¬ is_obj(r, st) | A User Theorem |
| isobj-type-07 | ⊦ st[r -- _type] .type = mkarraytype(ty) → ¬ is_obj(r, st) | A User Theorem |
| isobj-type-08 | ⊦ is_obj(r, st) → st[r -- _type] .type .jtelemtype = st[r -- _type] .type | A User Theorem |
| isobj-typeex | ⊦ ¬ type∃(str, st[r -- _type] .type) ∧ is_obj(r, class, st) → st[r -- _type] = typeval(mkclasstype(class)) | A User Theorem |
| isobj-typein | ⊦ ¬ r -- _type ∈ st → ¬ is_obj(r, class, st) | A User Theorem |
| isobj-typele | ⊦ is_obj(r, class, st) → st[r -- _type] .type ≤ mkclasstype(class) | A User Theorem |
| isobj-union | ⊦ ¬ r ∈ st .refs → (is_obj(r, class, sks, st ∪ st0) ↔ is_obj(r, class, sks, st0)) | A User Theorem |
| isobj-union-01 | ⊦ is_obj(r, st) → is_obj(r, st0 ∪ st) | A User Theorem |
| isobj-union-disjoint | ⊦ st1 .refs ∩ st .refs = ∅ ∧ r ∈ st1 ∧ is_obj(r, st1) → is_obj(r, st1 ∪ st) | A User Theorem |
| isobj-update | ⊦ r ≠ r0 → (is_obj(r, update(r0, fis, st)) ↔ is_obj(r, st)) | A User Theorem |
| isobj-update-01 | ⊦ r ≠ r0 → (is_obj(r, class, update(r0, fis, st)) ↔ is_obj(r, class, st)) | A User Theorem |
| isobj-void | ⊦ st[r -- _type] = typeval(void_type) ∧ r ≠ jvmref → ¬ is_obj(r, st) | A User Theorem |
| isvalidref-array | ⊦ okreftype(refval(r), mkarraytype(ty), st) → (is_valid_ref(r, st) ↔ is_array(r, st)) | A User Theorem |
| isvalidref-put-array-badindex | ⊦ i < 0 → (is_valid_ref(str, r0, st[r -- i ', val]) ↔ is_valid_ref(str, r0, st)) | A User Theorem |
| mode-addobj | ⊦ r ≠ jvmref → (_mode ∈ addobj(r, class1, fis, st) ↔ _mode ∈ st) | A User Theorem |
| new-add | ⊦ newref(r, addobj(r0, class1, fis, st)) ↔ r ≠ r0 ∧ newref(r, st) | A User Theorem |
| newref-addobj | ⊦ newref(addobj(r, class, fis, st)) ≠ r | A User Theorem |
| newref-addobj-in | ⊦ r ∈ st → newref(addobj(r, class, fis, st)) = newref(st) | A User Theorem |
| nouninit-addclass | ⊦ nouninit(claset, st) ∧ class ≠ `java.lang.Object' .class ∧ ¬ mkfs(class, void_type, `initstate' .field) ' ∈ fis → nouninit(claset, addclass(class, fis, st)) | A User Theorem |
| nouninit-addobj | ⊦ newref(r, st) → (nouninit(claset, addobj(r, class, fis, st)) ↔ nouninit(claset, st)) | A User Theorem |
| okarray-addobj | ⊦ r ≠ r0 → (okarray(r, int_type, addobj(r0, class1, fis, st)) ↔ okarray(r, int_type, st)) | A User Theorem |
| okfieldinits-abstract | ⊦ okfieldinits(class, fis) → ¬ mkfs(class, abstract_type, fieldvar) ' ∈ fis | A User Theorem |
| okfieldinits-at | ⊦ okfieldinits(class0, fis) ∧ mkfs(class, ty, fieldvar) ' ∈ fis → fis[mkfs(class, ty, fieldvar) '] = initial_value(ty) | A User Theorem |
| okfieldinits-class | ⊦ class ≠ class0 ∧ okfieldinits(class0, fis) → ¬ mkfs(class, ty, fieldvar) ' ∈ fis .keys | A User Theorem |
| okfieldinits-index | ⊦ okfieldinits(class, fis) ∧ sk ∈ fis .keys → ¬ is_indexkey(sk) | A User Theorem |
| okfieldinits-one | ⊦ okfieldinits(class, (sk × val) ') ↔ is_fskey(sk) ∧ val = initial_value(sk .fs .type) ∧ sk .fs .class = class ∧ sk .fs .type ≠ abstract_type | A User Theorem |
| refcount-addobj | ⊦ # addobj(newref(st), class, fis, st) .refs = # st .refs + 1 | A User Theorem |
| reffield-del | ⊦ r0 ≠ r → (has_reffield(r0, st -- r) ↔ has_reffield(r0, st)) | A User Theorem |
| reffield-null | ⊦ ¬ has_reffield(jvmref, st) | A User Theorem |
| statfields-index-01 | ⊦ is_indexkey(sk) → ¬ sk ∈ statfields(class) | A User Theorem |
| statfields-same-class-01 | ⊦ class ≠ class0 → ¬ mkfs(class0, ty, fieldvar) ' ∈ statfields(class) | A User Theorem |
| stsubset-addobj | ⊦ newref(r, st) → (st ⊆ addobj(r, class1, fis, st0) ↔ st ⊆ st0) | A User Theorem |
| valid-type-typeval | ⊦ st[r -- _type] .type = ty ∧ is_valid_ref(r, st) → st[r -- _type] = typeval(ty) | A User Theorem |
| validFields-addobj | ⊦ r ≠ r0 → (validFields(r, fis, addobj(r0, class, fis0, st)) ↔ validFields(r, fis, st)) | A User Theorem |
| validfieldinits-empty | ⊦ validfieldinits([], st) | A User Theorem |
| validfieldinits-one | ⊦ validfieldinits((sk × val) ', st) ↔ is_fskey(sk) ∧ oktype(val, sk .fs .type, st) ∧ ( is_referencevalue(val) → val .refval = jvmref ∨ val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ st[val .refval -- _type] .type ≤ sk .fs .type) | A User Theorem |
| validfieldinits-one-01 | ⊦ validfieldinits((mkfs(class, mkclasstype(class0), fieldvar) ' × refval(r)) ', st) ↔ r = jvmref ∨ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ st[r -- _type] .type ≤ mkclasstype(class0) | A User Theorem |
| validfieldinits-one-02 | ⊦ validfieldinits((mkfs(class, mkarraytype(ty), fieldvar) ' × refval(r)) ', st) ↔ r = jvmref ∨ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ st[r -- _type] .type ≤ mkarraytype(ty) | A User Theorem |
| validfieldinits-rec | ⊦ validfieldinits((sk × val) ' + fis, st) ↔ is_fskey(sk) ∧ oktype(val, sk .fs .type, st) ∧ ( is_referencevalue(val) → val .refval = jvmref ∨ val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ st[val .refval -- _type] .type ≤ sk .fs .type) ∧ validfieldinits(fis, st) | A User Theorem |
| validref | ⊦ ¬ is_obj(r, st) → (is_valid_ref(r, st) ↔ is_array(r, st)) | A User Theorem |
| validref-01 | ⊦ ¬ is_array(r, st) → (is_valid_ref(r, st) ↔ is_obj(r, st)) | A User Theorem |
| validref-02 | ⊦ is_obj(r, class, st) → is_valid_ref(r, st) | A User Theorem |
| validref-addobj | ⊦ r ≠ r0 → (is_valid_ref(r, addobj(r0, class, fis, st)) ↔ is_valid_ref(r, st)) | A User Theorem |
| validref-addobj-01 | ⊦ ¬ _type ∈ fis → (is_valid_ref(r, addobj(r, class, fis, st)) ↔ is_obj(r, addobj(r, class, fis, st))) | A User Theorem |
| validref-del | ⊦ ¬ is_valid_ref(r, st -- r) | A User Theorem |
| validref-del-01 | ⊦ r ≠ r0 → (is_valid_ref(r, st -- r0) ↔ is_valid_ref(r, st)) | A User Theorem |
| validref-isarray | ⊦ is_array(r, st) → is_valid_ref(r, st) | A User Theorem |
| validref-isobj | ⊦ is_obj(r, st) → is_valid_ref(r, st) | A User Theorem |
| validref-new | ⊦ newref(r, st) → ¬ is_valid_ref(r, st) | A User Theorem |
| validref-notin | ⊦ ¬ r ∈ st → ¬ is_valid_ref(r, st) | A User Theorem |
| validref-notin-01 | ⊦ ¬ r -- _type ∈ st → ¬ is_valid_ref(r, st) | A User Theorem |
| validref-notin-02 | ⊦ ¬ r ∈ st .refs → ¬ is_valid_ref(r, st) | A User Theorem |
| validref-null | ⊦ ¬ is_valid_ref(jvmref, st) | A User Theorem |
| validref-okreftype | ⊦ okreftype(refval(r), mkclasstype(class), st) ∧ class ≠ `java.lang.Object' .class ∧ r ≠ jvmref → (is_valid_ref(r, st) ↔ is_obj(r, st)) | A User Theorem |
| validref-primtype | ⊦ is_valid_ref(r, st) → st[r -- _type] .type ≠ byte_type | A User Theorem |
| validref-primtype-01 | ⊦ is_valid_ref(r, st) → st[r -- _type] .type ≠ short_type | A User Theorem |
| validref-primtype-02 | ⊦ is_valid_ref(r, st) → st[r -- _type] .type ≠ int_type | A User Theorem |
| validref-put | ⊦ oktype(val, ty, st) ∧ is_valid_ref(r, st) ∧ ty ≠ void_type ∧ mkfs(class, ty, fieldvar) ' ≠ _length → is_valid_ref(r, st[r1 -- mkfs(class, ty, fieldvar) ', val]) | A User Theorem |
| validref-put-01 | ⊦ r ≠ r0 → (is_valid_ref(r0, st[r -- sk, val]) ↔ is_valid_ref(r0, st)) | A User Theorem |
| validref-put-samefield | ⊦ r -- fs ' ∈ st ∧ oktype(st[r -- fs '], fs .type, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _length ∧ fs ' ≠ _type → (is_valid_ref(r, st[r -- fs ', val]) ↔ is_valid_ref(r, st)) | A User Theorem |
| validref-put-samefield-01 | ⊦ is_valid_ref(r, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _length ∧ fs ' ≠ _type → is_valid_ref(r, st[r -- fs ', val]) | A User Theorem |
| validref-reftype | ⊦ ¬ is_reftype(st[r -- _type] .type) → ¬ is_valid_ref(r, st) | A User Theorem |
| validref-typeval | ⊦ ¬ is_typevalue(st[r -- _type]) → ¬ is_valid_ref(r, st) | A User Theorem |