Software Evolution with a Typeful Version Control System

Abstract

Agile software development comprises small evolution steps that require discipline and planning to maintain the soundness between all the components of a system. Software product lines pose similar challenges when the soundness between different branches of a product is at stake. Such challenges are usually tackled by engineering methods that focus on the development process, and not on the subject of attention, the code. The risk of code inconsistency between versions has been mostly supported by analysis of the history of releases and by evaluating feature interferences. In this paper, we propose a language-based approach to provide a certifying version control system that enables the explicit specification of the evolution steps of a software artifact throughout its life-cycle, and ensures the sane sharing of code between versions. Our model is suitable to be integrated into a smart development environment to help manage the whole code base of an application. This enables the static verification of program evolution steps, based on the correctness of state transformations between related versions, and for the stable coexistence of multiple versions at run-time. We instantiate our formal developments in a core language that extends Featherweight Java and implements the verification as a type system.