Hide metadata

dc.date.accessioned2019-12-10T20:11:33Z
dc.date.available2019-12-10T20:11:33Z
dc.date.created2018-03-07T21:25:42Z
dc.date.issued2018
dc.identifier.citationDin, Crystal Chang Johnsen, Einar Broch Owe, Olaf Yu, Ingrid Chieh . A modular reasoning system using uninterpreted predicates for code reuse. Journal of Logical and Algebraic Methods in Programming. 2018, 95, 82-102
dc.identifier.urihttp://hdl.handle.net/10852/71545
dc.description.abstractThis paper proposes a modular proof system based on uninterpreted predicates. The proposed proof system allows modular reasoning about programs with an open-world assumption, which goes beyond behavioral subtyping. The proof system enables modular reasoning about languages with very flexible code reuse mechanisms, such as traits and deltas in the context of object-oriented programming. Whereas related work on incremental proof systems prove soundness in terms of internal consistency, this paper establishes both soundness and relative completeness of the proposed proof system by relating it to a standard proof system for a simple object-oriented language. The applicability of the approach is demonstrated on different code reuse mechanisms: unrestricted class inheritance, delta-oriented programming, and trait-based programming.
dc.languageEN
dc.titleA modular reasoning system using uninterpreted predicates for code reuse
dc.typeJournal article
dc.creator.authorDin, Crystal Chang
dc.creator.authorJohnsen, Einar Broch
dc.creator.authorOwe, Olaf
dc.creator.authorYu, Ingrid Chieh
cristin.unitcode185,15,5,32
cristin.unitnamePålitelige systemer
cristin.ispublishedtrue
cristin.fulltextpreprint
cristin.qualitycode2
dc.identifier.cristin1571286
dc.identifier.bibliographiccitationinfo:ofi/fmt:kev:mtx:ctx&ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.jtitle=Journal of Logical and Algebraic Methods in Programming&rft.volume=95&rft.spage=82&rft.date=2018
dc.identifier.jtitleJournal of Logical and Algebraic Methods in Programming
dc.identifier.volume95
dc.identifier.startpage82
dc.identifier.endpage102
dc.identifier.doihttps://doi.org/10.1016/j.jlamp.2017.11.004
dc.identifier.urnURN:NBN:no-74647
dc.type.documentTidsskriftartikkel
dc.source.issn2352-2216
dc.identifier.fulltextFulltext https://www.duo.uio.no/bitstream/handle/10852/71545/1/main.pdf
dc.type.versionSubmittedVersion
dc.relation.projectNFR/240614
dc.relation.projectNFR/237898


Files in this item

Appears in the following Collection

Hide metadata