Monahan, Rosemary (2010) Data Refinement in Object-Oriented Verification. PhD thesis, Dublin City University.
Abstract
Data refinement is a special instance of refinement where a specification is refined by replacing the data type used in the specification. The theory of data refinement guarantees that this replacement does not adversely affect the functional behaviour of the programs that use these specifications.
Object-oriented programming languages such as JML and Spec# support the specification and verification of object-oriented programs. We research their capabilities, identifying their strengths and weaknesses from both a specification and a tool-support point of view. This leads us to the conclusion that object-oriented specification languages should support a view of objects that abstracts away from the implementation details. We examine the specification and verification of programs that are written in this way, making use of existing language features, so that data refinements can be verified using existing verification tools.
We propose a framework for the specification and verification of modular data refinement within an object-oriented environment. Objects are specified in terms of one data type and implemented in terms of another. Clients who interact with these objects are never concerned with the underlying implementation details as they interact directly with the abstract specification. A proof-of-concept tool is developed to demonstrate the viability and effectiveness of our proposed framework. This tool takes the form of an application that checks whether or not a program conforms to our framework for the modular data refinement of object-oriented programs.
Metadata
Item Type: | Thesis (PhD) |
---|---|
Date of Award: | 22 September 2010 |
Refereed: | No |
Supervisor(s): | Morris, Joseph |
Subjects: | Computer Science > Computer software Computer Science > Software engineering |
DCU Faculties and Centres: | DCU Faculties and Schools > Faculty of Engineering and Computing > School of Computing |
Use License: | This item is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 3.0 License. View License |
ID Code: | 15718 |
Deposited On: | 04 Apr 2011 15:25 by David Sinclair . Last Modified 19 Jul 2018 14:51 |
Documents
Full text available as:
Preview |
PDF
- Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
516kB |
Downloads
Downloads
Downloads per month over past year
Archive Staff Only: edit this record