LOGICAL COMBINATORS FOR SYSTEM CONFIGURATION

Abstract

System configuration describes the construction of complex engineering systems from their component parts. The configuration language is at a meta-Ievel to a specification language and expresses the horizontal structuring of specifications and modules by extension and parameterization; it also expresses the implementation, of both specifications and modules during the development of a software system. The logic chosen for system configuration is many-sorted first-order logic which possesses the Craig interpolation property. Configuration is expressed precisely within the logical framework by the operation of combinators on recursively defined configured objects of sorts in the set {specification, module}; each configured object is a named theory presentation. Properties of commutativity between the combinators are illustrated by equivalent paths in the three-dimensional development space for configuration. The actual building of configured objects is expressed by constructing diagrams within a categorical workspace that is based on the structure of a KZ-doctrine.