**A research project in applying formal methods
at The Boeing Company, Seattle, Washington, USA is investigating
category-theoretic methods for knowledge-based systems development
and automated software synthesis. **

**Using The Kestrel Institute's Specware (TM) package (see publications and an index), investigators are experimenting with the automated
synthesis of detailed software specifications from simple, abstract
component specifications, and the automated translation of
specifications into programs in a target programming language.
**

**In doing this mathematically, the
specifications are formalized as finite presentations of theories in
a formal logic. Pairs of specifications are related through
mathematical relationships called specification morphisms, which
ensure that provable statements in one theory are representable as
provable statements in the other. Diagrams of specifications and
specifications morphisms represent a complex of interrelated theories
about an application (for example, theories of manufacturing,
material properties, and geometry are interrelated in manufacturing
airplane parts). An algorithm for finding colimits of these diagrams
is applied to synthesize detailed specifications that embody the
specifications and relationships expressed in the diagrams.
**

**In this way, knowledge about an application,
expressed mathematically (through categorical logic) is built up in a
sequential/parallel refinement process to produce mathematically
verified specifications for software. Software is then produced
through categorical mappings that transform theories from one logic
to another (i.e., from the specification logic to a formally-defined
version of a programming language). Categorical concepts in addition
to colimits, such as functors and natural transformations, and
sheaf-theoretic concepts that express commonality between
specifications in a diagram, are fundamental parts of this
process.**

***This document does not represent an official position of The
Boeing Company or any of its subsidiaries or suppliers.**