Invariants generation for method overriding using abstract interpretation / Siti Hafizah Ab. Hamid
Software verification is an important element of software reliability. The significance and importance of verification have been recognized by Bill Gates in his speech in WinHEC 2002. The software verification allows program’s specification to be formally proved to ensure the specification verified...
| Main Author: | |
|---|---|
| Format: | Thesis |
| Published: |
2013
|
| Subjects: | |
| Online Access: | http://studentsrepo.um.edu.my/5552/ http://studentsrepo.um.edu.my/5552/1/PhD_Thesis_WHA070027.pdf |
| _version_ | 1848772918594502656 |
|---|---|
| author | Ab. Hamid, Siti Hafizah |
| author_facet | Ab. Hamid, Siti Hafizah |
| author_sort | Ab. Hamid, Siti Hafizah |
| building | UM Research Repository |
| collection | Online Access |
| description | Software verification is an important element of software reliability. The significance and importance of verification have been recognized by Bill Gates in his speech in WinHEC 2002. The software verification allows program’s specification to be formally proved to ensure the specification verified the program before its execution time using static analysis. However, in the context of object-oriented program, studies show there is a need to have formal specifications for method overriding because the overriding feature plays important role in allowing program reusability. This thesis develops an abstract
formal framework for invariant generation of static analysis for method overriding in object-oriented program using inheritance. It focuses on late bound method in the class invariants generation. There are two main problems arise during the process of generating class invariant which are reverification of class invariant and over-approximation of late binding call. In the context of method overriding, the problem of late binding call happens
when the abstract semantic function uses behavioral subtyping that is restricted to the rule of contravariance and covariance. The abstract formal framework using abstract
interpretation theory is proposed to overcome the problem above. The framework exploits the capability of abstract interpretation method in making program analysis automated. It also overcomes the problem of generating the invariants for late binding call of method overriding with less restrictions rules of lazy behavioral subtyping method. The use of lazy behavioral subtyping results to the overridden method semantics has a not over approximated invariant. The framework produces two equations for two invariants, which
are modular invariants for inheritance and invariants for method overriding. A scenario based evaluation is conducted to validate the invariants and to compare the proposed
framework using lazy behavioral subtyping with the framework using behavioral subtyping. |
| first_indexed | 2025-11-14T13:34:09Z |
| format | Thesis |
| id | um-5552 |
| institution | University Malaya |
| institution_category | Local University |
| last_indexed | 2025-11-14T13:34:09Z |
| publishDate | 2013 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | um-55522015-06-15T04:33:28Z Invariants generation for method overriding using abstract interpretation / Siti Hafizah Ab. Hamid Ab. Hamid, Siti Hafizah QA76 Computer software Software verification is an important element of software reliability. The significance and importance of verification have been recognized by Bill Gates in his speech in WinHEC 2002. The software verification allows program’s specification to be formally proved to ensure the specification verified the program before its execution time using static analysis. However, in the context of object-oriented program, studies show there is a need to have formal specifications for method overriding because the overriding feature plays important role in allowing program reusability. This thesis develops an abstract formal framework for invariant generation of static analysis for method overriding in object-oriented program using inheritance. It focuses on late bound method in the class invariants generation. There are two main problems arise during the process of generating class invariant which are reverification of class invariant and over-approximation of late binding call. In the context of method overriding, the problem of late binding call happens when the abstract semantic function uses behavioral subtyping that is restricted to the rule of contravariance and covariance. The abstract formal framework using abstract interpretation theory is proposed to overcome the problem above. The framework exploits the capability of abstract interpretation method in making program analysis automated. It also overcomes the problem of generating the invariants for late binding call of method overriding with less restrictions rules of lazy behavioral subtyping method. The use of lazy behavioral subtyping results to the overridden method semantics has a not over approximated invariant. The framework produces two equations for two invariants, which are modular invariants for inheritance and invariants for method overriding. A scenario based evaluation is conducted to validate the invariants and to compare the proposed framework using lazy behavioral subtyping with the framework using behavioral subtyping. 2013 Thesis NonPeerReviewed application/pdf http://studentsrepo.um.edu.my/5552/1/PhD_Thesis_WHA070027.pdf Ab. Hamid, Siti Hafizah (2013) Invariants generation for method overriding using abstract interpretation / Siti Hafizah Ab. Hamid. PhD thesis, University of Malaya. http://studentsrepo.um.edu.my/5552/ |
| spellingShingle | QA76 Computer software Ab. Hamid, Siti Hafizah Invariants generation for method overriding using abstract interpretation / Siti Hafizah Ab. Hamid |
| title | Invariants generation for method overriding using abstract interpretation / Siti Hafizah Ab. Hamid |
| title_full | Invariants generation for method overriding using abstract interpretation / Siti Hafizah Ab. Hamid |
| title_fullStr | Invariants generation for method overriding using abstract interpretation / Siti Hafizah Ab. Hamid |
| title_full_unstemmed | Invariants generation for method overriding using abstract interpretation / Siti Hafizah Ab. Hamid |
| title_short | Invariants generation for method overriding using abstract interpretation / Siti Hafizah Ab. Hamid |
| title_sort | invariants generation for method overriding using abstract interpretation / siti hafizah ab. hamid |
| topic | QA76 Computer software |
| url | http://studentsrepo.um.edu.my/5552/ http://studentsrepo.um.edu.my/5552/1/PhD_Thesis_WHA070027.pdf |