{"id":{"repo_id":"dcu","oai_identifier":"oai:doras.dcu.ie:15718"},"canonical_url":"https://search.dev.ndltd.org/etd/dcu/oai:doras.dcu.ie:15718","repository":{"repo_id":"dcu","name":"Dublin City University","base_url":"http://doras.dcu.ie/cgi/oai2"},"display":{"title":"Data Refinement in Object-Oriented Verification","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Monahan, Rosemary"],"institution":"Dublin City University","degree_name":"phd","degree_level":"doctoral","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2010,"date_issued":"2010-09","date_published":"2010-09","updated_at":"2026-07-24T06:26:25Z","subjects":["Computer software","Software engineering"],"languages":["en"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":null,"outbound_label":null,"outbound_source":null},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Monahan, Rosemary"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2010-09-22"]},{"key":"dc:date.issued","label":"Date","values":["2010-09"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["Dublin City University"]},{"key":"dc:relation.isreferencedby","label":"Dc Relation Isreferencedby","values":["https://doras.dcu.ie/15718/"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["doctoral"]},{"key":"dc:type.qualificationname","label":"Dc Type Qualificationname","values":["phd"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer software","Software engineering"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://doras.dcu.ie/15718/1/THESISRM.PDF"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Data Refinement in Object-Oriented Verification"]}]}],"canonical_facts":{"dc:creator":["Monahan, Rosemary"],"dc:date":["2010-09-22"],"dc:date.issued":["2010-09"],"dc:description.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."],"dc:format":["application/pdf"],"dc:identifier.uri":["https://doras.dcu.ie/15718/1/THESISRM.PDF"],"dc:language":["en"],"dc:publisher.institution":["Dublin City University"],"dc:relation.isreferencedby":["https://doras.dcu.ie/15718/"],"dc:subject":["Computer software","Software engineering"],"dc:title":["Data Refinement in Object-Oriented Verification"],"dc:type":["Thesis"],"dc:type.qualificationlevel":["doctoral"],"dc:type.qualificationname":["phd"]},"updated_at":"2026-07-24T06:26:25Z"}