[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Theorem base summary for Specification junkrefs

bytearray-is-no-junk(7,2)junkref-not-hasclasstype(1,0)junkrefs-delete(32,9)junkrefs-union-disjoint(81,41)validfieldlist-def-01(28,13)validref-def(0,0)validref-put-norefval-equiv(12,4)validreflist-empty(1,1)validrefval-superset(7,3)validstatfields-storekeys-def(0,0)
initsubset-addclass(10,3)junkref-not-hasclasstype-01(22,10)junkrefs-delete-01(2,1)levelsubset-all-types(17,8)validfieldlist-empty(1,1)validref-forward(17,7)validref-put-null(12,4)validreflist-getarray(6,3)validrefval-union(6,2)validstatfields-subset(17,8)
initsubset-addclass-01(2,1)junkref-not-is-array(2,1)junkrefs-delete-02(34,12)levelsubset-classex(4,2)validfieldlist-mode(6,1)validref-forward-01(4,1)validref-put-refval(12,4)validreflist-getarray-less(1,1)validrefvalnotnull-addarray(3,2)validstatfields-throw-predef(4,2)
initsubset-addobj(3,1)junkref-not-okreftype(4,2)junkrefs-empty(0,0)levelsubset-classex-01(4,1)validfieldlist-mode-01(4,1)validref-forward-array(12,4)validref-put-shortval(9,3)validreflist-getarray-less-01(24,11)validrefvalnotnull-addobj(3,2)validstatfields-throw-predef-01(2,1)
initsubset-addobj-01(4,2)junkref-not-okreftype-01(4,2)junkrefs-empty-01(1,0)levelsubset-classex-02(4,1)validfieldlist-one-01(1,1)validref-forward-array-01(2,1)validref-put-statfield(8,4)validreflist-getarray-less-02(12,6)validrefvalnotnull-def(0,0)validstatfields-throw-predef-02(2,1)
initsubset-def(0,0)junkref-not-valid(7,4)junkrefs-inttype(5,1)levelsubset-classex-03(6,2)validfieldlist-put-statfield(10,5)validref-hasnoclasstype-level(4,2)validref-put-statfield-01(4,1)validreflist-getarray-less-03(1,1)validrefvalnotnull-put-statfield(9,3)validstatfields-union(5,2)
initsubset-init(5,2)junkref-not-valid-01(2,1)junkrefs-is-junk(0,0)levelsubset-def(0,0)validfieldlist-rec(10,5)validref-intarray-put(4,2)validref-put-statfield-02(4,1)validreflist-no-reftype(11,5)validstatfield-addclass-other(22,8)validstatfields-validstatfield(9,5)
initsubset-init-forward(5,2)junkref-notin(2,1)junkrefs-junkref(4,2)levelsubset-is-array(4,2)validfieldlist-superset(9,4)validref-intarray-put-01(6,3)validref-put-statfield-03(1,1)validreflist-one(1,1)validstatfield-addclass-same(16,5)validstatfields-validstatfield-01(3,1)
initsubset-initdone-forward(4,1)junkref-notypeex(1,0)junkrefs-levelsubset(35,11)levelsubset-is-obj(5,2)validmode(4,2)validref-is-junk(2,1)validref-putbar(18,8)validreflist-one-01(2,1)validstatfield-addobj(9,3)validstatfields-void(4,2)
initsubset-initerror(23,10)junkref-null(4,1)junkrefs-levelsubset-01(2,1)levelsubset-ref(1,1)validmode-01(2,1)validref-is-junk-better(2,1)validref-putrkvs(52,20)validreflist-rec(14,6)validstatfield-index(4,2)validsubset-addclass(1,1)
initsubset-initerror-01(2,1)junkref-okarray-byte(6,2)junkrefs-newref(2,1)levelsubset-tdnameex(7,3)validmode-addarray(10,5)validref-isarray(2,1)validref-putrkvs-norefval(11,4)validreflist-rec-01(1,1)validstatfield-level-expand(14,6)validsubset-addclass-01(2,1)
initsubset-initerror-02(27,11)junkref-okbytearray(3,1)junkrefs-newref-01(2,1)levelsubset-trans(16,6)validmode-addclass(7,4)validref-isarrayref(7,2)validref-refin(1,0)validreflist-supertype(9,4)validstatfield-levelsubset(10,3)validsubset-addobj(4,2)
initsubset-initerror-03(4,2)junkref-predefined(2,1)junkrefs-newref-02(2,1)levelsubset-typeex(3,1)validmode-addobj(9,4)validref-isobj(3,2)validref-runtimetype(2,1)validrefnotnull(1,0)validstatfield-mode(9,3)validsubset-addobj-01(9,4)
initsubset-initerror-04(42,14)junkref-primarray-level(4,3)junkrefs-newref-03(1,1)nojunkref-typeex(2,1)validmode-def(0,0)validref-isvalidref(3,1)validref-subset(8,4)validrefnotnull-addarray(3,2)validstatfield-other-statfield(4,1)validsubset-addobj-02(4,2)
initsubset-mode(4,2)junkref-primarray-level-01(35,15)junkrefs-newref-04(1,1)nojunkref-typeex-01(11,5)validmode-noval-put(4,2)validref-junkref(2,1)validref-subset-01(8,4)validrefnotnull-addarray-01(1,0)validstatfield-primtype-level(12,5)validsubset-def(0,0)
initsubset-mode-01(1,1)junkref-primarray-lvl(34,11)junkrefs-notin(51,19)nojunkref-typeex-02(4,1)validmode-noval-put-01(2,1)validref-levelsubset(4,2)validref-subtype(4,2)validrefnotnull-addarray-len(4,2)validstatfield-put-array-norefval(18,6)validsubset-okbytearray(7,4)
initsubset-mode-02(1,1)junkref-put-array-norefval(10,4)junkrefs-notin-01(2,1)okbytearray(4,2)validmode-put-nonnull(4,1)validref-levelsubset-01(2,1)validref-subtype-01(2,1)validrefnotnull-addobj(4,2)validstatfield-put-norefval(36,11)validsubset-okbytearray-01(1,0)
initsubset-put-statfield(28,13)junkref-put-ba(12,4)junkrefs-notin-02(2,1)okbytearray-01(2,1)validmode-put-nonnull-01(1,0)validref-mode(1,1)validref-subtype-02(5,2)validrefnotnull-array(2,1)validstatfield-put-statfield(23,9)validsubset-predefined(3,1)
initsubset-put-statfield-01(43,17)junkref-put-badarrayfield(10,4)junkrefs-notin-03(1,1)okbytearray-02(4,2)validmode-put-statfield(13,5)validref-newref(2,1)validref-supertype(4,2)validrefnotnull-array-01(2,1)validstatfield-put-statfield-int(8,4)validsubset-predefined-01(2,1)
initsubset-put-statfield-int(16,8)junkref-put-badarrayindex(6,2)junkrefs-null(0,0)okbytearray-putrkvs(4,3)validmode-put-statfield-01(2,1)validref-newref-subset(8,3)validref-throw(2,1)validrefnotnull-array-02(2,1)validstatfield-putbytearray-noreftype(13,6)validsubset-predefined-02(2,1)
initsubset-same(1,1)junkref-put-badclassfield(12,4)junkrefs-null-01(50,15)okbytearray-validref(26,10)validmode-put-statfield-02(3,1)validref-no-len(1,0)validref-type(4,2)validrefnotnull-array-len-subset(4,2)validstatfield-putrkvs(52,23)validsubset-predefined-03(2,1)
initsubset-trans(37,16)junkref-put-badfield(22,10)junkrefs-null-02(2,1)same-subclasses-classex(4,1)validmode-superset(11,6)validref-no-obj(3,1)validref-type-forward(4,2)validrefnotnull-bytearray(2,1)validstatfield-storekey-def(0,0)validsubset-put-statfield(14,5)
initsubset-validstatfield-forward(25,11)junkref-put-field(14,4)junkrefs-null-03(2,0)same-subclasses-classex-01(4,1)validmode-throw-predef(6,3)validref-no-type(2,1)validref-type-forward-01(2,1)validrefnotnull-def(0,0)validstatfield-subset(9,3)validsubset-put-statfield-01(1,1)
initsubset-validstatfields-forward(7,3)junkref-put-norefval(13,4)junkrefs-one(10,7)same-subclasses-classex-02(4,1)validmode-throw-predef-01(2,1)validref-noreftype(2,1)validref-typeex(2,1)validrefnotnull-getarray-subset(6,3)validstatfield-throw-predef(20,7)validsubset-put-statfield-02(1,1)
is_valid_ref-levelsubset(9,7)junkref-put-norefval-01(13,4)junkrefs-primarray(28,9)same-subclasses-interfaceex(4,1)validmode-throw-predef-02(2,1)validref-not-junkrefs(8,4)validref-typeex-01(1,0)validrefnotnull-is-junk(4,2)validstatfield-union(17,7)validsubset-same(1,1)
junkref-abstract(6,3)junkref-put-norefval-equiv(16,5)junkrefs-put-array-norefval(35,11)same-subclasses-interfaceex-01(4,1)validmode-throw-typeex(6,2)validref-not-tdnameex(6,2)validref-typele(2,1)validrefnotnull-isarray(4,2)validstatfield-validref(11,3)validsubset-trans(22,9)
junkref-ac(29,11)junkref-put-null(12,3)junkrefs-put-ba(17,5)same-subclasses-is-array(20,9)validmodeval-def(0,0)validref-notin(2,1)validref-union(8,4)validrefnotnull-isvalidref(5,2)validstatfield-void(2,1)validsubset-validref-forward(4,1)
junkref-addarray-01(50,19)junkref-put-refval(16,6)junkrefs-put-badarrayfield(34,11)same-subclasses-is-obj(4,2)validref-ac(26,10)validref-null(1,1)validref-union-left(2,1)validrefnotnull-junk(2,1)validstatfields-addclass(29,14)validval-def(0,0)
junkref-addarray-02(2,1)junkref-put-refval-01(23,9)junkrefs-put-badarrayindex(35,11)same-subclasses-one-def(0,0)validref-addarray(6,3)validref-object(4,2)validref-voidtype(7,4)validrefnotnull-no-len(2,1)validstatfields-addclass-other(32,10)validval-field-byteval(5,2)
junkref-addarray-03(2,1)junkref-put-refval-statfield(11,5)junkrefs-put-badclassfield(44,15)same-subclasses-ref(1,1)validref-addarray-get(2,1)validref-object-01(3,1)validrefkeynotnull-addarray(12,5)validrefnotnull-no-newref(2,1)validstatfields-addobj(9,4)validval-field-norefval(6,2)
junkref-addarray-04(23,11)junkref-put-refval-statfield-01(1,1)junkrefs-put-badfield(57,19)same-subclasses-subclass(10,3)validref-addarray-get-01(2,1)validref-okarray(7,2)validrefkeynotnull-addobj(6,3)validrefnotnull-no-type(2,1)validstatfields-addobj-01(7,4)validval-field-shortval(5,2)
junkref-addarray-newref(10,4)junkref-put-statfield(10,3)junkrefs-put-norefval(6,1)same-subclasses-tdnameex(2,1)validref-addarray-other-01(5,3)validref-okreftype(6,4)validrefkeynotnull-def(0,0)validrefnotnull-not(2,1)validstatfields-class(0,0)validval-index-byteval(3,2)
junkref-addarray-newref-put(14,5)junkref-putbar(19,9)junkrefs-put-norefval-01(43,15)same-subclasses-tdnameex-01(3,1)validref-addarray-same(6,3)validref-primarray(29,10)validrefkeynotnull-has-field(13,5)validrefnotnull-notnull(1,1)validstatfields-class-01(30,12)validval-index-norefval(4,2)
junkref-addarray-noreftype(6,2)junkref-putbar-01(16,7)junkrefs-put-norefval-equiv(45,16)same-subclasses-tdnameex-02(7,3)validref-addarray-same-01(1,0)validref-put-any(9,3)validrefkeynotnull-in(2,1)validrefnotnull-null(2,1)validstatfields-def(0,0)validval-int(1,1)
junkref-addbytearray(2,1)junkref-rec-case(16,6)junkrefs-put-notin(52,16)same-subclasses-tdnameex-03(2,1)validref-addobj(9,5)validref-put-any-01(7,2)validrefkeynotnull-no-newrefs(4,1)validrefnotnull-primarray(4,2)validstatfields-empty(1,1)validval-null(1,1)
junkref-addobj(11,5)junkref-rec-keep-case(14,4)junkrefs-put-notin-butlast(64,26)same-subclasses-tdnameex-04(7,3)validref-addobj-this(6,2)validref-put-array-any(8,4)validrefkeynotnull-notnewref(8,3)validrefnotnull-put-byteval(10,3)validstatfields-empty-01(5,3)validval-put-any(102,39)
junkref-addobj-01(54,22)junkref-subset(22,13)junkrefs-put-null(50,14)same-subclasses-tdnameex-05(1,0)validref-array(3,1)validref-put-array-norefval(6,3)validrefkeynotnull-notnull(2,2)validrefnotnull-put-shortval(13,5)validstatfields-initundone(25,8)validval-putrkvs(29,13)
junkref-array(40,15)junkref-tdnameex(2,1)junkrefs-put-null-01(62,19)same-subclasses-trans(16,6)validref-array-01(2,1)validref-put-array-norefval-01(4,2)validrefkeynotnull-put-byteval(17,6)validrefnotnull-put-statfield(9,4)validstatfields-levelsubset(7,3)validvals-append(21,6)
junkref-bad-type(2,1)junkref-union(2,1)junkrefs-put-null-02(39,13)same-subclasses-typeex(30,13)validref-array-02(3,1)validref-put-array-refval(5,3)validrefkeynotnull-put-shortval(17,6)validrefnotnull-put-statfield-01(4,1)validstatfields-one(1,1)validvals-append-01(1,0)
junkref-class(44,15)junkref-union-disjoint(15,7)junkrefs-put-refval(87,32)valid-typeex(4,2)validref-array-03(5,2)validref-put-array-refval-01(4,1)validrefkeynotnull-put-statfield(2,2)validrefnotnull-put-statfield-02(8,3)validstatfields-put-array-norefval(5,2)validvals-one(3,1)
junkref-class-01(59,22)junkref-void(3,1)junkrefs-put-refval-01(75,29)validfield-def(0,0)validref-array-len-in(6,2)validref-put-array-refval-02(6,1)validrefkeynotnull-refval-in(8,3)validrefnotnull-putbar(20,10)validstatfields-put-byteval(1,0)validvals-put-any(9,4)
junkref-class-02(24,7)junkref-voidarray(4,2)junkrefs-put-refval-02(49,20)validfield-levelsubset(9,3)validref-array-notin(2,1)validref-put-array-refval-03(8,2)validrefkeynotnull-statfield-intersect(11,5)validrefnotnull-subset(6,3)validstatfields-put-byteval-01(6,1)validvals-putrkvs(9,3)
junkref-classtype(8,4)junkreflist-def(0,0)junkrefs-put-refval-statfield(33,11)validfield-one(8,4)validref-array-rec(18,7)validref-put-badarrayfield(6,3)validrefkeynotnull-subset(20,11)validrefnotnull-type(2,1)validstatfields-put-norefval-field(13,4)validvals-voidtype(7,4)
junkref-def(64,25)junkreflist-empty(2,1)junkrefs-put-statfield(34,11)validfield-put-statfield(11,4)validref-arrayreftype(9,3)validref-put-badarrayindex(6,3)validrefkeynotnull-union(19,10)validrefnotnull-typeex(2,1)validstatfields-put-norefval-field-better(15,6)validvals-voidtype-01(2,1)
junkref-field-reftype(21,10)junkreflist-rec(15,5)junkrefs-runtimetype(2,1)validfield-put-statfield-01(4,1)validref-arraytype(2,1)validref-put-badclassfield(8,3)validrefkeynotnull-union-01(3,1)validrefnotnull-union-at-right(40,19)validstatfields-put-other-statfield(40,16)validvals-voidtype-02(3,2)
junkref-is-junk(6,3)junkrefs-addarray(43,15)junkrefs-sametype(4,2)validfield-superset(14,6)validref-bad-type(2,1)validref-put-badfield(10,4)validrefkeynotnull-union-same(2,1)validrefnotnull-validref(2,1)validstatfields-put-statfield(5,1)
junkref-is_array(2,1)junkrefs-addarray-newref-put(6,2)junkrefs-sametype-01(1,0)validfieldinits-def(0,0)validref-bytearray(2,1)validref-put-byteval(10,3)validrefkeynotnull-union-same-01(2,1)validrefval-addarray(3,2)validstatfields-put-statfield-01(8,4)
junkref-isarray-typeex(16,6)junkrefs-addarray-noreftype(15,6)junkrefs-subclass(7,2)validfieldinits-def-01(45,17)validref-bytearray-level(1,0)validref-put-field(8,3)validrefkeynotnull-union-same-02(2,1)validrefval-addobj(3,2)validstatfields-put-statfield-02(8,3)
junkref-keyin(2,1)junkrefs-addobj(35,12)junkrefs-subset(50,20)validfieldinits-empty(1,1)validref-bytearray-level-01(4,2)validref-put-field-any(10,3)validrefkeynotnull-validrefnotnull(4,2)validrefval-def(0,0)validstatfields-put-statfield-03(11,4)
junkref-levelsubset(8,3)junkrefs-append(31,10)junkrefs-subtype(29,11)validfieldinits-junkref(6,3)validref-class(16,6)validref-put-field-refval(6,1)validrefkeyval-def(0,0)validrefval-junkref(2,0)validstatfields-put-statfield-04(4,1)
junkref-levelsubset-01(2,1)junkrefs-array(0,0)junkrefs-supertype(28,13)validfieldinits-one(8,3)validref-class-rec(22,7)validref-put-field-refval-01(8,1)validrefkeyvalues-def(0,0)validrefval-put-statfield(6,2)validstatfields-put-statfield-05(3,1)
junkref-newref(3,2)junkrefs-bytearray(3,2)junkrefs-typein(2,1)validfieldinits-rec(24,9)validref-class-rec-better(10,3)validref-put-norefval(10,3)validreflist-addarray(12,4)validrefval-put-statfield-01(1,1)validstatfields-put-statfield-06(36,10)
junkref-noreftype(2,1)junkrefs-class(0,0)junkrefs-union(57,21)validfieldinits-validreflist(26,8)validref-class-rec-better-keep(8,2)validref-put-norefval-01(6,1)validreflist-def(0,0)validrefval-ref(1,1)validstatfields-rec(10,4)