This paper presents a Hoare-style logic for reasoning about the frequency response of control systems in the continuous-time
domain. Two properties, the gain (amplitude) and phase shift, of a control system are considered. These properties are for
a sinusoidal input of variable frequency. The logic operates over a simplified form of block diagram, including arbitrary
transfer functions, feedback loops, and summation of signals. Reasoning is compositional, i.e. properties of a system can
be deduced from properties of its subsystems. A prototype tool has been implemented in a mechanised theorem prover.
Research supported by QinetiQ and by an EPSRC studentship to the second author.
Affiliation with the University of St Andrews ceased in June 2002.