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.
CITATION STYLE
Yatake, K., Aoki, T., & Katayama, T. (2005). Implementing application-specific object-oriented theories in HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3722 LNCS, pp. 501–516). https://doi.org/10.1007/11560647_33
Mendeley helps you to discover research relevant for your work.