Login (DCU Staff Only)
Login (DCU Staff Only)

DORAS | DCU Research Repository

Explore open access research and scholarly works from DCU

Advanced Search

Data Refinement in Object-Oriented Verification

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:

[thumbnail of THESISRM.PDF]
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