ABSTRACT. Software synthesis tools support the translation of requirements into acceptable software de-
signs. The requirements may be expressed logically, with a deductive design process, or the
requirements may come in the form of datasets, with an inductive design process. This session
focuses on modularity in software synthesis, and in particular on modular knowledge about re-
quirements, software design, and the structure of the design process. We briefly outline some of
the key forms of modularization that arise in these aspects of software synthesis.
1. Requirements
For applications where mathematical correctness is important, requirements and high-level
designs can be structured using formal logical specifications as finite presentations of theo-
ries, which are composed using specification morphisms and colimits. For machine learning
applications, the requirements come in form of structured data sets.
2. Software Design Knowledge
Representations of software design knowledge allow developers to guide an automated synthe-
sis system so that it can effectively translate requirement-level specifications into acceptable
high-level designs. Transformations (replace specification or code patterns by other code
patterns) and inference rules that relate logical goals with program structure (e.g. deduc-
tive synthesis rules) provide some of the basic design knowledge modules for any synthesis
system. Larger grain modules can capture reusable higher-level design knowledge: algorithm
design theories, datatype specifications and refinements, formalized design patterns, and
architectural patterns. These are used with deductive/refinement techniques to generate ini-
tial designs from requirement-level specifications. Machine learning applications also exploit
larger-grain patterns, such as linear regression models and neural networks. These provide a
computation pattern (with parameters to-be-learned and chosen hyperparameters) that can
be instantiated using methods for fitting models to the given data. More ad-hoc forms of de-
sign knowledge include sketches, program templates, and schemata. These are used with (1)
deductive/refinement techniques to generate instantiations from logical specifications, or (2)
inductive generalization techniques that search a space of instances given concrete examples.
3. Derivations
A software synthesis process that generates interesting software usually involves the compo-
sition of many kinds of design knowledge and so it is relevant to consider the structuring of
that composition, called a derivation. Derivations can be a sequence (or tree) of specifications
where each is derived from its predecessor by applying a module of design knowledge. Typ-
ically, the early knowledge applications in a derivation introduce the overall algorithmic or
architectural structure and then many more knowledge applications are applied to improve
performance and to fit the design to the target computational substrate.
