A Two-Component Language for Adaptation: Design, Semantics, and Program Analysis

Adaptive systems are designed to modify their behaviour in response to changes of their operational environment. Wepropose a two-component language for adaptive programming, within the Context-Oriented Programming paradigm. It has adeclarative constituent for programming the context and a functional one for computing. We equip our language with a dynamic formalsemantics. Since wrong adaptation could severely compromise the correct behaviour of applications and violate their properties, wealso introduce a two-phase verification mechanism. It is based on a type and effect system that type-checks programs and computes,as an effect, a sound approximation of their behaviour. The effect is exploited at load time to mechanically verify that programs correctlyadapt themselves to all possible running environments.