JUCS - Journal of Universal Computer Science 14(12): 2059-2082, doi: 10.3217/jucs-014-12-2059
Modularizing Theorems for Software Product Lines: The Jbook Case Study
expand article infoDon Batory‡, Egon Börger§
‡ University of Texas at Austin, Austin, United States of America§ University of Pisa, Pisa, Italy

Corresponding author: Don Batory ( batory@cs.utexas.edu )

© Don Batory, Egon Börger.
This article is freely available under the J.UCS Open Content License.
Citation: Batory D, Börger E (2008) Modularizing Theorems for Software Product Lines: The Jbook Case Study. JUCS - Journal of Universal Computer Science 14(12): 2059-2082. https://doi.org/10.3217/jucs-014-12-2059
Open Access
Abstract
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.
Keywords
ASM, features, composition, verification, AHEAD