Structured formal specifications
Peter White · 1990
Formal specification languages offer the ability to mathematically demonstrate a priori the correctness of a system, in place of the traditional a posteriori method of testing an implementation of a system. Such a priori knowledge of the correctness of the system may avoid many of the pitfalls of moden software development, such as continuous redesign and retesting of the system under development. If formal specification languages are to succeed in large scale software products, the languages must allow the structuring of formal specifications. The language must allow the user to break a problem into subproblems, specify solutions for the subproblems, and then combine the specifications into a solution for the original problem. This dissertation investigates using the mathematical notion of a category to provide structured formal specifications. A category is a collection of objects and arrows. A diagram in a category is also a collection of objects and arrows, however, a diagram does not satisfy some of the defining properties of a category. In this dissertation, diagrams are used to describe specifications of computer systems. A functor is a mapping between categories that preserves some of the structure of a category. Functors are used to describe the relation between category theoretic specifications. Given several category theoretic specifications, and functors to describe the relationships between them, the colimit construction is used to combine the specifications into another specification, which acquires features from the component specifications. The central results of this dissertation are the use of diagrams to represent specifications, the notion of completing a diagram into a category, the use of functors to describe the relation between categories, the explicit construction of a combined specification using the colimit construction, and the creation of new arrows in a combined specification, taking advantage of the properties acquired from the component specifications. The mathematical machinery in this dissertation is used on a nontrivial example, to construct a secure read specification from four component specifications. This nontrivial example demonstrates the power of the category theoretic technique to build a complex specification from simpler specifications.