Modular subclass verification: Safely creating correct subclasses without superclass code

dc.contributor.author Ruby, Clyde
dc.contributor.department Computer Science
dc.date 2018-02-14T00:26:12.000
dc.date.accessioned 2020-06-30T01:56:19Z
dc.date.available 2020-06-30T01:56:19Z
dc.date.issued 2006-12-01
dc.description.abstract <p>The documentation of object-oriented frameworks and class libraries needs to provide enough information so programmers can reason about the correctness of subclass methods without superclass code. Even though a superclass method satisfies its specification and behaves properly in the context of the superclass itself, a new subclass may cause that method to have unexpected or unverifiable behavior. For example, inherited superclass code can call down to subclass methods which may cause a superclass method to no longer satisfy its specification. Furthermore, without superclass code, downcalls can result in unverifiable side-effects. Aliasing can also result in unexpected or unverifiable side-effects. In this dissertation, we present a reasoning technique that allows programmers, who have no access to superclass code, to avoid the problems caused by downcalls and aliasing. The rules use the specification of the abstract data representation of a class and the frame axiom of each method to determine when a method override is necessary and when verifiers can safely reason about the behavior of super-calls. We describe a type system and propose a tool that would warn when a super-call is unsafe or when a superclass method needs to be overridden. A verification logic is also presented and proved sound. The verification logic is based on specifications given in the Java Modeling Language (JML) and uses superclass and subclass specifications to modularly verify the correctness of subclass code. A set of guidelines is proposed for class library implementers that, if followed, guarantees that superclass methods will always be safe to call and that our verification logic can safely be used. These guidelines make our technique easy to use in practice.</p>
dc.identifier archive/lib.dr.iastate.edu/cs_techreports/274/
dc.identifier.articleid 1299
dc.identifier.contextkey 5494216
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath cs_techreports/274
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/20099
dc.source.bitstream archive/lib.dr.iastate.edu/cs_techreports/274/TR.pdf|||Fri Jan 14 23:07:11 UTC 2022
dc.subject.disciplines Programming Languages and Compilers
dc.subject.disciplines Software Engineering
dc.subject.disciplines Theory and Algorithms
dc.subject.keywords Downcalls
dc.subject.keywords super-calls
dc.subject.keywords subclass
dc.subject.keywords semantic fragile subclassing problem
dc.subject.keywords subclassing contract
dc.subject.keywords code contract
dc.subject.keywords specification inheritance
dc.subject.keywords method refinement
dc.subject.keywords alias control
dc.subject.keywords specification of side effects
dc.subject.keywords Java language
dc.subject.keywords JML language
dc.title Modular subclass verification: Safely creating correct subclasses without superclass code
dc.type article
dc.type.genre article
dspace.entity.type Publication
relation.isOrgUnitOfPublication f7be4eb9-d1d0-4081-859b-b15cee251456
File
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
TR.pdf
Size:
2.84 MB
Format:
Adobe Portable Document Format
Description:
Collections