Transforming constraint diagrams

Constraint diagrams were proposed by Kent for the purposes of formal software specification in a visual manner. They have recently been formalized and generalized, making them more expressive. This paper presents a collection of transformations that can be applied to the so called unitary α fragment of constraint diagrams. The transformations can be used to define inference rules in a more succinct manner than in earlier systems. We establish that the transformations are sufficient to transform any given unitary α-diagram into any other unitary α-diagram. Therefore, they are sufficient for formalizing any inference rules between such diagrams