An Incremental Synthesis Strategy

In the case of incremental synthesis, let s view the steps of one synthesis increment as a macro-step performing a transformation trans. Synthesis is then the design of a series of logic algorithms  

This covers iterative synthesis, where only the last presented example or property is actually used by trans. If trans is monotonic and continuous (wrt the order on logic algorithms), then trans Lj) is its least fixpoint. So if trans preserves partial correctness wrt then the fixed point is also partially correct wrt % Note that completeness wrt is not necessarily achieved, and that the resulting logic algorithm can involve infinitely many literals. This incremental strategy yields increasing (hence monotonic) synthesis it may yield consistent or inconsistent synthesis. 

---