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: |
|---|---|---|
| irref | ⊦ ¬ rk < rk | An Axiom |
| trans | ⊦ rk < rk0 ∧ rk0 < rk1 → rk < rk1 | An Axiom |
| total | ⊦ rk < rk0 ∨ rk = rk0 ∨ rk0 < rk | An Axiom |
| out | ⊦ _out = jvmref -- mkfs(`java.lang.Object' .class, void_type, `out' .field) ' | An Axiom |
| type | ⊦ _type = mkfs(`java.lang.Object' .class, void_type, `type' .field) ' | An Axiom |
| mode | ⊦ _mode = jvmref -- mkfs(`java.lang.Object' .class, void_type, `mode' .field) ' | An Axiom |
| length | ⊦ _length = mkfs(`*Array*' .class, int_type, `length' .field) ' | An Axiom |
| uninit | ⊦ _uninit = jvmref -- mkfs(`java.lang.Object' .class, void_type, `uninit' .field) ' | An Axiom |
| initfield | ⊦ _initfield = `initstate' .field | An Axiom |
| endfinallymode | ⊦ _endfinallymode = jvmref -- mkfs(`java.lang.Object' .class, void_type, `endfinallymode' .field) ' | An Axiom |
| diff | ⊦ _out ≠ _mode | A User Theorem |
| diff-01 | ⊦ r -- _type ≠ _mode | A User Theorem |
| diff-02 | ⊦ r -- _type ≠ _out | A User Theorem |
| diff-03 | ⊦ _uninit ≠ _mode | A User Theorem |
| diff-04 | ⊦ _uninit ≠ _out | A User Theorem |
| diff-05 | ⊦ r -- _type ≠ _uninit | A User Theorem |
| diff-06 | ⊦ r -- _length ≠ _uninit | A User Theorem |
| diff-07 | ⊦ r -- i ' ≠ _uninit | A User Theorem |
| endfin-diff | ⊦ _endfinallymode ≠ _out | A User Theorem |
| endfin-diff-01 | ⊦ _endfinallymode ≠ _mode | A User Theorem |
| endfin-diff-02 | ⊦ _endfinallymode ≠ _uninit | A User Theorem |
| endfin-eq | ⊦ _endfinallymode = r -- sk ↔ ¬ ¬ (r = jvmref ∧ sk = mkfs(`java.lang.Object' .class, void_type, `endfinallymode' .field) ') | A User Theorem |
| endfin-key | ⊦ _endfinallymode .key = mkfs(`java.lang.Object' .class, void_type, `endfinallymode' .field) ' | A User Theorem |
| endfin-ref | ⊦ _endfinallymode .ref = jvmref | A User Theorem |
| initfield-01 | ⊦ fieldvar = _initfield ↔ fieldvar .field = `initstate' | A User Theorem |
| len | ⊦ _length ≠ i ' | A User Theorem |
| length-01 | ⊦ mkfs(class1, ty, `initstate' .field) ' ≠ _length | A User Theorem |
| length-02 | ⊦ mkfs(class1, ty, fieldvar) ' = _length → class1 = `*Array*' .class ∧ ty = int_type ∧ fieldvar = `length' .field | A User Theorem |
| length-03 | ⊦ mkfs(`*Array*' .class, int_type, `length' .field) ' = _length | A User Theorem |
| length-04 | ⊦ is_fskey(_length) | A User Theorem |
| length-05 | ⊦ mkfs(class, mkclasstype(class0), fieldvar) ' ≠ _length | A User Theorem |
| length-diff | ⊦ _length ≠ mkfs(class, short_type, fieldvar) ' | A User Theorem |
| mode-01 | ⊦ jvmref -- mkfs(`java.lang.Object' .class, void_type, `mode' .field) ' = _mode | A User Theorem |
| mode-02 | ⊦ _mode = jvmref -- sk ↔ sk = mkfs(`java.lang.Object' .class, void_type, `mode' .field) ' | A User Theorem |
| mode-03 | ⊦ _mode = r -- sk → r = jvmref | A User Theorem |
| mode-04 | ⊦ _mode ≠ r -- i ' | A User Theorem |
| mode-05 | ⊦ _mode ≠ r -- _length | A User Theorem |
| mode-06 | ⊦ r ≠ jvmref → _mode ≠ r -- sk | A User Theorem |
| mode-key | ⊦ _mode .key = mkfs(`java.lang.Object' .class, void_type, `mode' .field) ' | A User Theorem |
| mode-neq | ⊦ ty ≠ void_type → _mode ≠ r -- mkfs(class, ty, fieldvar) ' | A User Theorem |
| mode-ref | ⊦ _mode .ref = jvmref | A User Theorem |
| out-01 | ⊦ jvmref -- mkfs(`java.lang.Object' .class, void_type, `out' .field) ' = _out | A User Theorem |
| out-02 | ⊦ r ≠ jvmref → r -- sk ≠ _out | A User Theorem |
| out-03 | ⊦ _out = jvmref -- sk ↔ sk = mkfs(`java.lang.Object' .class, void_type, `out' .field) ' | A User Theorem |
| out-04 | ⊦ _out ≠ r -- i ' | A User Theorem |
| out-05 | ⊦ _out ≠ r -- _length | A User Theorem |
| th-01 | class1 ≠ `java.lang.Object' .class ⊦ _mode ≠ r -- mkfs(class1, ty, fieldvar) ' | A User Theorem |
| type-01 | ⊦ mkfs(`java.lang.Object' .class, void_type, `type' .field) ' = _type | A User Theorem |
| type-02 | ⊦ _type = mkfs(class1, ty, fieldvar) ' ↔ ¬ ¬ (class1 = `java.lang.Object' .class ∧ ty = void_type ∧ fieldvar = `type' .field) | A User Theorem |
| type-03 | ⊦ _type ≠ i ' | A User Theorem |
| type-04 | ⊦ _type ≠ _length | A User Theorem |
| type-05 | ⊦ _type = mkfs(class1, ty, fieldvar) ' → class1 = `java.lang.Object' .class ∧ ty = void_type ∧ fieldvar = `type' .field | A User Theorem |
| type-06 | ⊦ is_fskey(_type) | A User Theorem |
| type-07 | ⊦ mkfs(class1, int_type, fieldvar) ' ≠ _type | A User Theorem |
| type-08 | ⊦ mkfs(class1, short_type, fieldvar) ' ≠ _type | A User Theorem |
| type-09 | ⊦ mkfs(class1, byte_type, fieldvar) ' ≠ _type | A User Theorem |
| type-10 | ⊦ mkfs(class1, boolean_type, fieldvar) ' ≠ _type | A User Theorem |
| type-11 | ⊦ mkfs(class1, mkclasstype(class0), fieldvar) ' ≠ _type | A User Theorem |
| type-12 | ⊦ mkfs(class1, mkarraytype(ty), fieldvar) ' ≠ _type | A User Theorem |
| type-fieldspec | ⊦ _type .fs = mkfs(`java.lang.Object' .class, void_type, `type' .field) | A User Theorem |
| type-neq | ⊦ ty ≠ void_type → mkfs(class, ty, fieldvar) ' ≠ _type | A User Theorem |
| uninit-01 | ⊦ r ≠ jvmref → r -- sk ≠ _uninit | A User Theorem |
| uninit-02 | ⊦ r -- fs ' = _uninit ↔ r = jvmref ∧ fs = mkfs(`java.lang.Object' .class, void_type, `uninit' .field) | A User Theorem |
| uninit-eq | ⊦ jvmref -- sk = _uninit ↔ sk = mkfs(`java.lang.Object' .class, void_type, `uninit' .field) ' | A User Theorem |