  Design-by-contract is an important technique for model-based design in which
a composite system is specified by a collection of contracts that specify the
behavioural assumptions and guarantees of each component. In this paper, we
describe a unifying theory for reactive design contracts that provides the
basis for modelling and verification of reactive systems. We provide a language
for expression and composition of contracts that is supported by a rich
calculational theory. In contrast with other semantic models in the literature,
our theory of contracts allow us to specify both the evolution of state
variables and the permissible interactions with the environment. Moreover, our
model of interaction is abstract, and supports, for instance, discrete time,
continuous time, and hybrid computational models. Being based in Unifying
Theories of Programming (UTP), our theory can be composed with further
computational theories to support semantics for multi-paradigm languages.
Practical reasoning support is provided via our proof framework, Isabelle/UTP,
including a proof tactic that reduces a conjecture about a reactive program to
three predicates, symbolically characterising its assumptions and guarantees
about intermediate and final observations. This allows us to verify programs
with a large or infinite state space. Our work advances the state-of-the-art in
semantics for reactive languages, description of their contractual
specifications, and compositional verification.
