This paper presents a theory of Object-Oriented concepts embedded shallowly in HOL for the verification of OO analysis models. The theory is application-specific in the sense that it is automatically constructed depending on the type information of the application. This allows objects to have attributes of arbitrary types, making it possible to verify models using not only basic types but also highly abstracted types specific to the target domain. The theory is constructed by definitional extension based on the operational semantics of a heap memory model, which guarantees the soundness of the theory. This paper mainly focuses on the implementation details of the theory. © Springer-Verlag Berlin Heidelberg 2005.

Yatake K., Aoki T., Katayama T.

717.pdf    Gửi cho bạn bè

Từ khóa : Information theory; Mathematical models; Semantics; Storage allocation (computer); Definitional extensions; Heap memory models; Object-oriented theories; Operational semantics; Object oriented programming