In feature-oriented software development, software product lines are defined as families of systems where features encapsulate incremental or optional behaviors. There are mainly two different approaches for specifying feature-oriented systems: either annotative of compositional, i.e., either guarding code by presence conditions over features or specifying components for each feature along with a composition operation. Both approaches have their merits and downsides with respect to, among others, separation of concerns, granularity, extensibility, and analyzability. One challenge posed by Apel and Kästner already in 2008 is to establish a hybrid approach that is both annotative and compositional, uniting the benefits of both approaches. In this talk, I will face this challenge from a formal perspective and illustrate how such a hybrid approach can be achieved for feature-oriented systems specified in a variant of Dijkstra’s guarded command language. I will present extensions, further benefits for formal analysis of feature-oriented systems, and how the results can be transferred back to the field of feature-oriented software development.