Reasoning about control

The concept now generally known as “Hoare logic” can be traced back at least as for as a paper of Turing. If you think of a program as a flowchart, the idea is to have inference rules that tell you what each component of the flowchart does to the state, thus allowing you  to make inferences about the whole program. We fell into our work after talking to some industry control engineers about something else, and realising that the way they explained things, component by component of the block diagram, used the same kind of inference rules.

Devising a satisfactory Hoare logic, without ugly side conditions, took us to presenting an abstraction of Hoare logic to traced symmetric monoidal categories, a very general framework for the theory of systems. Our abstraction is based on a traced monoidal functor from an arbitrary traced monoidal category into the category of pre-orders and monotone relations. This generalises the usual Hoare logics (partial correctness of while programs, partial correctness of pointer programs and so on), and allows us to develop new ones (for example run-time analysis of while programs and stream circuits).

We have applied this to  reason about linear systems expressed as block diagrams that give a graphical representation of a system of differential equations or recurrence equations. We use the notion of additive relation borrowed from homological algebra to give a convenient framework in which all diagrams have a semantic value. This  gives a sound system of Hoare-style rules for the block diagram constructors that singles out a tractable subset of the block diagram language in which all diagrams represent total functions. 

Work continues with collaborators Rob Arthan (Lemma One), Paulo Oliva (Queen Mary University of London) and Colin O'Halloran (D-Risq).