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: |
|---|---|---|
| array-compat | ⊦ compatarray(str, r, st) ↔ is_arraytype(st[r -- _type] .type) ∧ r -- _length ∈ st ∧ is_integervalue(st[r -- _length]) ∧ 0 ≤ st[r -- _length] .intval ∧ is_arrayref(r, st[r -- _length] .intval, st) ∧ (∀ j. 0 ≤ j ∧ j < st[r -- _length] .intval → compat(str, st[r -- j '], st[r -- _type] .type .type, st)) | An Axiom |
| store-compat | ⊦ compat(str, st) ↔ compatmode(str, st) ∧ compatstatic(str, st) ∧ compatrefs(str, st) | An Axiom |
| mode-compat | ⊦ compatmode(str, st) ↔ _mode ∈ st ∧ compatmode(str, st[_mode], st) | An Axiom |
| static-compat | ⊦ compatstatic(str, st) ↔ (∀ class. tdname∃(str, class) ∧ initdone(class, st) → compatfields(str, jvmref, statfields(class), st)) | An Axiom |
| refs-compat | ⊦ compatrefs(str, st) ↔ (∀ r. r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) → (is_classtype(st[r -- _type] .type) ∧ class+∃(str, st[r -- _type] .type .class) → compatobj(str, r, st)) ∧ ( is_arraytype(st[r -- _type] .type) ∧ (¬ has_classtype(st[r -- _type] .type) ∨ tdname+∃(str, st[r -- _type] .type .jtelemtype .class)) → compatarray(str, r, st))) | An Axiom |
| obj-compat | ⊦ compatobj(str, r, st) ↔ is_classtype(st[r -- _type] .type) ∧ class+∃(str, st[r -- _type] .type .class) ∧ compatfields(str, r, instfields(st[r -- _type] .type .class), st) | An Axiom |
| fields-compat | ⊦ compatfields(str, r, sks, st) ↔ (∀ sk. sk ∈ sks → r -- sk ∈ st ∧ is_fskey(sk) ∧ compat(str, st[r -- sk], sk .fs .type, st)) | An Axiom |
| value-compat | ⊦ compat(str, val, ty, st) ↔ okval(val, ty) ∧ ( is_referencevalue(val) ∧ val .refval ≠ jvmref → val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ is_reftype(st[val .refval -- _type] .type) ∧ (has_classtype(st[val .refval -- _type] .type) → tdname+∃(str, st[val .refval -- _type] .type .jtelemtype .class)) ∧ (is_classtype(st[val .refval -- _type] .type) → class+∃(str, st[val .refval -- _type] .type .class)) ∧ asgcomp(str, val, ty, st)) | An Axiom |
| params-compat | ⊦ compat(str, vts, st) ↔ (∀ vt. vt ∈ vts → compat(str, vt .val, vt .type, st)) | An Axiom |
| modeval-compat | ⊦ compatmode(str, val, st) ↔ val = noval ∨ is_break_mode(val) ∨ val = return(noval, void_type) ∨ is_return_mode(val) ∧ compat(str, val .val, val .type, st) ∨ is_throw_mode(val) ∧ val .refval ≠ jvmref ∧ compat(str, refval(val .refval), val .type, st) ∧ is_subtype(str, val .type, mkclasstype(`java.lang.Throwable' .class)) | An Axiom |
| acyclic-ref-def | ⊦ acyclic-ref(r, st) ↔ ⟪followRefs(r, st)⟫ true | An Axiom |
| cyclic-ref-def | ⊦ cyclic-ref(r, st) ↔ ¬ acyclic-ref(r, st) | An Axiom |
| okpath-rec-array | ⊦ typeval(ty) = st[r -- _type] ∧ is_arraytype(ty) → (okpath(r, st, r0 + refs) ↔ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ st[r -- i '] = refval(r0) ∧ okpath(r0, st, refs))) | An Axiom |
| okpath-rec | ⊦ typeval(ty) = st[r -- _type] ∧ is_classtype(ty) → (okpath(r, st, r0 + refs) ↔ (∃ fs. fs ' ∈ instfields(ty .class) ∧ st[r -- fs '] = refval(r0) ∧ okpath(r0, st, refs))) | An Axiom |
| okpath-empty | ⊦ okpath(r, st, []) | An Axiom |
| okpath-notin | ⊦ ¬ r1 ∈ st → ¬ okpath(r, st, r1 + refs) | An Axiom |
| decl | An Axiom | |
| compat-addclass | ⊦ fis .keys = statfields(class) ∧ okfieldinits(class, fis) ∧ compat(str, st) → compat(str, addclass(class, fis, st)) | A User Theorem |
| compat-addobj | ⊦ is_predefined_class(class) ∧ newref(r, st) ∧ compat(str, st) → compat(str, addobj(r, class, [], st)) | A User Theorem |
| compat-newref | ⊦ newref(r, st) → ¬ compat(str, refval(r), ty, st) | A User Theorem |
| compat-put | ⊦ compat(str, val, fs .type, st) ∧ compat(str, st) ∧ fs ' ≠ _length ∧ fs .type ≠ void_type → compat(str, st[r -- fs ', val]) | A User Theorem |
| compat-throw-02 | ⊦ compat(str, st) → ( compat(str, st[_mode, throw(r, mkclasstype(class))]) ↔ class ≤ `java.lang.Throwable' .class ∧ r ≠ jvmref ∧ compat(str, refval(r), mkclasstype(class), st)) | A User Theorem |
| compatarray-abstract | ⊦ compatarray(str, r, st) ∧ r ≠ jvmref ∧ st[r -- _type] .type = mkarraytype(abstract_type) → st[r -- _length] .intval = 0 | A User Theorem |
| compatarray-isarray | ⊦ ¬ is_array(r, st) ∧ r ≠ jvmref → ¬ compatarray(str, r, st) | A User Theorem |
| compatarray-isarray-01 | ⊦ is_array(r, st) ∧ (∀ i. 0 ≤ i ∧ i < st[r -- _length] .intval → compat(str, st[r -- i '], st[r -- _type] .type .type, st)) → compatarray(str, r, st) | A User Theorem |
| compatarray-mode | ⊦ r ≠ jvmref → (compatarray(str, r, st[_mode, val]) ↔ compatarray(str, r, st)) | A User Theorem |
| compatarray-void | ⊦ compatarray(str, r, st) ∧ r ≠ jvmref ∧ st[r -- _type] .type = mkarraytype(void_type) → (∀ i. 0 ≤ i ∧ i < st[r -- _length] .intval → st[r -- i '] = refval(jvmref)) | A User Theorem |
| compatfields-mode | ⊦ r ≠ jvmref → (compatfields(str, r, instfields(class), st[_mode, val]) ↔ compatfields(str, r, instfields(class), st)) | A User Theorem |
| compatobj-isobj | ⊦ ¬ is_obj(r, st) ∧ r ≠ jvmref → ¬ compatobj(str, r, st) | A User Theorem |
| compatobj-mode | ⊦ r ≠ jvmref → (compatobj(str, r, st[_mode, val]) ↔ compatobj(str, r, st)) | A User Theorem |
| compatrefs-mode | ⊦ compatrefs(str, st[_mode, val]) ↔ compatrefs(str, st) | A User Theorem |
| compatstatic-mode | ⊦ compatstatic(str, st[_mode, val]) ↔ compatstatic(str, st) | A User Theorem |
| compatval-addclass | ⊦ fis .keys = statfields(class) ∧ okfieldinits(class, fis) ∧ compat(str, val, ty, st) → compat(str, val, ty, addclass(class, fis, st)) | A User Theorem |
| compatval-noref | ⊦ ¬ is_referencevalue(val) → (compat(str, val, ty, st) ↔ okval(val, ty)) | A User Theorem |
| compatval-put | ⊦ compat(str, val, ty, st) ∧ fs .type ≠ void_type → compat(str, val, ty, st[r -- fs ', val0]) | A User Theorem |