Hide metadata

dc.date.accessioned2013-03-12T08:04:44Z
dc.date.available2013-03-12T08:04:44Z
dc.date.issued2007en_US
dc.date.submitted2008-03-26en_US
dc.identifier.urihttp://hdl.handle.net/10852/9860
dc.description.abstractCurrent object-oriented approaches to distributed programs may be criticized in several respects. First, method calls are generally synchronous, which leads to much waiting in distributed and unstable networks. Second, the common model of thread concurrency makes reasoning about program behavior very challenging. Object-oriented models based on concurrent objects communicating by asynchronous method calls, have been proposed to combine object orientation and distribution in a more satisfactory way. In this report, a high-level language and proof system are developed for such a model, emphasizing simplicity and modularity. In particular, the proof system is used to derive external specifications of observable behavior for objects, encapsulating their state. A simple and compositional proof system is paramount to allow verification of real programs. The proposed proof rules are derived from the Hoare rules of a standard sequential language by a semantic encoding preserving soundness and relative completeness. Thus, the report demonstrates that these models not only address the first criticism above, but also the second.nor
dc.language.isoengen_US
dc.relation.ispartofResearch report http://urn.nb.no/URN:NBN:no-35645en_US
dc.relation.urihttp://urn.nb.no/URN:NBN:no-35645
dc.titleA compositional proof system for dynamic object systemsen_US
dc.typeResearch reporten_US
dc.date.updated2008-03-31en_US
dc.creator.authorDovland, Johanen_US
dc.creator.authorJohnsen, Einar B.en_US
dc.creator.authorOwe, Olafen_US
dc.subject.nsiVDP::420en_US
dc.identifier.urnURN:NBN:no-18788en_US
dc.type.documentForskningsrapporten_US
dc.identifier.duo71231en_US
dc.identifier.bibsys080489923en_US
dc.identifier.fulltextFulltext https://www.duo.uio.no/bitstream/handle/10852/9860/1/Report351.pdf


Files in this item

Appears in the following Collection

Hide metadata