dc.date.accessioned | 2013-03-12T08:14:29Z | |
dc.date.available | 2013-03-12T08:14:29Z | |
dc.date.issued | 2007 | en_US |
dc.date.submitted | 2008-03-28 | en_US |
dc.identifier.uri | http://hdl.handle.net/10852/9861 | |
dc.description.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. | nor |
dc.language.iso | eng | en_US |
dc.relation.ispartof | Research report http://urn.nb.no/URN:NBN:no-35645 | en_US |
dc.relation.uri | http://urn.nb.no/URN:NBN:no-35645 | |
dc.title | Lazy behavioral subtyping | en_US |
dc.type | Research report | en_US |
dc.date.updated | 2008-04-04 | en_US |
dc.creator.author | Dovland, Johan | en_US |
dc.creator.author | Johnsen, Einar B. | en_US |
dc.creator.author | Owe, Olaf | en_US |
dc.creator.author | Steffen, Martin | en_US |
dc.subject.nsi | VDP::420 | en_US |
dc.identifier.urn | URN:NBN:no-18810 | en_US |
dc.type.document | Forskningsrapport | en_US |
dc.identifier.duo | 71311 | en_US |
dc.identifier.bibsys | 080525946 | en_US |
dc.identifier.fulltext | Fulltext https://www.duo.uio.no/bitstream/handle/10852/9861/1/Report368.pdf | |