Upward and downward progression

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. 

Example 7-9 LA fsum) is a better complete approximation of Sum than LA/ft sum). 

A first idea of a non-incremental stepwise synthesis strategy (with a fixed, finite number /of predefined steps) is to achieve downward progression  

In such a non-incremental synthesis, the series of expanded logic algorithms can be shown to progress upwards (see below). To achieve this expansion, we here only consider logic algorithms whose bodies are in disjunctive normal form. The used predicates are assumed to be either primitives or the predicate rhi that is defined by the logic algorithm. Let s start with a few basic definitions. 

Definition 7-21 LtiD[X] be a disjunct of a logic algorithm LA(r), such that the only free variables of D are the n universal variables X in the head of LA r), We say that D[X] covers atom r t) iff 3D[t] is true in 3. 

---

The non-incremental synthesis strategy above can now be refined as follows, so as to achieve simultaneous upward and downward progressions [Flener and Deville 92,93ab] ... 

---