[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 addfuns

ac-bad(24,4)ac-new(24,7)add-init-newref(1,1)add-type(6,1)addobj-keysrec(0,0)instore-addobj(11,5)is_obj-reftype(1,0)is_valid_ref-type-typeval(9,5)isobj-put-03(15,6)reffield-del(29,15)
ac-bad-01(24,4)ac-newrefs(3,2)add-init-newref-01(1,1)add-type-01(1,0)addobj-mode(1,0)instore-addobj-rec(21,11)is_obj-refval(3,2)is_valid_ref-typeex(10,4)isobj-put-04(6,1)reffield-null(2,1)
ac-bad-02(23,4)ac-no1(6,0)add-init-newref-02(1,1)add-type-02(1,0)addobj-mode-01(1,0)is-any-object(0,0)is_obj-refval-01(3,2)is_valid_ref-typeex-01(2,1)isobj-put-badfield(18,7)statfields-abstract(0,0)
ac-bad-03(23,4)ac-no2(4,1)add-initdone(1,0)add-type-03(2,1)addobj-okarray(8,2)is-real-object-def(0,0)is_obj-subset(4,2)is_valid_ref-typeex-02(1,0)isobj-put-index-01(15,8)statfields-index(0,0)
ac-class(2,2)ac-okarray(14,4)add-initdone-01(4,2)add-type-04(1,0)addobj-okbytearray(2,1)is-valid-ref(0,0)is_obj-type(1,0)is_valid_ref-typeval(1,0)isobj-put-index-02(5,1)statfields-index-01(2,1)
ac-del(29,6)ac-okarray-01(8,2)add-initerror(3,2)add-uninit(2,1)addobj-oktype(1,0)is-valid-ref-stronger-def(0,0)is_obj-type-01(1,0)is_valid_ref-typeval-01(2,1)isobj-put-samefield(12,3)statfields-nodups(0,0)
ac-del-01(29,6)ac-okarrays(22,8)add-initerror-01(1,0)add-update-same(19,8)addobj-out-put(2,1)is_array-addobj(4,2)is_obj-type-02(1,0)is_valid_ref-update(3,1)isobj-put-samefield-01(17,6)statfields-predef(0,0)
ac-del-02(7,2)ac-okclass(5,3)add-initundone(4,2)addclass-base(0,0)addobj-put(1,1)is_array-addobj-01(2,1)is_obj-typeex(2,1)is_valid_ref-void(3,1)isobj-put-samefield-02(8,3)statfields-same-class(0,0)
ac-del-03(3,3)ac-okreftype(5,2)add-initundone-01(1,0)addclass-exactarray(8,4)addobj-put-switch(2,1)is_array-validref(2,1)is_obj-typeex-01(2,1)isarray-isobj(1,0)isobj-put-samefield-03(12,3)statfields-same-class-01(2,1)
ac-dups(1,0)ac-oktype(1,0)add-isarray(4,2)addclass-mode-in(3,2)addobj-put-switch-01(4,1)is_obj(0,0)is_obj-typeex-02(2,1)isarray-isobj-01(2,1)isobj-put-statfield(5,1)statfields-special(0,0)
ac-dups-01(1,0)ac-one1(1,1)add-length(4,2)addclass-no(1,0)addobj-rec(0,0)is_obj-01(1,0)is_obj-typele(4,2)isobj-addclass(20,8)isobj-putbar(17,8)statfields-typeex(0,0)
ac-dups-02(27,7)ac-one2(2,1)add-mode(1,0)addclass-no1(0,0)addobj-rec-01(1,0)is_obj-addobj(2,1)is_obj-union(4,2)isobj-addobj(14,7)isobj-putbar-01(20,9)stsubset-addobj(22,11)
ac-dups-03(27,7)ac-one3(1,1)add-mode-01(3,2)addclass-no2(0,0)addobj-simple(0,0)is_obj-addobj-01(3,1)is_obj-union-disjoint(8,4)isobj-addobj-01(11,6)isobj-putbar-02(2,1)valid-type-typeval(11,4)
ac-dups-04(13,3)ac-out(25,5)add-mode-02(1,1)addclass-okarray(27,7)addobj-subset(6,3)is_obj-array(1,0)is_obj-update(3,1)isobj-addobj-02(4,2)isobj-putref(3,3)validFields-addobj(4,2)
ac-dups-05(13,3)ac-out-01(3,2)add-new(1,0)addclass-okbytearray(3,2)addobj-throw-subset(4,2)is_obj-array-01(1,0)is_obj-validref(1,0)isobj-addobj-03(12,6)isobj-rec(11,5)validfieldinits-all(0,0)
ac-getbar(23,3)ac-refin(23,3)add-new-01(1,0)addclass-switch(27,6)addobj-type(1,0)is_obj-arraytype(1,0)is_obj_exact(0,0)isobj-addobj-04(24,11)isobj-reftype(4,1)validfieldinits-empty(1,1)
ac-in(29,10)ac-refs(20,5)add-notin(10,1)addclass-switch-01(27,6)addobj-union(13,7)is_obj-arraytype-01(1,0)is_valid_ref(3,1)isobj-all(6,2)isobj-subset(27,11)validfieldinits-one(6,3)
ac-in-01(1,0)ac-reftype(3,2)add-nput(10,4)addclass-union-sw(9,5)addobj-union-rew(17,9)is_obj-arraytype-02(1,0)is_valid_ref-01(1,0)isobj-array(2,1)isobj-type(1,0)validfieldinits-one-01(2,1)
ac-in-02(22,3)ac-shift(27,6)add-nput-01(8,3)addclass-update-sw(10,5)addobj-union-switch(10,5)is_obj-bytearray(1,0)is_valid_ref-02(7,3)isobj-array-01(2,1)isobj-type-01(2,1)validfieldinits-one-02(2,1)
ac-in-03(23,3)ac-shift-01(1,0)add-nput-02(8,3)addclass-validFields(13,7)ao-init(4,2)is_obj-classtype(1,0)is_valid_ref-03(1,0)isobj-arraytype(2,1)isobj-type-02(1,0)validfieldinits-rec(21,7)
ac-in-03-02(23,3)ac-shift-02(24,5)add-okarray(6,2)addclass-yes(0,0)ao-init-01(5,2)is_obj-def(0,0)is_valid_ref-addobj(6,4)isobj-arraytype-01(10,2)isobj-type-03(2,1)validref(1,0)
ac-in-04(1,0)ac-shift-03(28,7)add-okarray-01(2,1)addobj-addclass-sw(29,15)ao-init-02(4,2)is_obj-del(2,1)is_valid_ref-addobj-01(4,2)isobj-arraytype-02(2,1)isobj-type-04(2,1)validref-01(2,1)
ac-in-05(1,0)ac-type(27,4)add-okarray-02(2,1)addobj-addobj-switch(15,8)ao-put(10,4)is_obj-del-01(1,0)is_valid_ref-array(1,0)isobj-bytearray(10,4)isobj-type-05(2,1)validref-02(2,1)
ac-in-06(35,6)ac-uninit(2,1)add-okarray-03(2,1)addobj-at(2,0)del-addobj(12,8)is_obj-field-in(1,0)is_valid_ref-array-01(1,0)isobj-classtype(2,1)isobj-type-06(2,1)validref-addobj(2,1)
ac-in-07(1,0)ac-uninitset(8,4)add-okarray-04(2,1)addobj-at-01(10,4)endfinallymode(2,1)is_obj-field-noreftype(11,4)is_valid_ref-def(10,5)isobj-del(6,2)isobj-type-07(2,1)validref-addobj-01(1,0)
ac-in-08(21,3)add-at(2,1)add-okarray-05(12,3)addobj-at-02(2,1)endfinallymode-01(1,0)is_obj-field-norefval(11,4)is_valid_ref-del(1,0)isobj-del-01(14,7)isobj-type-08(2,1)validref-del(3,1)
ac-in-09(29,6)add-at-01(1,0)add-okbar(3,2)addobj-at-03(2,1)endfinallymode-02(2,1)is_obj-full-expand(8,2)is_valid_ref-del-01(4,2)isobj-del-02(2,1)isobj-typeex(1,0)validref-del-01(4,2)
ac-in-10(22,3)add-class(4,2)add-okclass(2,1)addobj-at-null(4,2)endfinallymode-03(2,2)is_obj-hasclasstype(1,0)is_valid_ref-field-in(3,1)isobj-del-03(4,2)isobj-typein(2,1)validref-isarray(2,1)
ac-in-11(22,4)add-classof(2,1)add-okclass-01(4,2)addobj-at-other(2,1)endfinallymode-04(2,1)is_obj-isarray(1,0)is_valid_ref-int(2,1)isobj-del-04(2,1)isobj-typele(2,1)validref-isobj(2,1)
ac-init(34,10)add-dupput(15,9)add-okreftype(4,2)addobj-at-other-01(2,1)endfinallymode-05(3,2)is_obj-isobj-01(1,0)is_valid_ref-isarray(1,0)isobj-field-in(11,4)isobj-union(4,2)validref-new(2,1)
ac-init-01(27,6)add-field(1,0)add-okstore(12,6)addobj-at-other-02(2,1)eqmode-01(1,0)is_obj-newref(1,0)is_valid_ref-isobj(1,0)isobj-fieldtype(5,3)isobj-union-01(18,8)validref-notin(3,1)
ac-init-02(27,6)add-field-01(1,0)add-oktype(1,0)addobj-at-other-03(8,1)exactarray-addobj(8,4)is_obj-no-interface(3,1)is_valid_ref-new(1,0)isobj-hasclasstype(2,1)isobj-union-disjoint(2,1)validref-notin-01(4,2)
ac-init-03(2,1)add-field-02(1,0)add-oktype-01(1,0)addobj-at-this(6,2)exactarray-addobj-01(2,0)is_obj-no-refval(10,3)is_valid_ref-no-arraytype(1,0)isobj-instfields(1,0)isobj-update(6,1)validref-notin-02(2,1)
ac-init-04(4,2)add-field-03(1,0)add-oktype-02(2,0)addobj-at-this-01(2,1)getByteArray-addobject(4,1)is_obj-no-refval-01(10,3)is_valid_ref-notin(1,0)isobj-isarray(4,1)isobj-update-01(16,9)validref-null(2,1)
ac-init-05(4,2)add-field-if(2,0)add-one(2,1)addobj-base(0,0)getByteArray-addobject-01(4,1)is_obj-no-refval-02(2,1)is_valid_ref-notin-01(1,0)isobj-isobj(6,3)isobj-void(2,1)validref-okreftype(6,2)
ac-init-06(2,1)add-field-same(5,1)add-out(1,0)addobj-delsw(16,8)has_reffield-array(0,0)is_obj-no-refval-03(2,1)is_valid_ref-notin-02(1,0)isobj-isobj-01(2,1)isvalidref-array(1,0)validref-primtype(5,4)
ac-init-07(2,1)add-field-same-01(1,0)add-out-01(3,2)addobj-getarray(4,2)has_reffield-class(0,0)is_obj-not-classex(1,0)is_valid_ref-null(1,0)isobj-jvmref(2,1)isvalidref-put-array-badindex(13,7)validref-primtype-01(5,4)
ac-init-08(2,1)add-field-same-02(5,1)add-out-02(3,2)addobj-getarray-01(9,4)has_reffield-no(0,0)is_obj-not-classex-01(1,0)is_valid_ref-obj(1,0)isobj-mode(2,2)mode-addobj(3,2)validref-primtype-02(5,4)
ac-init-09(2,1)add-gins(9,4)add-put(1,0)addobj-getintarray(4,2)haskeys-addobj(5,2)is_obj-not-classex-02(1,0)is_valid_ref-okbytearray(1,0)isobj-newref(2,1)new-add(3,2)validref-put(7,5)
ac-init-10(2,1)add-gins-01(1,0)add-put-01(1,0)addobj-getintarray-01(4,2)instfields-Object(1,1)is_obj-not-tdnameex(1,0)is_valid_ref-primarray(7,3)isobj-newref-01(2,1)newref-addobj(2,1)validref-put-01(10,6)
ac-init-11(2,1)add-goodfield(2,1)add-put-02(2,1)addobj-in(2,1)instfields-abstract(0,0)is_obj-notin(1,0)is_valid_ref-primtype(1,0)isobj-newref-02(2,1)newref-addobj-in(2,1)validref-put-samefield(9,5)
ac-init-first(9,5)add-gput(1,0)add-put-03(1,0)addobj-in-01(2,1)instfields-index(0,0)is_obj-notin-01(9,3)is_valid_ref-primtype-01(1,0)isobj-notin(2,1)nouninit-addclass(7,4)validref-put-samefield-01(9,5)
ac-init-other(4,2)add-in(1,0)add-put-04(2,1)addobj-in-02(9,5)instfields-index-01(2,1)is_obj-null(1,0)is_valid_ref-put(17,9)isobj-notin-01(2,1)nouninit-addobj(6,2)validref-reftype(3,1)
ac-isarray(22,6)add-in-01(1,0)add-put-05(2,1)addobj-init(3,2)instfields-index-02(2,1)is_obj-put(4,2)is_valid_ref-put-01(2,1)isobj-notin-02(2,1)okarray-addobj(4,2)validref-typeval(4,2)
ac-lookup(25,6)add-in-02(10,4)add-put-06(2,1)addobj-init-01(4,2)instfields-nodups(0,0)is_obj-put-01(2,1)is_valid_ref-put-byte(1,0)isobj-notin-03(2,1)okfieldinits-abstract(11,3)
ac-lookup-01(1,0)add-in-03(8,3)add-putbar-rew(27,13)addobj-init-02(9,5)instfields-predef(0,0)is_obj-put-badfield(2,1)is_valid_ref-put-equiv(8,3)isobj-notin-04(2,1)okfieldinits-at(13,4)
ac-lookup-02(23,3)add-in-04(6,2)add-ref(5,2)addobj-initdone(2,1)instfields-special(0,0)is_obj-put-equiv(12,4)is_valid_ref-put-index(1,0)isobj-notin-05(2,1)okfieldinits-class(12,2)
ac-lookup-03(24,3)add-in-05(1,0)add-refin(1,0)addobj-initerror(4,2)instfields-subclass(0,0)is_obj-put-index(2,1)is_valid_ref-put-samefield(8,3)isobj-null(1,0)okfieldinits-empty(0,0)
ac-lookup-04(23,3)add-in-06(5,2)add-refs(4,3)addobj-initundone(6,3)instfields-subclass-01(5,3)is_obj-put-samefield(6,2)is_valid_ref-put-samefield-01(6,2)isobj-null-01(2,1)okfieldinits-index(12,2)
ac-lookup-05(25,4)add-in-07(1,0)add-reftype(1,1)addobj-isarray(5,2)instfields-subclass-in(3,0)is_obj-put-samefield-01(6,2)is_valid_ref-putbytearray(8,4)isobj-null-02(2,1)okfieldinits-one(5,2)
ac-lookup-06(22,4)add-in-08(8,4)add-reftype-01(4,2)addobj-isarray-01(2,1)instfields-type(3,1)is_obj-put-statfield(2,0)is_valid_ref-reftype(3,1)isobj-put(4,2)okfieldinits-rec(0,0)
ac-mode(23,3)add-in-09(10,4)add-reftype-02(4,2)addobj-keys-one(1,1)instfields-type-01(3,2)is_obj-putba(4,2)is_valid_ref-type(6,2)isobj-put-01(4,2)okstatfields-def(0,0)
ac-mode-01(26,3)add-init(1,0)add-tput(1,0)addobj-keysempty(0,0)instfields-typeex(0,0)is_obj-putbar(2,1)is_valid_ref-type-01(1,0)isobj-put-02(10,3)refcount-addobj(2,1)