  When developing complex software and systems, contracts provide a means for
controlling the complexity by dividing the responsibilities among the
components of the system in a hierarchical fashion. In specific application
areas, dedicated contract theories formalise the notion of contract and the
operations on contracts in a manner that supports best the development of
systems in that area. At the other end, contract meta-theories attempt to
provide a systematic view on the various contract theories by axiomatising
their desired properties. However, there exists a noticeable gap between the
most well-known contract meta-theory of Benveniste et al., which focuses on the
design of embedded and cyber-physical systems, and the established way of using
contracts when developing general software, following Meyer's
design-by-contract methodology. At the core of this gap appears to be the
notion of procedure: while it is a central unit of composition in software
development, the meta-theory does not suggest an obvious way of treating
procedures as components.
  In this paper, we provide a first step towards a contract theory that takes
procedures as the basic building block, and is at the same time an
instantiation of the meta-theory. To this end, we propose an abstract contract
theory for sequential programming languages with procedures, based on
denotational semantics. We show that, on the one hand, the specification of
contracts of procedures in Hoare logic, and their procedure-modular
verification, can be cast naturally in the framework of our abstract contract
theory. On the other hand, we also show our contract theory to fulfil the
axioms of the meta-theory. In this way, we give further evidence for the
utility of the meta-theory, and prepare the ground for combining our
instantiation with other, already existing instantiations.
