Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6874855 | Journal of Logical and Algebraic Methods in Programming | 2018 | 21 Pages |
Abstract
This 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.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Crystal Chang Din, Einar Broch Johnsen, Olaf Owe, Ingrid Chieh Yu,