Stepwise Logic Algorithm Synthesis Strategies

Let us now relate the refinement operator gen to the syntactic generality relation  

An inverse operator specjl of genjl is similarly defined, such that specjl is a syntactic specialization operator that can generate all logic algorithms of L r) from T.  

It is interesting to decompose a synthesis process into a series of steps, each designing an intermediate logic algorithm. Indeed  

Using the criteria defined in the two previous sections, a huge variety of stepwise synthesis strategies can be defined, fitting any valid combination of the features enumerated above. In Section 7.3.1, we briefly sketch a strategy for incremental synthesis, and in Section 7.3.2, we fully describe a strategy for non-incremental synthesis. 

---

Let s reconsider the strategies of stepwise synthesis of logic algorithms, seen in Section 7.3. An interesting idea, especially with non-incremental stepwise strategies, is then to establish a mapping between steps and the variables of a schema each step synthesizes instance(s) of some predicate- or schema-variable(s) of a given schema. 

---