DIKUL - logo
E-resources
Full text
  • Enhancing program verificat...
    Xing, Cong-Cong

    Proceedings of the 2006 ACM symposium on Applied computing, 04/2006
    Conference Proceeding

    Object types are abstract specifications of object behaviors; object behaviors are abstractly indicated by object component interdependencies; and program verifications are based on object behaviors. In conventional object type systems, object component interdependencies are not taken into account. As a result, distinct behaviors of objects are confused, which can lead to fundamental typing/subtyping loopholes and program verification troubles. In this paper, we first identify a program verification problem which is caused by the loose conventional object typing/subtyping which is in turn caused by the overlooking of object component interdependencies. Then, as a new object typing scheme, we introduce object type graphs (OTG) in which object component interdependencies are integrated into object types. Finally, we show how the verification problem can be resolved under OTG.