Proving Systolic Systems Correct

Abstract

A language for describing communicating systems is described. It is sufficiently expressive to describe both the desired behavior of systems, their specifications , and their actual implementations in terms of simpler components. We say I satisfies S if 1 is a correct implementation of the specification S . We briefly discuss a semantic treatment of this notion of satisfaction, but the main emphasis of the paper is on a proof technique for proving statements of the form I satisfies S , based on syntactic transformations and induction. Two examples are given, both systolic systems from the literature.