Return to search

Feature modularity in mechanized reasoning

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

Identiferoai:union.ndltd.org:UTEXAS/oai:repositories.lib.utexas.edu:2152/22867
Date15 January 2014
CreatorsDelaware, Benjamin James
Source SetsUniversity of Texas
Languageen_US
Detected LanguageEnglish
Formatapplication/pdf

Page generated in 0.0018 seconds