Verifying traits: a proof system for fine-grained reuse
Verifying traits: a proof system for fine-grained reuse
复制标题
验证特征：细粒度重用的证明系统
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Ina Schaefer
中科院分区：
文献类型：
--
作者：
Ferruccio Damiani;Johan Dovland;E. Johnsen;Ina Schaefer
在面向对象编程中，Traits被认为是一种比类继承更灵活的代码结构化机制，可以实现细粒度的代码重用。最初为一个目的开发的特性可以在完全不同的上下文中修改和重用。trait的形式化已经被广泛研究，trait的实现已经开始出现在编程语言中。然而，正式建立基于特质的程序的属性的工作到目前为止主要集中在类型系统上。本文提出了第一个基于特征的面向对象语言的演绎证明系统。如果一个特征的规范可以先验地给出，覆盖该特征的所有实际使用，那么我们的证明系统是模块化的，因为每个特征只分析一次。为了反映特征的灵活重用潜力，我们的证明系统还允许以增量的方式将新的规范添加到特征中，而不会违反已建立的证明。我们形式化和证明系统的可靠性。
Traits have been proposed as a more flexible mechanism for code structuring in object-oriented programming than class inheritance, for achieving fine-grained code reuse. A trait originally developed for one purpose can be modified 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. However, work on formally establishing properties of trait-based programs has so far mostly concentrated on type systems. This paper proposes the first deductive proof system for a trait-based object-oriented language. If a specification for 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. In order to reflect the flexible reuse potential of traits, our proof system additionally allows new specifications to be added to a trait in an incremental way which does not violate established proofs. We formalize and show the soundness of the proof system.