wiki:external

Version 2 (modified by Mark Evenson, 8 years ago) (diff)

--

==Verification==

Java 7 Specification of verification.

http://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.10

"4.10.1. Verification by Type Checking"

classIsTypeSafe(Class) :-
    classClassName(Class, Name), 
    classDefiningLoader(Class, L),
    superclassChain(Name, L, Chain),
    Chain \= [],
    classSuperClassName(Class, SuperclassName),
    loadedClass(SuperclassName, L, Superclass),
    classIsNotFinal(Superclass),	 
    classMethods(Class, Methods), 
    checklist(methodIsTypeSafe(Class), Methods).
classIsTypeSafe(Class) :-
    classClassName(Class, 'java/lang/Object'),
    classDefiningLoader(Class, L),
    isBootstrapClassLoader(L),
    classMethods(Class, Methods), 
    checklist(methodIsTypeSafe(Class), Methods).
Verification types:

                             top
                 ____________/\____________
                /                          \
               /                            \
            oneWord                       twoWord
           /   |   \                     /       \
          /    |    \                   /         \
        int  float  reference        long        double
                     /     \
                    /       \____________
                   /                     \
                  /                       \
           uninitialized                Object
            /         \                     \
           /           \                     \
uninitializedThis  uninitialized(offset)     +----------------------+
                                             |                      |
                                             | Java class hierarchy |
                                             |                      |
                                             +----------------------+
                                                        |
                                                        |
                                                       null