A Hoare logic for linear systems

We consider reasoning 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. We give 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. We show these rules in action on some simple examples from a variety of applications domains.