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: |
|---|---|---|
| validrefset-empty | ⊦ ¬ is_valid_ref(str, r, st) → validrefset(str, r, st) = ∅ | An Axiom |
| validrefset-def | ⊦ is_valid_ref(str, r, st) → ( refs ∈ validrefset(str, r, st) ↔ refs ≠ [] ∧ refs .first = r ∧ ¬ has_reffield(refs .last, st) ∧ ¬ dups(refs) ∧ validrefs(str, refs, st[r -- _type] .type, st)) | An Axiom |
| maxpath-zero | ⊦ validrefset(str, r, st) = ∅ → maxpath(str, r, st) = 0 | An Axiom |
| maxpath-in | ⊦ validrefset(str, r, st) ≠ ∅ → (∃ refs. refs ∈ validrefset(str, r, st) ∧ maxpath(str, r, st) = # refs) | An Axiom |
| maxpath-max | ⊦ refs ∈ validrefset(str, r, st) → # refs ≤ maxpath(str, r, st) | An Axiom |
| pseq-def | ⊦ ps=(r, st, r1, st1) ↔ r = jvmref ∧ r1 = jvmref ∨ r ≠ jvmref ∧ r1 ≠ jvmref ∧ st[r -- _type] = st1[r1 -- _type] ∧ ( is_classtype(st[r -- _type] .type) → (∀ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) → ps=(st[r -- fs '] .refval, st, st1[r1 -- fs '] .refval, st1)) ∧ (∀ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ ¬ is_referencevalue(st[r -- fs ']) → st[r -- fs '] = st1[r1 -- fs '])) ∧ ( is_arraytype(st[r -- _type] .type) → st[r -- _length] .intval = st1[r1 -- _length] .intval ∧ (∀ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) → ps=(st[r -- i '] .refval, st, st1[r1 -- i '] .refval, st1)) ∧ (∀ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ ¬ is_referencevalue(st[r -- i ']) → st[r -- i '] = st1[r1 -- i '])) | An Axiom |
| unchanged-def | ⊦ unchanged(str, r, st, st0) ↔ (∀ r0. (path∃(str, r, r0, st) ↔ path∃(str, r, r0, st0)) ∧ (path∃(str, r, r0, st) → unchangedNorec(r0, st, st0))) | An Axiom |
| unchangedNorec-def | ⊦ unchangedNorec(r, st, st0) ↔ r = jvmref ∨ r ≠ jvmref ∧ st[r -- _type] = st0[r -- _type] ∧ (is_classtype(st[r -- _type] .type) → (∀ fs. fs ' ∈ instfields(st[r -- _type] .type .class) → st[r -- fs '] = st0[r -- fs '])) ∧ ( is_arraytype(st[r -- _type] .type) → st[r -- _length] = st0[r -- _length] ∧ (∀ i. 0 ≤ i ∧ i < st[r -- _length] .intval → st[r -- i '] = st0[r -- i '])) | An Axiom |
| cyclic-pseq | ⊦ ps=(r, st, r1, st1) ∧ ¬ junkref(str, r, st) ∧ ¬ junkref(str, r1, st1) ∧ ¬ cyclic(str, r1, st1) → ¬ cyclic(str, r, st) | A User Theorem |
| getbytearray-pseq | ⊦ ps=(r, st, r1, st1) ∧ r ≠ jvmref ∧ validref(`docs2store', r, mkarraytype(byte_type), st) → getbytearray(r, st) = getbytearray(r1, st1) | A User Theorem |
| getbytearray-pseq-02 | ⊦ validref(`docs2store', r, mkarraytype(byte_type), st) ∧ ps=(r, st, r1, st1) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ i + i1 ≤ st[r -- _length] .intval ∧ 0 ≤ i1 ∧ r ≠ jvmref → getbytearray(r, i, i1, st) = getbytearray(r1, i, i1, st1) | A User Theorem |
| getbytearray-pseq-nojunk | ⊦ ps=(r, st, r1, st1) ∧ r ≠ jvmref ∧ ¬ junkref(`docs2store', r, st) ∧ st[r -- _type] .type = mkarraytype(byte_type) → getbytearray(r, st) = getbytearray(r1, st1) | A User Theorem |
| getbytearray-pseq-nojunk-02 | ⊦ ¬ junkref(`docs2store', r, st) ∧ st[r -- _type] .type = mkarraytype(byte_type) ∧ ps=(r, st, r1, st1) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ i + i1 ≤ st[r -- _length] .intval ∧ 0 ≤ i1 ∧ r ≠ jvmref → getbytearray(r, i, i1, st) = getbytearray(r1, i, i1, st1) | A User Theorem |
| maxpath-array | ⊦ is_array(str, r, st) ∧ st[r -- i '] = refval(r0) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ ¬ junkref(str, r, st) ∧ ¬ cyclic(str, r, st) → ¬ maxpath(str, r, st) ≤ maxpath(str, r0, st) | A User Theorem |
| maxpath-array-ls | ⊦ is_array(str, r, st) ∧ st[r -- i '] = refval(r0) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ ¬ junkref(str, r, st) ∧ ¬ cyclic(str, r, st) → ¬ maxpath(str, r, st) < maxpath(str, r0, st) | A User Theorem |
| maxpath-object | ⊦ is_obj(str, r, st) ∧ st[r -- fs '] = refval(r0) ∧ fs ' ∈ instfields(st[r -- _type] .type .class) ∧ ¬ junkref(str, r, st) ∧ ¬ cyclic(str, r, st) → ¬ maxpath(str, r, st) ≤ maxpath(str, r0, st) | A User Theorem |
| pseq-jvmref | ⊦ ps=(jvmref, st, jvmref, st0) | A User Theorem |
| pseq-subset | ⊦ ¬ junkref(str, r, st) ∧ ¬ cyclic(str, r, st) ∧ ¬ junkref(str, r1, st1) ∧ ¬ cyclic(str, r1, st1) ∧ ps=(r, st, r1, st1) ∧ st ⊆ st2 → ps=(r, st2, r1, st1) | A User Theorem |
| pseq-subset-01 | ⊦ ¬ junkref(str, r, st) ∧ ¬ cyclic(str, r, st) ∧ ¬ junkref(str, r1, st1) ∧ ¬ cyclic(str, r1, st1) ∧ ps=(r, st, r1, st1) ∧ st1 ⊆ st2 → ps=(r, st, r1, st2) | A User Theorem |
| pseq-sym | ⊦ ¬ cyclic(str, r, st) ∧ ¬ cyclic(str, r1, st1) ∧ ¬ junkref(str, r, st) ∧ ¬ junkref(str, r1, st1) → (ps=(r, st, r1, st1) ↔ ps=(r1, st1, r, st)) | A User Theorem |
| pseq-sym-01 | ⊦ ¬ cyclic(str, r, st) ∧ ¬ cyclic(str, r1, st1) ∧ ¬ junkref(str, r, st) ∧ ¬ junkref(str, r1, st1) → (ps=(r, st, r1, st1) → ps=(r1, st1, r, st)) | A User Theorem |
| unchNorec-def-keep | ⊦ ¬ ( st[r -- _type] = st0[r -- _type] ∧ (is_classtype(st[r -- _type] .type) → (∀ fs. fs ' ∈ instfields(st[r -- _type] .type .class) → st[r -- fs '] = st0[r -- fs '])) ∧ ( is_arraytype(st[r -- _type] .type) → st[r -- _length] = st0[r -- _length] ∧ (∀ i. 0 ≤ i ∧ i < st[r -- _length] .intval → st[r -- i '] = st0[r -- i ']))) ∧ r ≠ jvmref → ¬ unchangedNorec(r, st, st0) | A User Theorem |
| unchNorec-field | ⊦ unchangedNorec(r, st, st0) ∧ fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_classtype(st[r -- _type] .type) ∧ r ≠ jvmref → st[r -- fs '] = st0[r -- fs '] | A User Theorem |
| unchNorec-field0 | ⊦ unchangedNorec(r, st, st0) ∧ fs ' ∈ instfields(st0[r -- _type] .type .class) ∧ is_classtype(st0[r -- _type] .type) ∧ r ≠ jvmref → st0[r -- fs '] = st[r -- fs '] | A User Theorem |
| unchNorec-index | ⊦ unchangedNorec(r, st, st0) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_arraytype(st[r -- _type] .type) ∧ r ≠ jvmref → st[r -- i '] = st0[r -- i '] | A User Theorem |
| unchNorec-index0 | ⊦ unchangedNorec(r, st, st0) ∧ 0 ≤ i ∧ i < st0[r -- _length] .intval ∧ is_arraytype(st0[r -- _type] .type) ∧ r ≠ jvmref → st0[r -- i '] = st[r -- i '] | A User Theorem |
| unchNorec-isarray | ⊦ unchangedNorec(r, st, st0) ∧ is_array(r, st) → (¬ is_array(r, st0) ↔ false) | A User Theorem |
| unchNorec-isarray-01 | ⊦ unchangedNorec(r, st, st0) ∧ is_array(str, r, st) → (¬ is_array(str, r, st0) ↔ false) | A User Theorem |
| unchNorec-isarray-02 | ⊦ unchangedNorec(r, st, st0) ∧ is_array(str, r, st0) → (¬ is_array(str, r, st) ↔ false) | A User Theorem |
| unchNorec-isobj | ⊦ unchangedNorec(r, st, st0) ∧ is_obj(r, st) → (¬ is_obj(r, st0) ↔ false) | A User Theorem |
| unchNorec-isobj-01 | ⊦ unchangedNorec(r, st, st0) ∧ is_obj(str, r, st) → (¬ is_obj(str, r, st0) ↔ false) | A User Theorem |
| unchNorec-isobj-02 | ⊦ unchangedNorec(r, st, st0) ∧ is_obj(str, r, st0) → (¬ is_obj(str, r, st) ↔ false) | A User Theorem |
| unchNorec-isvalidref | ⊦ unchangedNorec(r, st, st0) ∧ is_valid_ref(str, r, st) → (¬ is_valid_ref(str, r, st0) ↔ false) | A User Theorem |
| unchNorec-isvalidref-01 | ⊦ unchangedNorec(r, st, st0) ∧ is_valid_ref(str, r, st0) → (¬ is_valid_ref(str, r, st) ↔ false) | A User Theorem |
| unchNorec-junkrefs | ⊦ junkrefs(str, refs, ty, st) ∧ (∀ r. r ∈ refs → unchangedNorec(r, st, st0)) → junkrefs(str, refs, ty, st0) | A User Theorem |
| unchNorec-junkrefs-equiv | ⊦ (∀ r. r ∈ refs → unchangedNorec(r, st, st0)) → (junkrefs(str, refs, ty, st) ↔ junkrefs(str, refs, ty, st0)) | A User Theorem |
| unchNorec-length | ⊦ unchangedNorec(r, st, st0) ∧ is_arraytype(st[r -- _type] .type) ∧ r ≠ jvmref → st[r -- _length] = st0[r -- _length] | A User Theorem |
| unchNorec-length-intro | ⊦ r ≠ jvmref ∧ st[r -- _length] ≠ st0[r -- _length] ∧ is_arraytype(st[r -- _type] .type) → ¬ unchangedNorec(r, st, st0) | A User Theorem |
| unchNorec-length0 | ⊦ unchangedNorec(r, st, st0) ∧ is_arraytype(st[r -- _type] .type) ∧ r ≠ jvmref → st0[r -- _length] = st[r -- _length] | A User Theorem |
| unchNorec-null | ⊦ unchangedNorec(jvmref, st, st0) | A User Theorem |
| unchNorec-put-nopathex | ⊦ ¬ path∃(str, r, r0, st) ∧ ¬ junkref(str, r, st) ∧ sk ≠ _type → unchangedNorec(r, st, st[r0 -- sk, val]) | A User Theorem |
| unchNorec-reflexivity | ⊦ unchangedNorec(r, st, st) | A User Theorem |
| unchNorec-sym | ⊦ unchangedNorec(r, st, st0) ↔ unchangedNorec(r, st0, st) | A User Theorem |
| unchNorec-transitivity | ⊦ unchangedNorec(r, st, st0) ∧ unchangedNorec(r, st0, st1) → unchangedNorec(r, st, st1) | A User Theorem |
| unchNorec-type | ⊦ unchangedNorec(r, st, st0) ∧ r ≠ jvmref → st[r -- _type] = st0[r -- _type] | A User Theorem |
| unchNorec-type-intro | ⊦ r ≠ jvmref ∧ st[r -- _type] ≠ st0[r -- _type] → ¬ unchangedNorec(r, st, st0) | A User Theorem |
| unchNorec-type0 | ⊦ unchangedNorec(r, st, st0) ∧ r ≠ jvmref → st0[r -- _type] = st[r -- _type] | A User Theorem |
| unchNorec-validrefs | ⊦ validrefs(str, refs, ty, st) ∧ (∀ r. r ∈ refs → unchangedNorec(r, st, st0)) → validrefs(str, refs, ty, st0) | A User Theorem |
| unchNorec-validrefs-equiv | ⊦ (∀ r. r ∈ refs → unchangedNorec(r, st, st0)) → (validrefs(str, refs, ty, st) ↔ validrefs(str, refs, ty, st0)) | A User Theorem |
| unchNorec-validrefs-pathex | ⊦ validrefs(str, refs, ty, st) ∧ r = refs .first ∧ r0 ∈ refs ∧ (∀ r. r ∈ refs → unchangedNorec(r, st, st0)) ∧ refs ≠ [] → path∃(str, r, r0, st0) | A User Theorem |
| unchanged-array-forward | ⊦ unchanged(str, r, st, st1) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_array(str, r, st) ∧ is_referencevalue(st[r -- i ']) ∧ r ≠ jvmref ∧ ( st[r -- i '] .refval ≠ jvmref → st[st[r -- i '] .refval -- _type] .type ≤ st[r -- _type] .type .type ∧ is_valid_ref(str, st[r -- i '] .refval, st)) → unchanged(str, st[r -- i '] .refval, st, st1) | A User Theorem |
| unchanged-class-forward | ⊦ unchanged(str, r, st, st1) ∧ sk ∈ instfields(st[r -- _type] .type .class) ∧ is_obj(str, r, st) ∧ is_referencevalue(st[r -- sk]) ∧ r ≠ jvmref ∧ (st[r -- sk] .refval ≠ jvmref → st[st[r -- sk] .refval -- _type] .type ≤ sk .fs .type ∧ is_valid_ref(str, st[r -- sk] .refval, st)) → unchanged(str, st[r -- sk] .refval, st, st1) | A User Theorem |
| unchanged-cyclic | ⊦ unchanged(str, r, st, st0) ∧ ¬ junkref(str, r, st) ∧ cyclic(str, r, st) → cyclic(str, r, st0) | A User Theorem |
| unchanged-cyclic-equiv | ⊦ unchanged(str, r, st, st0) ∧ ¬ junkref(str, r, st) → (cyclic(str, r, st) ↔ cyclic(str, r, st0)) | A User Theorem |
| unchanged-def-keep | ⊦ ¬ (∀ r0. (path∃(str, r, r0, st) ↔ path∃(str, r, r0, st0)) ∧ (path∃(str, r, r0, st) → unchangedNorec(r0, st, st0))) → ¬ unchanged(str, r, st, st0) | A User Theorem |
| unchanged-field-lookup | ⊦ unchanged(str, r, st, st1) ∧ sk ∈ instfields(st[r -- _type] .type .class) ∧ is_obj(str, r, st) ∧ r ≠ jvmref → st[r -- sk] = st1[r -- sk] | A User Theorem |
| unchanged-field-lookup-01 | ⊦ unchanged(str, r, st, st1) ∧ sk ∈ instfields(st[r -- _type] .type .class) ∧ is_obj(str, r, st) ∧ r ≠ jvmref → st1[r -- sk] = st[r -- sk] | A User Theorem |
| unchanged-getbar | ⊦ getbytearray(r, st) ≠ getbytearray(r, st0) ∧ okbytearray(r, st) → ¬ unchanged(str, r, st, st0) | A User Theorem |
| unchanged-isarray | ⊦ unchanged(str, r, st, st1) ∧ is_array(str, r, st) → (¬ is_array(str, r, st1) ↔ false) | A User Theorem |
| unchanged-isobj | ⊦ unchanged(str, r, st, st1) ∧ is_obj(str, r, st) → (¬ is_obj(str, r, st1) ↔ false) | A User Theorem |
| unchanged-junkref | ⊦ ¬ junkref(str, r, st) ∧ unchanged(str, r, st, st1) → ¬ junkref(str, r, st1) | A User Theorem |
| unchanged-junkref-level | ⊦ unchanged(str0, r, st, st1) ∧ junkref(str, r, st) ∧ level⊆(str, str0) → junkref(str, r, st1) | A User Theorem |
| unchanged-junkrefs | ⊦ unchanged(str, refs .first, st, st1) ∧ ¬ junkrefs(str, refs, ty, st) → ¬ junkrefs(str, refs, ty, st1) | A User Theorem |
| unchanged-junkrefs-level | ⊦ unchanged(str0, refs .first, st, st1) ∧ junkrefs(str, refs, ty, st) ∧ level⊆(str, str0) → junkrefs(str, refs, ty, st1) | A User Theorem |
| unchanged-levelsubset | ⊦ unchanged(str, r, st, st0) ∧ ¬ junkref(str, r, st) ∧ level⊆(str, str0) → unchanged(str0, r, st, st0) | A User Theorem |
| unchanged-levelsubset-equiv | ⊦ ¬ junkref(str, r, st) ∧ level⊆(str, str0) → (unchanged(str, r, st, st0) ↔ unchanged(str0, r, st, st0)) | A User Theorem |
| unchanged-lookup-generic | ⊦ unchanged(str, r, st, st0) ∧ path∃(str, r, r0, st) ∧ r0 ≠ jvmref ∧ (is_classtype(st[r0 -- _type] .type) → sk ∈ instfields(st[r0 -- _type] .type .class)) ∧ (is_arraytype(st[r0 -- _type] .type) → sk = _length ∨ is_indexkey(sk) ∧ 0 ≤ sk .index ∧ sk .index < st[r0 -- _length] .intval) → st[r0 -- sk] = st0[r0 -- sk] | A User Theorem |
| unchanged-null | ⊦ unchanged(str, jvmref, st, st0) | A User Theorem |
| unchanged-okbar | ⊦ unchanged(str, r, st, st0) ∧ path∃(str, r, r1, st) ∧ okbytearray(r1, st) → okbytearray(r1, st0) | A User Theorem |
| unchanged-pathex | ⊦ unchanged(str, r, st, st1) ∧ path∃(str, r, r0, st) → path∃(str, r, r0, st1) | A User Theorem |
| unchanged-pathex-append | ⊦ unchanged(str, r, st, st1) ∧ path∃(str, r, r0, st) ∧ path∃(str, r0, r1, st) → path∃(str, r0, r1, st1) | A User Theorem |
| unchanged-pathex-unchNorec | ⊦ unchanged(str, r, st, st0) ∧ path∃(str, r, r0, st) → unchangedNorec(r0, st, st0) | A User Theorem |
| unchanged-pathex-unchanged | ⊦ unchanged(str, r, st, st1) ∧ path∃(str, r, r0, st) → unchanged(str, r0, st, st1) | A User Theorem |
| unchanged-put-nopathex | ⊦ ¬ path∃(str, r, r0, st) ∧ ¬ junkref(str, r, st) ∧ sk ≠ _type → unchanged(str, r, st, st[r0 -- sk, val]) | A User Theorem |
| unchanged-rec-generic | ⊦ unchanged(str, r, st, st0) ∧ ¬ junkref(str, r, st) ∧ r ≠ jvmref ∧ is_referencevalue(st[r -- sk]) ∧ (is_classtype(st[r -- _type] .type) → sk ∈ instfields(st[r -- _type] .type .class)) ∧ (is_arraytype(st[r -- _type] .type) → is_indexkey(sk) ∧ 0 ≤ sk .index ∧ sk .index < st[r -- _length] .intval) → unchanged(str, st[r -- sk] .refval, st, st0) | A User Theorem |
| unchanged-symmetric | ⊦ unchanged(str, r, st, st1) ↔ unchanged(str, r, st1, st) | A User Theorem |
| unchanged-type | ⊦ unchanged(str, r, st, st1) ∧ is_valid_ref(str, r, st) ∧ r ≠ jvmref → st[r -- _type] = st1[r -- _type] | A User Theorem |
| unchanged-type-01 | ⊦ unchanged(str, r, st, st1) ∧ is_valid_ref(str, r, st) ∧ r ≠ jvmref → st1[r -- _type] = st[r -- _type] | A User Theorem |
| unchanged-type-in | ⊦ ¬ r -- _type ∈ st1 ∧ is_obj(str, r, st) → ¬ unchanged(str, r, st, st1) | A User Theorem |
| unchanged-unchNorec-same | ⊦ ¬ unchangedNorec(r, st, st0) ∧ is_obj(str, r, st) → ¬ unchanged(str, r, st, st0) | A User Theorem |
| unchanged-unchNorec-same-01 | ⊦ ¬ unchangedNorec(r, st, st0) ∧ is_valid_ref(str, r, st) → ¬ unchanged(str, r, st, st0) | A User Theorem |
| unchanged-validref | ⊦ validref(str, r, ty, st) ∧ unchanged(str, r, st, st1) → validref(str, r, ty, st1) | A User Theorem |
| unchanged-validrefs-unchNorec | ⊦ unchanged(str, refs .first, st, st0) ∧ validrefs(str, refs, ty, st) ∧ r0 ∈ refs → unchangedNorec(r0, st, st0) | A User Theorem |
| validref-pseq | ⊦ validref(`docs2store', r1, ty, st1) ∧ ps=(r, st, r1, st1) ∧ ¬ junkref(`docs2store', r, st) → validref(`docs2store', r, ty, st) | A User Theorem |