An algebraic proof in VDM ^♣

Abstract

We present a simple example to illustrate the algebraic, constructive style of specification and proof used in the Irish School of the VDM(VDM ^♣). The example exploits a new and fundamental result which we have used frequently in VDM ^♣. Our illustration also demonstrates a novel approach within in the VDM tradition which harnesses additional branches of abstract algebra for use in the specification and development of software. This innovation offers, we believe, several benefits: (i) an extension of the mathematical foundation of the emerging software engineering discipline, (ii) a more appropriate and abstract mathematical level at which the designer may work which abbreviates and simplifies proof and consequently (iii) a mathematical setting where insights into designs are easier to make and on foot of which designs may be confidently modified or improved. As a representative example, we also offer a proof,using the same approach, which we believe to be new, of one of the theorems used in the example.

The authors would like to acknowledge their debt to Dr. Mícheál Mac an Airchinnigh for his early work on indexed monoids and for encouraging us to experiment with them. We would also like to thank other members of the Formal Methods Working Group and the anonymous referees whose comments helped us improve the presentation of this paper.