Verifying JVMO - JVM

We instantiate the diligentScheme by the trustfulVMO and the extension of the verifySchemeC by succO and checkO.

Veri_cation of JVMO code has to consider, in a run-time independent way, the impact of instance methods and instance _elds, of subtypes, and of object initialization. Checking instance methods and instance _elds raises no new problem but requires slight modi_cations. The most obvious is, that the initialization of the veri_er must be adapted to prepend the target reference of instance methods and constructors before the parameter types. For a constructor not in class Object the target reference has type InInit. In all other cases the type of the target reference is the class of the method. The derived function formals is therefore re_ned by:

Because of the subtype relation two di_erent class types can be merged to a common ancestor in the class tree and not to the type unusable as in the case of primitive types. A common ancestor of two class types, however, can also be an interface type. In general, two reference types can have several least ancestor types. Therefore we work with sets of reference types. The least upper bound t of two sets of reference types with respect to the compatibility relation v is simply their union. rs1 t rs2 = rs1 [ rs2

The least upper bound of a set of reference types and a verify type which is not a set of reference types is the type unusable.

The diligentVMO is obtained by instantiating the diligentScheme with the check function checkO, the successor function succO and the trustfulVMO.

Reference types require that instructions might be checked several times. Nevertheless, the veri_cation process terminates. The type states can be merged only a _nite number of times: the domains of the type state functions are _nite and the number of reference types in a program is _nite.

All rights reserved © 2018 Wisdom IT Services India Pvt. Ltd Protection Status

JVM Topics