Modelling Jackson's programming method

The aim of this paper is to present a modelling scheme for programming methods and to illustrate it on Jackson's programming method. We first give a formal semantics to the objects of this method and we model the basic strategy of matching trees in order to build a program structure. In the next section we study how to support a formal development, its automatization, and the building of a formal specification within the scope of our model. Then an example is developed. The last section addresses alternative strategies suggested by the method in order to solve clash problems, where the basic strategy fails. Boundary and ordering clash situations are presented and their strategies are modelled.