[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,
enrich classnames with
constants
predefined_classes : classnames;
functions
predef_supers : classname → classnames;
predef_superClass : classname → classname;
predicates
is_predefined_class : classname;
axioms
predef-classes
: ⊦
predefined_classes
= `java.lang.NullPointerException' .class
+ `java.lang.ArithmeticException' .class
+ `java.lang.ClassCastException' .class
+ `java.lang.ArrayStoreException' .class
+ `java.lang.NegativeArraySizeException' .class
+ `java.lang.ArrayIndexOutOfBoundsException' .class
+ `java.lang.IndexOutOfBoundsException' .class
+ `java.lang.RuntimeException' .class
+ `java.lang.NoClassDefFoundError' .class
+ `java.lang.ExceptionInInitializerError' .class
+ `java.lang.Error' .class
+ `java.lang.Exception' .class
+ `java.lang.Throwable' .class
+ (`*Array*' .class + `java.lang.Object' .class);
predefined
: ⊦
is_predefined_class(class)
↔ class = `java.lang.Object' .class ∨ class = `*Array*' .class ∨ class = `java.lang.NullPointerException' .class
∨ class = `java.lang.ArithmeticException' .class ∨ class = `java.lang.ClassCastException' .class
∨ class = `java.lang.ArrayStoreException' .class ∨ class = `java.lang.NegativeArraySizeException' .class
∨ class = `java.lang.ArrayIndexOutOfBoundsException' .class ∨ class = `java.lang.IndexOutOfBoundsException' .class
∨ class = `java.lang.NoClassDefFoundError' .class ∨ class = `java.lang.ExceptionInInitializerError' .class
∨ class = `java.lang.Error' .class ∨ class = `java.lang.RuntimeException' .class ∨ class = `java.lang.Exception' .class
∨ class = `java.lang.Throwable' .class;
lsone-01 : ⊦ ¬ `java.lang.Object' .class <_1 class;
used for : s, ls;
lsone-02 : ⊦ `*Array*' .class <_1 class ↔ class = `java.lang.Object' .class;
used for : s, ls;
lsone-03 : ⊦ `java.lang.Throwable' .class <_1 class ↔ class = `java.lang.Object' .class;
used for : s, ls;
lsone-04 : ⊦ `java.lang.Error' .class <_1 class ↔ class = `java.lang.Throwable' .class;
used for : s, ls;
lsone-05 : ⊦ `java.lang.Exception' .class <_1 class ↔ class = `java.lang.Throwable' .class;
used for : s, ls;
lsone-06 : ⊦ `java.lang.NoClassDefFoundError' .class <_1 class ↔ class = `java.lang.Error' .class;
used for : s, ls;
lsone-07 : ⊦ `java.lang.ExceptionInInitializerError' .class <_1 class ↔ class = `java.lang.Error' .class;
used for : s, ls;
lsone-08 : ⊦ `java.lang.RuntimeException' .class <_1 class ↔ class = `java.lang.Exception' .class;
used for : s, ls;
lsone-09 : ⊦ `java.lang.NullPointerException' .class <_1 class ↔ class = `java.lang.RuntimeException' .class;
used for : s, ls;
lsone-10 : ⊦ `java.lang.ArithmeticException' .class <_1 class ↔ class = `java.lang.RuntimeException' .class;
used for : s, ls;
lsone-11 : ⊦ `java.lang.ClassCastException' .class <_1 class ↔ class = `java.lang.RuntimeException' .class;
used for : s, ls;
lsone-12 : ⊦ `java.lang.ArrayStoreException' .class <_1 class ↔ class = `java.lang.RuntimeException' .class;
used for : s, ls;
lsone-13 : ⊦ `java.lang.NegativeArraySizeException' .class <_1 class ↔ class = `java.lang.RuntimeException' .class;
used for : s, ls;
lsone-14 : ⊦ `java.lang.IndexOutOfBoundsException' .class <_1 class ↔ class = `java.lang.RuntimeException' .class;
used for : s, ls;
lsone-15 : ⊦ `java.lang.ArrayIndexOutOfBoundsException' .class <_1 class ↔ class = `java.lang.IndexOutOfBoundsException' .class;
used for : s, ls;
supers-not : ⊦ ¬ is_predefined_class(class) → predef_supers(class) = [];
used for : s, ls;
supers-01 : ⊦ predef_supers(`java.lang.Object' .class) = `java.lang.Object' .class ';
used for : s, ls;
supers-02 : ⊦ predef_supers(`*Array*' .class) = `*Array*' .class + `java.lang.Object' .class;
used for : s, ls;
supers-03 : ⊦ predef_supers(`java.lang.Throwable' .class) = `java.lang.Throwable' .class + `java.lang.Object' .class;
used for : s, ls;
supers-04 : ⊦ predef_supers(`java.lang.Error' .class) = `java.lang.Error' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class);
used for : s, ls;
supers-05
: ⊦ predef_supers(`java.lang.Exception' .class) = `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class);
used for : s, ls;
supers-06
: ⊦
predef_supers(`java.lang.NoClassDefFoundError' .class)
= `java.lang.NoClassDefFoundError' .class + `java.lang.Error' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class);
used for : s, ls;
supers-07
: ⊦
predef_supers(`java.lang.ExceptionInInitializerError' .class)
= `java.lang.ExceptionInInitializerError' .class + `java.lang.Error' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class);
used for : s, ls;
supers-08
: ⊦
predef_supers(`java.lang.RuntimeException' .class)
= `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class);
used for : s, ls;
supers-09
: ⊦
predef_supers(`java.lang.NullPointerException' .class)
= `java.lang.NullPointerException' .class
+ `java.lang.RuntimeException' .class
+ `java.lang.Exception' .class
+ (`java.lang.Throwable' .class + `java.lang.Object' .class);
used for : s, ls;
supers-10
: ⊦
predef_supers(`java.lang.ArithmeticException' .class)
= `java.lang.ArithmeticException' .class
+ `java.lang.RuntimeException' .class
+ `java.lang.Exception' .class
+ (`java.lang.Throwable' .class + `java.lang.Object' .class);
used for : s, ls;
supers-11
: ⊦
predef_supers(`java.lang.ClassCastException' .class)
= `java.lang.ClassCastException' .class
+ `java.lang.RuntimeException' .class
+ `java.lang.Exception' .class
+ (`java.lang.Throwable' .class + `java.lang.Object' .class);
used for : s, ls;
supers-12
: ⊦
predef_supers(`java.lang.ArrayStoreException' .class)
= `java.lang.ArrayStoreException' .class
+ `java.lang.RuntimeException' .class
+ `java.lang.Exception' .class
+ (`java.lang.Throwable' .class + `java.lang.Object' .class);
used for : s, ls;
supers-13
: ⊦
predef_supers(`java.lang.NegativeArraySizeException' .class)
= `java.lang.NegativeArraySizeException' .class
+ `java.lang.RuntimeException' .class
+ `java.lang.Exception' .class
+ (`java.lang.Throwable' .class + `java.lang.Object' .class);
used for : s, ls;
supers-14
: ⊦
predef_supers(`java.lang.IndexOutOfBoundsException' .class)
= `java.lang.IndexOutOfBoundsException' .class
+ `java.lang.RuntimeException' .class
+ `java.lang.Exception' .class
+ (`java.lang.Throwable' .class + `java.lang.Object' .class);
used for : s, ls;
supers-15
: ⊦
predef_supers(`java.lang.ArrayIndexOutOfBoundsException' .class)
= `java.lang.ArrayIndexOutOfBoundsException' .class
+ `java.lang.IndexOutOfBoundsException' .class
+ `java.lang.RuntimeException' .class
+ `java.lang.Exception' .class
+ (`java.lang.Throwable' .class + `java.lang.Object' .class);
used for : s, ls;
superClass-not : ⊦ ¬ is_predefined_class(class) → predef_superClass(class) = `java.lang.Object' .class;
used for : s, ls;
superClass-01 : ⊦ predef_superClass(`java.lang.Object' .class) = `java.lang.Object' .class;
used for : s, ls;
superClass-02 : ⊦ predef_superClass(`*Array*' .class) = `java.lang.Object' .class;
used for : s, ls;
superClass-03 : ⊦ predef_superClass(`java.lang.Throwable' .class) = `java.lang.Object' .class;
used for : s, ls;
superClass-04 : ⊦ predef_superClass(`java.lang.Error' .class) = `java.lang.Throwable' .class;
used for : s, ls;
superClass-05 : ⊦ predef_superClass(`java.lang.Exception' .class) = `java.lang.Throwable' .class;
used for : s, ls;
superClass-06 : ⊦ predef_superClass(`java.lang.NoClassDefFoundError' .class) = `java.lang.Error' .class;
used for : s, ls;
superClass-07 : ⊦ predef_superClass(`java.lang.ExceptionInInitializerError' .class) = `java.lang.Error' .class;
used for : s, ls;
superClass-08 : ⊦ predef_superClass(`java.lang.RuntimeException' .class) = `java.lang.Exception' .class;
used for : s, ls;
superClass-09 : ⊦ predef_superClass(`java.lang.NullPointerException' .class) = `java.lang.RuntimeException' .class;
used for : s, ls;
superClass-10 : ⊦ predef_superClass(`java.lang.ArithmeticException' .class) = `java.lang.RuntimeException' .class;
used for : s, ls;
superClass-11 : ⊦ predef_superClass(`java.lang.ClassCastException' .class) = `java.lang.RuntimeException' .class;
used for : s, ls;
superClass-12 : ⊦ predef_superClass(`java.lang.ArrayStoreException' .class) = `java.lang.RuntimeException' .class;
used for : s, ls;
superClass-13 : ⊦ predef_superClass(`java.lang.NegativeArraySizeException' .class) = `java.lang.RuntimeException' .class;
used for : s, ls;
superClass-14 : ⊦ predef_superClass(`java.lang.IndexOutOfBoundsException' .class) = `java.lang.RuntimeException' .class;
used for : s, ls;
superClass-15 : ⊦ predef_superClass(`java.lang.ArrayIndexOutOfBoundsException' .class) = `java.lang.IndexOutOfBoundsException' .class;
used for : s, ls;
end enrich