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
| Identifer | oai:union.ndltd.org:UTEXAS/oai:repositories.lib.utexas.edu:2152/22867 |
| Date | 15 January 2014 |
| Creators | Delaware, Benjamin James |
| Source Sets | University of Texas |
| Language | en_US |
| Detected Language | English |
| Format | application/pdf |
Page generated in 0.0021 seconds