• English
    • Norsk
  • English 
    • English
    • Norsk
  • Administration
View Item 
  •   Home
  • Det matematisk-naturvitenskapelige fakultet
  • Institutt for informatikk
  • Institutt for informatikk
  • View Item
  •   Home
  • Det matematisk-naturvitenskapelige fakultet
  • Institutt for informatikk
  • Institutt for informatikk
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Lazy behavioral subtyping

Dovland, Johan; Johnsen, Einar B.; Owe, Olaf; Steffen, Martin
Research report
View/Open
Report368.pdf (211.6Kb)
Year
2007
Permanent link
http://urn.nb.no/URN:NBN:no-18810

Is part of
Research report
Metadata
Show metadata
Appears in the following Collection
  • Institutt for informatikk [3652]
Abstract
Late binding allows flexible code reuse but complicates formal reasoning significantly, as a method call’s receiver class is not statically known. This is especially true when programs are incrementally developed by extending class hierarchies. This report develops a novel method to reason about late bound method calls. In contrast to traditional behavioral subtyping, reverification is avoided without restricting method overriding to fully behavior-preserving redefinition. The approach ensures that when analyzing the methods of a class, it suffices to consider that class and its superclasses. Thus, the full class hierarchy is not needed, and incremental reasoning is supported. We formalize this approach as a calculus which lazily imposes context-dependent subtyping constraints on method definitions. The calculus ensures that all method specifications required by late bound calls remain satisfied when new classes extend a class hierarchy. The calculus does not depend on a specific program logic, but the examples in the report use a Hoare-style proof system. We show soundness of the analysis method.
 
Responsible for this website 
University of Oslo Library


Contact Us 
duo-hjelp@ub.uio.no


Privacy policy
 

 

For students / employeesSubmit master thesisAccess to restricted material

Browse

All of DUOCommunities & CollectionsBy Issue DateAuthorsTitlesThis CollectionBy Issue DateAuthorsTitles

For library staff

Login
RSS Feeds
 
Responsible for this website 
University of Oslo Library


Contact Us 
duo-hjelp@ub.uio.no


Privacy policy