A transformational proof system for delta-oriented programming
A transformational proof system for delta-oriented programming
复制标题
面向增量编程的转换证明系统
DOI：
10.1145/2364412.2364422
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Ingrid Chieh Yu
中科院分区：
文献类型：
--
作者：
Ferruccio Damiani;Olaf Owe;Johan Dovland;Ina Schaefer;E. Johnsen;Ingrid Chieh Yu
面向增量的编程是一种模块化的，但灵活的技术，以实现软件产品线。为了有效地验证产品线的所有可能的产品变体的规格，生成所有产品变体并单独验证它们通常是不可行的。为了解决这个问题，我们提出了一个转换证明系统中的规格在一个三角洲模块描述以前的规格的变化。我们的方法允许每个三角洲模块进行验证隔离，基于符号假设调用的方法，可能在其他三角洲模块。当从delta模块生成产品变体时，这些假设通过所考虑的产品变体中的方法的实际保证来实例化，并用于导出该产品变体的规格。
Delta-oriented programming is a modular, yet flexible technique to implement software product lines. To efficiently verify the specifications of all possible product variants of a product line, it is usually infeasible to generate all product variants and to verify them individually. To counter this problem, we propose a transformational proof system in which the specifications in a delta module describe changes to previous specifications. Our approach allows each delta module to be verified in isolation, based on symbolic assumptions for calls to methods which may be in other delta modules. When product variants are generated from delta modules, these assumptions are instantiated by the actual guarantees of the methods in the considered product variant and used to derive the specifications of this product variant.