| Summary: | Complex systems are naturally understood as combinations of their
distinguishing characteristics or \definit{features}. Distinct features
differentiate between variations of configurable systems and also
identify the novelties of extensions. The implementation of a
conceptual feature is often scattered throughout an artifact, forcing
designers to understand the entire artifact in order to reason about
the behavior of a single feature. It is particularly challenging to
independently develop novel extensions to complex systems as a
result.
This dissertation shows how to modularly reason about the
implementation of conceptual features in both the formalizations of
programming languages and object-oriented software product lines. In
both domains, modular verification of features can be leveraged to
reason about the behavior of artifacts in which they are included:
fully mechanized metatheory proofs for programming languages can be
synthesized from independently developed proofs, and programs built
from well-formed feature modules are guaranteed to be well-formed
without needing to be typechecked. Modular reasoning about individual
features can furthermore be used to efficiently reason about families
of languages and programs which share a common set of features. === text
|
|---|
