Abstract :
We have defined a model suited to underly several kinds of symbolic
manipulations of programs: a linear loop is described through a
high-level of abstraction formalization of the computations it performs,
its schema. We showed that a small number of computation categories
and their refinements
suffice to describe a large number of loops.
We also implemented two systems, PRISME, that computes the schema of a
linear loop,
and SignEdit, that on the contrary synthesizes a loop from a schema, and integrated them
within a programming environment. This allowed us to
explore using schemas during several programming tasks: program construction,
comprehension, searching through and reasoning about programs.
In this paper, we introduce our model of schemas and show how it is
implemented, thus validated. We also discuss the roles schemas play in
programming tasks and describe the programming environment that
automates schema manipulation.
Ce papier est disponible sur demande à fb@ai.univ-paris8.fr.