一句话：提出形式框架统一比较静态可变性语言的表达力，并在 Agda 中机器化验证其可靠性与完备性。
软件可变性广泛存在，但用于静态（编译期）可变性建模的多种形式语言长期缺乏系统比较，其相互包含关系与适用场景不明。本文提出一个形式化框架，以公共语义域捕捉显式可变性的直觉，并定义可变性语言的可靠性、完备性与表达力等性质。作者证明了一系列现有语言的（非）可靠性与（非）完备性，并刻画它们表达同一可变系统的能力。该框架被实现为可扩展的开源 Agda 库，证明同时充当语言间正确编译器或差分算法。结果显示不同语言具有不同表达力层级，存在相对统一语义域完备或不完备的语言，其中 choice calculus 属于表达力最强的语言之一。
Variability permeates software development to satisfy ever-changing requirements and mass-customization needs. A prime example is the Linux kernel, which employs the C preprocessor to specify a set of related but distinct kernel variants. To study, analyze, and verify variational software, several formal languages have been proposed. For example, the choice calculus has been successfully applied for type checking and symbolic execution of configurable software, while other formalisms have been used for variational model checking, change impact analysis, among other use cases. Yet, these languages have not been formally compared, hence, little is known about their relationships. Crucially, it is unclear to what extent one language subsumes another, how research results from one language can be applied to other languages, and which language is suitable for which purpose or domain. In this paper, we propose a formal framework to compare the expressive power of languages for static (i.e. compile-time) variability. By establishing a common semantic domain to capture a widely used intuition of explicit variability, we can formulate the basic, yet to date neglected, properties of soundness, completeness, and expressiveness for variability languages. We then prove the (un)soundness and (in)completeness of a range of existing languages, and relate their ability to express the same variational systems. We implement our framework as an extensible open source Agda library in which proofs act as correct compilers between languages or differencing algorithms. We find different levels of expressiveness as well as complete and incomplete languages w.r.t. our unified semantic domain, with the choice calculus being among the most expressive languages.
@article{BittnerSMYTWAT24,
title = {On the Expressive Power of Languages for Static Variability},
author = {Paul Maximilian Bittner and Alexander Schultheiß and Benjamin Moosherr and Jeffrey M. Young and Leopoldo Teixeira and Eric Walkingshaw and Parisa Ataei and Thomas Thüm},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689747}
}