Verifying traits: an incremental proof system for fine-grained reuse
Verifying traits: an incremental proof system for fine-grained reuse
复制标题
验证特征：用于细粒度重用的增量证明系统
DOI：
10.1007/s00165-013-0278-3
复制
发表时间：
2014
影响因子：
1
通讯作者：
Ina Schaefer
中科院分区：
文献类型：
--
作者：
Ferruccio Damiani;Johan Dovland;Einar Broch Johnsen;Ina Schaefer
在面向对象编程中，Traits被认为是一种比类继承更灵活的结构化代码机制，以实现细粒度的代码重用。最初为一个目的开发的特性可以在完全不同的环境中进行调整和重用。trait的形式化已经被广泛研究，trait的实现已经开始出现在编程语言中。到目前为止，正式建立基于特质的程序的属性的工作主要集中在类型系统上。本文提出了第一个基于特征的面向对象语言的演绎证明系统。如果一个特征的规范可以先验地给出，覆盖该特征的所有实际使用，那么我们的证明系统是模块化的，因为每个特征只分析一次。然而，在许多情况下，强加这样的限制可能不必要地限制了trait作为灵活代码重用的机制。为了反映特征的灵活重用潜力，我们的证明系统还允许新的规范被添加到一个特征中，这并不违反已建立的证明。我们形式化和证明系统的可靠性。
Traits have been proposed as a more flexible mechanism than class inheritance for structuring code in object-oriented programming, to achieve fine-grained code reuse. A trait originally developed for one purpose can be adapted and reused in a completely different context. Formalizations of traits have been extensively studied, and implementations of traits have started to appear in programming languages. So far, work on formally establishing properties of trait-based programs has mostly concentrated on type systems. This paper presents the first deductive proof system for a trait-based object-oriented language. If a specification of a trait can be given a priori, covering all actual usage of that trait, our proof system is modular as each trait is analyzed only once. However, imposing such a restriction may in many cases unnecessarily limit traits as a mechanism for flexible code reuse. In order to reflect the flexible reuse potential of traits, our proof system additionally allows new specifications to be added to a trait in anincrementalway which does not violate established proofs. We formalize and show the soundness of the proof system.
登录
查看更多内容
基本 AOP：微积分
DOI：
--
发表时间：
2010
期刊：
TOPL
影响因子：
--
作者：
B. D. Fraine;Erik Ernst;Mario Südholt
通讯作者：
Mario Südholt
验证特征：细粒度重用的证明系统
DOI：
--
发表时间：
2011
期刊：
FTfJP@ECOOP
影响因子：
--
作者：
Ferruccio Damiani;Johan Dovland;E. Johnsen;Ina Schaefer
通讯作者：
Ina Schaefer
DOI：
10.1145/2364412.2364422
发表时间：
2012
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
Ferruccio Damiani;Olaf Owe;Johan Dovland;Ina Schaefer;E. Johnsen;Ingrid Chieh Yu
通讯作者：
Ingrid Chieh Yu
面向 Delta 编程的 Liskov 原理
DOI：
10.1007/978-3-642-34026-0_4
发表时间：
2012
期刊：
Software - Practice and Experience
影响因子：
--
作者：
Reiner Hähnle;Ina Schaefer
通讯作者：
Ina Schaefer
类 Java 环境中框和特征的微积分
DOI：
10.1007/978-3-642-13414-2_4
发表时间：
2010
期刊：
Proceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences
影响因子：
--
作者：
Lorenzo Bettini;Ferruccio Damiani;M. D. Luca;Kathrin Geilmann;Jan Schäfer
通讯作者：
Jan Schäfer