Modularizing Theorems for Software Product Lines: The Jbook Case Study
Modularizing Theorems for Software Product Lines: The Jbook Case Study
复制标题
软件产品线的模块化定理：Jbook 案例研究
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
E. Börger
中科院分区：
文献类型：
--
作者：
D. Batory;E. Börger
软件产品线的一个目标是在一系列程序中经济地组装程序。在本文中，我们将探讨如何定理的程序属性可以集成到基于功能的开发软件产品线。作为一个案例研究，我们分析了现有的Java/JVM编译正确性证明的定义，解释，编译和执行字节码的Java语言。我们展示了如何功能模块化的程序源代码，定理语句及其证明。通过组合特征，程序的源代码、定理陈述和证明被组合在一起。本文的研究揭示了基于抽象状态机（ASM）的系统开发和软件产品线的面向对象编程（FOP）中所使用的精化概念的惊人相似性。我们建议利用这一观察结果，在两个社区的研究人员富有成效的互动。
A goal of software product lines is the economical assembly of programs in a family of programs. In this paper, we explore how theorems about program properties may be integrated into feature-based development of software product lines. As a case study, we analyze an existing Java/JVM compilation correctness proof for defining, interpreting, compiling, and executing bytecode for the Java language. We show how features modularize program source, theorem statements and their proofs. By composing features, the source code, theorem statements and proofs for a program are assembled. The investigation in this paper reveals a striking similarity of the refinement concepts used in Abstract State Machines (ASM) based system development and Feature-Oriented Programming (FOP) of software product lines. We suggest to exploit this observation for a fruitful interaction of researchers in the two communities.