• adaptivity
• context-oriented programming
• programming languages
• static analysis

Adaptive systems modify their behaviour in order to run always and everywhere. Their
structure is therefore subject to continuous changes, which however could compromise
the correct behaviour of applications and break the guarantees on their non-functional
requirements. Effective mechanisms are thus required to adapt software to the new
added functionalities and to changes of the operational environment, namely the context in which applications are plugged in. These mechanisms must also maintain the
applications properties after adaptation occurs.

Consequently, a shift in programming technologies and methodologies is needed to manage adaptivity successfully. Since every system, be it adaptive or not, has to be programmed, programming languages need to natively support adaptivity. Furthermore, having adaptivity as a linguistic construct enables us to design and to develop more
adequate verification tools that can help to prevent system failures due to erroneous or
unexpected changes.

This thesis addresses adaptivity, adopting an approach firmly based on programming languages and formal methods. In particular, we have two main concerns. The first one consists of introducing appropriate linguistic primitives to describe the context and to express adaptation. The second one is about the design of verification tools, based on static analysis techniques, in order to ensure that the software maintains its consistency after adaptation.