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: |
|---|---|---|
| flatten-rec | ⊦ flatten(val ++ (val0 ++ val1)) = flatten(val ++ val0 ++ val1) | An Axiom |
| flatten-shift | ⊦ ¬ is_valuelist(val0) → flatten(val ++ val0) = flatten(val) ++ val0 | An Axiom |
| base | ⊦ ¬ is_valuelist(val) → flatten(val) = val | An Axiom |
| refp | ⊦ refp(val) ↔ is_referencevalue(val) ∧ val .refval ≠ jvmref | An Axiom |
| normal_mode | ⊦ is_normal_mode(val) ↔ val = noval | An Axiom |
| init_val_array | ⊦ initial_value(mkarraytype(ty)) = refval(jvmref) | An Axiom |
| init_val_class | ⊦ initial_value(mkclasstype(class1)) = refval(jvmref) | An Axiom |
| init_val_byte | ⊦ initial_value(byte_type) = byteval(0b) | An Axiom |
| init_val_short | ⊦ initial_value(short_type) = shortval(0s) | An Axiom |
| init_val_int | ⊦ initial_value(int_type) = intval(0) | An Axiom |
| init_val_bool | ⊦ initial_value(boolean_type) = boolval(false) | An Axiom |
| refin-throw | ⊦ r ∈ throw(r0, ty) ↔ r = r0 | An Axiom |
| refin-return | ⊦ r ∈ return(val, ty) ↔ r ∈ val | An Axiom |
| refin-continue | ⊦ ¬ r ∈ continue(lbl) | An Axiom |
| refin-break | ⊦ ¬ r ∈ break(lbl) | An Axiom |
| refin-initval | ⊦ ¬ r ∈ initval(istate) | An Axiom |
| refin-type | ⊦ ¬ r ∈ typeval(ty) | An Axiom |
| refin-noval | ⊦ ¬ r ∈ noval | An Axiom |
| refin-list | ⊦ r ∈ val ++ val0 ↔ r ∈ val ∨ r ∈ val0 | An Axiom |
| refin-bool | ⊦ ¬ r ∈ boolval(boolvar) | An Axiom |
| refin-ref | ⊦ r ∈ refval(r0) ↔ r = r0 | An Axiom |
| refin-short | ⊦ ¬ r ∈ shortval(sho) | An Axiom |
| refin-byte | ⊦ ¬ r ∈ byteval(by) | An Axiom |
| refin-int | ⊦ ¬ r ∈ intval(i) | An Axiom |
| get-rec | ⊦ get(m +1, val) = get(m, shiftright(val) .restval) | An Axiom |
| get-zero | ⊦ get(0, val) = shiftright(val) .firstval | An Axiom |
| getRange-rec | ⊦ m < n → getrange(m, n, val) = getrange(m, n -1, val) ++ get(n, val) | An Axiom |
| getRange-base | ⊦ getrange(m, m, val) = get(m, val) | An Axiom |
| shiftright-rec | ⊦ shiftright(val ++ val0 ++ val1) = shiftright(val ++ (val0 ++ val1)) | An Axiom |
| shiftright-shift | ⊦ ¬ is_valuelist(val) → shiftright(val ++ val0) = shiftright(val) ++ val0 | An Axiom |
| string2ref | ⊦ s→r(str) = s→r(str0) ↔ str = str0 | An Axiom |
| okprimtype-abstract | ⊦ ¬ okprimtype(val, abstract_type) | An Axiom |
| okprimtype-void | ⊦ ¬ okprimtype(val, void_type) | An Axiom |
| okprimtype-array | ⊦ ¬ okprimtype(val, mkarraytype(ty)) | An Axiom |
| okprimtype-class | ⊦ ¬ okprimtype(val, mkclasstype(class1)) | An Axiom |
| okprimtype-byte | ⊦ okprimtype(val, byte_type) ↔ is_bytevalue(val) | An Axiom |
| okprimtype-short | ⊦ okprimtype(val, short_type) ↔ is_shortvalue(val) | An Axiom |
| okprimtype-int | ⊦ okprimtype(val, int_type) ↔ is_integervalue(val) | An Axiom |
| okprimtype-bool | ⊦ okprimtype(val, boolean_type) ↔ is_boolvalue(val) | An Axiom |
| refin-string | ⊦ ¬ r ∈ stringval(stringvar) | An Axiom |
| replref-throw | ⊦ (throw(r1, ty)[r, r0]) = throw((r1 = r ⊃ r0; r1), ty) | An Axiom |
| replref-return | ⊦ (return(val, ty)[r, r0]) = return(val[r, r0], ty) | An Axiom |
| replref-continue | ⊦ (continue(lbl)[r, r0]) = continue(lbl) | An Axiom |
| replref-break | ⊦ (break(lbl)[r, r0]) = break(lbl) | An Axiom |
| replref-initval | ⊦ (initval(istate)[r, r0]) = initval(istate) | An Axiom |
| replref-type | ⊦ (typeval(ty)[r, r0]) = typeval(ty) | An Axiom |
| replref-noval | ⊦ noval[r, r0] = noval | An Axiom |
| replref-list | ⊦ (val ++ val0)[r, r0] = val[r, r0] ++ val0[r, r0] | An Axiom |
| replref-string | ⊦ (stringval(stringvar)[r, r0]) = stringval(stringvar) | An Axiom |
| replref-bool | ⊦ (boolval(boolvar)[r, r0]) = boolval(boolvar) | An Axiom |
| replref-ref | ⊦ (refval(r1)[r, r0]) = refval((r1 = r ⊃ r0; r1)) | An Axiom |
| replref-short | ⊦ (shortval(sho)[r, r0]) = shortval(sho) | An Axiom |
| replref-byte | ⊦ (byteval(by)[r, r0]) = byteval(by) | An Axiom |
| replref-int | ⊦ (intval(i)[r, r0]) = intval(i) | An Axiom |
| init_val_abst | ⊦ initial_value(abstract_type) = noval | An Axiom |
| init_val_void | ⊦ initial_value(void_type) = refval(jvmref) | An Axiom |
| refval-xtra | ⊦ ¬ is_referencevalue(val) → val .refval = jvmref | An Axiom |
| boolval-xtra | ⊦ ¬ is_boolvalue(val) → (val .boolval ↔ false) | An Axiom |
| intval-xtra | ⊦ ¬ is_integervalue(val) → val .intval = 0 | An Axiom |
| typeval-xtra | ⊦ ¬ is_typevalue(val) → val .type = void_type | An Axiom |
| incdec-other | ⊦ ¬ is_bytevalue(val) ∧ ¬ is_shortvalue(val) → incdec(val, i) = intval(val .intval + i) | An Axiom |
| incdec-short | ⊦ is_shortvalue(val) → incdec(val, i) = shortval(i2s(s2i(val .shortval) + i)) | An Axiom |
| incdec-byte | ⊦ is_bytevalue(val) → incdec(val, i) = byteval(i2b(b2i(val .byteval) + i)) | An Axiom |
| type4value-bool | ⊦ type4value(boolval(boolvar)) = boolean_type | An Axiom |
| type4value-short | ⊦ type4value(shortval(sho)) = short_type | An Axiom |
| type4value-byte | ⊦ type4value(byteval(by)) = byte_type | An Axiom |
| type4value-int | ⊦ type4value(intval(i)) = int_type | An Axiom |
| val2int-int | ⊦ val2int(intval(i)) = i | An Axiom |
| val2int-short | ⊦ val2int(shortval(sho)) = s2i(sho) | An Axiom |
| val2int-byte | ⊦ val2int(byteval(by)) = b2i(by) | An Axiom |
| val2int-xtra | ⊦ ¬ is_bytevalue(val) ∧ ¬ is_shortvalue(val) ∧ ¬ is_integervalue(val) → val2int(val) = 0 | An Axiom |
| shiftright-base | ⊦ ¬ is_valuelist(val) → shiftright(val) = val | An Axiom |
| coerce-void | ⊦ coerce(val, void_type) = refval(val .refval) | An Axiom |
| coerce-array | ⊦ coerce(val, mkarraytype(ty)) = refval(val .refval) | An Axiom |
| coerce-class | ⊦ coerce(val, mkclasstype(class)) = refval(val .refval) | An Axiom |
| coerce-char | ⊦ coerce(val, char_type) = charval(val .charval) | An Axiom |
| coerce-double | ⊦ coerce(val, double_type) = doubleval(val .doubleval) | An Axiom |
| coerce-float | ⊦ coerce(val, float_type) = floatval(val .floatval) | An Axiom |
| coerce-long | ⊦ coerce(val, long_type) = longval(val .longval) | An Axiom |
| coerce-byte | ⊦ coerce(val, byte_type) = byteval(val .byteval) | An Axiom |
| coerce-short | ⊦ coerce(val, short_type) = shortval(val .shortval) | An Axiom |
| coerce-int | ⊦ coerce(val, int_type) = intval(val .intval) | An Axiom |
| coerce-bool | ⊦ coerce(val, boolean_type) = boolval(val .boolval) | An Axiom |
| coerce-abstract | ⊦ coerce(val, abstract_type) = noval | An Axiom |
| init_val_double | ⊦ initial_value(double_type) = doubleval(0d) | An Axiom |
| init_val_float | ⊦ initial_value(float_type) = floatval(0f) | An Axiom |
| init_val_char | ⊦ initial_value(char_type) = charval(mkchar(0)) | An Axiom |
| init_val_long | ⊦ initial_value(long_type) = longval(0l) | An Axiom |
| okval-abstract | ⊦ ¬ okval(val, abstract_type) | An Axiom |
| okval-void | ⊦ okval(val, void_type) ↔ is_referencevalue(val) | An Axiom |
| okval-array | ⊦ okval(val, mkarraytype(ty)) ↔ is_referencevalue(val) | An Axiom |
| okval-class | ⊦ okval(val, mkclasstype(class1)) ↔ is_referencevalue(val) | An Axiom |
| okval-char | ⊦ okval(val, char_type) ↔ is_charvalue(val) | An Axiom |
| okval-double | ⊦ okval(val, double_type) ↔ is_doublevalue(val) | An Axiom |
| okval-float | ⊦ okval(val, float_type) ↔ is_floatvalue(val) | An Axiom |
| okval-long | ⊦ okval(val, long_type) ↔ is_longvalue(val) | An Axiom |
| okval-byte | ⊦ okval(val, byte_type) ↔ is_bytevalue(val) | An Axiom |
| okval-short | ⊦ okval(val, short_type) ↔ is_shortvalue(val) | An Axiom |
| okval-int | ⊦ okval(val, int_type) ↔ is_integervalue(val) | An Axiom |
| okval-bool | ⊦ okval(val, boolean_type) ↔ is_boolvalue(val) | An Axiom |
| okprimtype-char | ⊦ okprimtype(val, char_type) ↔ is_charvalue(val) | An Axiom |
| okprimtype-double | ⊦ okprimtype(val, double_type) ↔ is_doublevalue(val) | An Axiom |
| okprimtype-float | ⊦ okprimtype(val, float_type) ↔ is_floatvalue(val) | An Axiom |
| okprimtype-long | ⊦ okprimtype(val, long_type) ↔ is_longvalue(val) | An Axiom |
| replref-char | ⊦ (charval(jchar)[r, r0]) = charval(jchar) | An Axiom |
| replref-double | ⊦ (doubleval(doublevar)[r, r0]) = doubleval(doublevar) | An Axiom |
| replref-float | ⊦ (floatval(floatvar)[r, r0]) = floatval(floatvar) | An Axiom |
| replref-long | ⊦ (longval(lo)[r, r0]) = longval(lo) | An Axiom |
| refin-char | ⊦ ¬ r ∈ charval(jchar) | An Axiom |
| refin-double | ⊦ ¬ r ∈ doubleval(doublevar) | An Axiom |
| refin-float | ⊦ ¬ r ∈ floatval(floatvar) | An Axiom |
| refin-long | ⊦ ¬ r ∈ longval(lo) | An Axiom |
| base-boolval | ⊦ flatten(boolval(boolvar)) = boolval(boolvar) | A User Theorem |
| base-break | ⊦ flatten(break(lbl)) = break(lbl) | A User Theorem |
| base-byteval | ⊦ flatten(byteval(by)) = byteval(by) | A User Theorem |
| base-continue | ⊦ flatten(continue(lbl)) = continue(lbl) | A User Theorem |
| base-initval | ⊦ flatten(initval(istate)) = initval(istate) | A User Theorem |
| base-intval | ⊦ flatten(intval(i)) = intval(i) | A User Theorem |
| base-noval | ⊦ flatten(noval) = noval | A User Theorem |
| base-refval | ⊦ flatten(refval(r)) = refval(r) | A User Theorem |
| base-return | ⊦ flatten(return(val, ty)) = return(val, ty) | A User Theorem |
| base-shortval | ⊦ flatten(shortval(sho)) = shortval(sho) | A User Theorem |
| base-stringval | ⊦ flatten(stringval(str)) = stringval(str) | A User Theorem |
| base-throw | ⊦ flatten(throw(r, ty)) = throw(r, ty) | A User Theorem |
| base-typeval | ⊦ flatten(typeval(ty)) = typeval(ty) | A User Theorem |
| boolval | ⊦ flatten(val ++ boolval(boolvar)) = flatten(val) ++ boolval(boolvar) | A User Theorem |
| boolval-xtra-01 | ⊦ ¬ is_boolvalue(val) → ¬ val .boolval | A User Theorem |
| break | ⊦ flatten(val ++ break(lab)) = flatten(val) ++ break(lab) | A User Theorem |
| byteval | ⊦ flatten(val ++ byteval(by)) = flatten(val) ++ byteval(by) | A User Theorem |
| coerce-okval | ⊦ okval(coerce(val, ty), ty) ↔ ty ≠ abstract_type | A User Theorem |
| coerce-ref | ⊦ is_referencevalue(coerce(val, ty)) ↔ is_classtype(ty) ∨ is_arraytype(ty) ∨ ty = void_type | A User Theorem |
| continue | ⊦ flatten(val ++ continue(lab)) = flatten(val) ++ continue(lab) | A User Theorem |
| exlist | ⊦ ∃ val1, val2. flatten(val ++ val0) = val1 ++ val2 | A User Theorem |
| flatten-char | ⊦ flatten(val ++ charval(jchar)) = flatten(val) ++ charval(jchar) | A User Theorem |
| flatten-double | ⊦ flatten(val ++ doubleval(doublevar)) = flatten(val) ++ doubleval(doublevar) | A User Theorem |
| flatten-float | ⊦ flatten(val ++ floatval(floatvar)) = flatten(val) ++ floatval(floatvar) | A User Theorem |
| flatten-long | ⊦ flatten(val ++ longval(lo)) = flatten(val) ++ longval(lo) | A User Theorem |
| hasclasstype | ⊦ has_classtype(ty) → ¬ okprimtype(val, ty) | A User Theorem |
| incdec-byte-01 | ⊦ incdec(byteval(by), i) = byteval(i2b(b2i(by) + i)) | A User Theorem |
| incdec-int | ⊦ incdec(intval(i0), i) = intval(i0 + i) | A User Theorem |
| incdec-short-01 | ⊦ incdec(shortval(sho), i) = shortval(i2s(s2i(sho) + i)) | A User Theorem |
| initial-okval | ⊦ okval(initial_value(ty), ty) ↔ ty ≠ abstract_type | A User Theorem |
| initial-value | ⊦ is_referencevalue(initial_value(ty)) → initial_value(ty) = refval(jvmref) | A User Theorem |
| initial-value-01 | ⊦ is_referencevalue(initial_value(ty)) ↔ is_reftype(ty) ∨ ty = void_type | A User Theorem |
| initial-value-02 | ⊦ is_reftype(ty) → initial_value(ty) = refval(jvmref) | A User Theorem |
| initval | ⊦ flatten(val ++ initval(istate)) = flatten(val) ++ initval(istate) | A User Theorem |
| initval-ref | ⊦ initial_value(ty) = refval(r) ↔ r = jvmref ∧ (is_reftype(ty) ∨ ty = void_type) | A User Theorem |
| intval | ⊦ flatten(val ++ intval(i)) = flatten(val) ++ intval(i) | A User Theorem |
| noval | ⊦ flatten(val ++ noval) = flatten(val) ++ noval | A User Theorem |
| noval-01 | ⊦ flatten(val) = noval ↔ val = noval | A User Theorem |
| okprim-array | ⊦ okprimtype(val, ty) → ¬ is_arraytype(ty) | A User Theorem |
| okprim-class | ⊦ okprimtype(val, ty) → ¬ is_classtype(ty) | A User Theorem |
| okprim-letype | ⊦ okprimtype(val, ty) → (ty0 ≤ ty ↔ ty0 = ty) | A User Theorem |
| okprim-ref | ⊦ is_reftype(ty) → ¬ okprimtype(val, ty) | A User Theorem |
| okprimtype-okval | ⊦ okprimtype(val, ty) → okval(val, ty) | A User Theorem |
| okprimtype-okval-01 | ⊦ ¬ okval(val, ty) → ¬ okprimtype(val, ty) | A User Theorem |
| okprimtype-refval | ⊦ ¬ okprimtype(refval(r), ty) | A User Theorem |
| okval-case | ⊦ okval(val, ty) ↔ is_boolvalue(val) ∧ ty = boolean_type ∨ is_integervalue(val) ∧ ty = int_type ∨ is_shortvalue(val) ∧ ty = short_type ∨ is_bytevalue(val) ∧ ty = byte_type ∨ is_longvalue(val) ∧ ty = long_type ∨ is_floatvalue(val) ∧ ty = float_type ∨ is_doublevalue(val) ∧ ty = double_type ∨ is_charvalue(val) ∧ ty = char_type ∨ is_referencevalue(val) ∧ (is_classtype(ty) ∨ is_arraytype(ty) ∨ ty = void_type) | A User Theorem |
| okval-noval | ⊦ ¬ okval(noval, ty) | A User Theorem |
| okval-reftype | ⊦ is_reftype(ty) → (okval(val, ty) ↔ is_referencevalue(val)) | A User Theorem |
| okval-refval | ⊦ okval(refval(r), ty) ↔ ty = void_type ∨ is_reftype(ty) | A User Theorem |
| okval-refval-01 | ⊦ is_referencevalue(val) → (okval(val, ty) ↔ ty = void_type ∨ is_reftype(ty)) | A User Theorem |
| okval-subtype | ⊦ ¬ is_referencevalue(val) ∧ ty0 ≤ ty ∧ is_reftype(ty) → ¬ okval(val, ty) | A User Theorem |
| okval-subtype-01 | ⊦ ¬ is_referencevalue(val) ∧ ty0 ≤ ty ∧ is_reftype(ty) → ¬ okval(val, ty0) | A User Theorem |
| okval-supertype | ⊦ okval(val, ty) ∧ ty ≤ ty0 → okval(val, ty0) | A User Theorem |
| refin-not | ⊦ is_integervalue(val) → ¬ r ∈ val | A User Theorem |
| refin-not-01 | ⊦ is_bytevalue(val) → ¬ r ∈ val | A User Theorem |
| refin-not-02 | ⊦ is_shortvalue(val) → ¬ r ∈ val | A User Theorem |
| refin-not-03 | ⊦ is_boolvalue(val) → ¬ r ∈ val | A User Theorem |
| refin-not-04 | ⊦ is_referencevalue(val) → (r ∈ val ↔ r = val .refval) | A User Theorem |
| refin-not-05 | ⊦ is_stringvalue(val) → ¬ r ∈ val | A User Theorem |
| refin-not-06 | ⊦ is_novalue(val) → ¬ r ∈ val | A User Theorem |
| refin-not-07 | ⊦ is_typevalue(val) → ¬ r ∈ val | A User Theorem |
| refin-not-08 | ⊦ is_initvalue(val) → ¬ r ∈ val | A User Theorem |
| refin-not-09 | ⊦ is_break_mode(val) → ¬ r ∈ val | A User Theorem |
| refin-not-10 | ⊦ is_continue_mode(val) → ¬ r ∈ val | A User Theorem |
| refin-not-11 | ⊦ is_return_mode(val) → (r ∈ val ↔ r ∈ val .val) | A User Theorem |
| refin-not-12 | ⊦ is_throw_mode(val) → (r ∈ val ↔ r = val .refval) | A User Theorem |
| refp-01 | ⊦ refp(val) → refval(val .refval) = val | A User Theorem |
| refp-02 | ⊦ refp(refval(r)) ↔ r ≠ jvmref | A User Theorem |
| refval | ⊦ flatten(val ++ refval(r)) = flatten(val) ++ refval(r) | A User Theorem |
| return | ⊦ flatten(val ++ return(val0, ty)) = flatten(val) ++ return(val0, ty) | A User Theorem |
| shortval | ⊦ flatten(val ++ shortval(sho)) = flatten(val) ++ shortval(sho) | A User Theorem |
| stringval | ⊦ flatten(val ++ stringval(str)) = flatten(val) ++ stringval(str) | A User Theorem |
| throw | ⊦ flatten(val ++ throw(r, ty)) = flatten(val) ++ throw(r, ty) | A User Theorem |
| typeval | ⊦ flatten(val ++ typeval(ty)) = flatten(val) ++ typeval(ty) | A User Theorem |
| typeval-01 | ⊦ val ≠ typeval(mkclasstype(class)) → val .type ≠ mkclasstype(class) | A User Theorem |
| typeval-02 | ⊦ val ≠ typeval(mkarraytype(ty)) → val .type ≠ mkarraytype(ty) | A User Theorem |
| typeval-03 | ⊦ val ≠ typeval(boolean_type) → val .type ≠ boolean_type | A User Theorem |
| typeval-04 | ⊦ val ≠ typeval(byte_type) → val .type ≠ byte_type | A User Theorem |
| typeval-05 | ⊦ val ≠ typeval(short_type) → val .type ≠ short_type | A User Theorem |
| typeval-06 | ⊦ val ≠ typeval(int_type) → val .type ≠ int_type | A User Theorem |
| val2int-int-01 | ⊦ is_integervalue(val) → val2int(val) = val .intval | A User Theorem |