ASE'99 Tutorial:
Schema-guided Generation of Correctly Reusable Programs

Pierre Flener, Uppsala University, Sweden
Kung-Kiu Lau, University of Manchester, UK
Mario Ornaghi, University of Milan, Italy
Julian Richardson, University of Edinburgh, UK

Schemas encode (human) programming methodologies, such as divide-and-conquer or constrain-and-generate, and are thus useful for guiding program development, as demonstrated by powerful, highly automated programming environments, such as KIDS, DesignWare, and PlanWare.

In this tutorial, we first briefly survey current research on program generation, so as to argue why schema-guided programming can overcome the drawbacks of the more traditional approaches, such as proofs-as-programs or transformation. Then we introduce the notion of specification framework, as a possibly parametric formalisation of a problem domain, which serves as background during all development steps. This allows us to give a semantic definition of schemas, while covering their representation, correctness, and reusability. Finally, we show how all this can be put to useful practice, by actively guiding the generation of correct and reusable programs through the (re)use of schemas. We address automation issues, compare with related work, and outline future work.


Pierre Flener is an associate professor in the Computer Science Division of the Department of Information Science at Uppsala University in Sweden. His main research interests lie in automating various tasks of software engineering, using the concept of schema.

Kung-Kiu Lau is a senior lecturer in the Department of Computer Science at the University of Manchester in the UK.  His current research is mainly about component-based software development (in computational logic).

Mario Ornaghi is an associate professor in the Department of Information Science at the University of Milan in Italy.  He is currently interested in the theoretical foundations of component-based software development.

Julian Richardson is a research fellow in the Mathematical Reasoning Group of the Institute for Representation and Reasoning in the Division of Informatics at the University of Edinburgh in the UK.  He carries out research in various aspects of automated theorem proving, including proof planning.


Cover Page
Table of Contents
  1. Introduction
  2. Our Definition of Correct Schemas
  3. Schema-Guided Program Generation
  4. Automation Issues
  5. Future Directions
  6. Conclusion