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.
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.
Table of Contents