A Transformational Proof System for Delta-Oriented Programming

Delta-oriented programming is a modular, yet flexible technique to implement software product lines. To efficiently verify the specications 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 specications in a delta module describe changes to previous specications. Our approach allows each delta module to be veried 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 specications of this product variant.